Scala 3中非直谓式类型赋值：两类定义差异及可行原因解析

Scala 3是一门非直谓式语言，通常不能把高阶类型直接赋值给常规类型（否则可能触发Girard悖论），但下面两段代码的表现却截然不同：

trait Vec[T]

type VV1 = Vec // 触发悖论！

type VV2 = [T] => Vec[T] // 无悖论？

两行代码的核心差异 #

• type VV1 = Vec：这里直接把高阶类型Vec（它需要接收一个类型参数，属于* -> *的kind）赋值给了默认kind为*的类型别名VV1。简单说就是试图把一个"类型生成器"当成"具体类型"来用，这直接违反了非直谓式类型系统的约束，会触发悖论相关的类型错误。
• type VV2 = [T] => Vec[T]：这是Scala 3的类型lambda语法，它定义的是一个* -> * kind的类型构造器，和Vec本身的kind完全匹配。这里并没有把高阶类型降级成常规类型，只是用lambda的形式重新描述了和Vec等价的类型构造器，本质上是同一类东西，所以不会有问题。

为什么第二行代码可行？ #

Scala 3的类型系统里，类型lambda的作用是显式描述类型构造器的行为，它的kind和被赋值的类型别名完全一致：

1. [T] => Vec[T]的kind是* -> *，和Vec一模一样，赋值给VV2时没有改变类型的kind层级，不存在把高阶类型塞进常规类型位置的操作。
2. Girard悖论的触发前提是允许"类型构造器被当作具体类型使用"，进而导致类型系统逻辑不一致。而第二行只是用lambda语法重新定义了一个同层级的类型构造器，没有跨越kind的边界，自然不会触发悖论。

内容的提问来源于stack exchange，提问作者tribbloid