问题描述
假设 F[_ <: A] <: B
作为 f: A => B
的类型级模拟,让 [F[_ <: Int] <: List[Int],A <: Int]
,那么当 {{1} 时不应键入 application F[A]
yield List[Int]
},所以 A = Int
应该在以下情况下编译
f(List(42))
通过显式提供类型参数来应用错误消息使其工作
$ scala3-repl
scala> def f[F[_ <: Int] <: List[Int],A <: Int](as: F[A]) = as
def f[F[_$1] <: List[Int],A <: Int](as: F[A]): F[A]
scala> f(List(42))
1 |f(List(42))
| ^^^^^^^^
|Found: List[Int]
|required: F[A]
|
|where: A is a type variable with constraint <: Int
| F is a type variable with constraint <: [_$1 <: Int] =>> List[Int]
类比在哪里中断?我将 scala> f[[_ <: Int] =>> List[Int],Int](List(42))
val res0: List[Int] = List(42)
视为从 F[_ <: Int] <: List[Int]
到 Int
的类型级函数的心智模型哪里错了?
解决方法
首先关于推断类型 lambdas,我认为类型推断不会达到仅仅为了满足约束而提出类型 lambdas 的程度,否则从直觉上看,似乎一切都基本上可以使用一些复杂的类型 lambda 进行类型检查,并且在发现类型错误方面没有用处。
至于为什么 f[List,Int](List(42))
无法编译(因此无法推断),我们需要参考 lambdas 类型的 Subtyping Rules:
假设有两种类型的 lambdas
type TL1 = [X >: L1 <: U1] =>> R1
type TL2 = [X >: L2 <: U2] =>> R2
然后TL1 <: TL2
,如果
- 类型区间
L2..U2
包含在类型区间L1..U1
中(即L1 <: L2
和U2 <: U1
), R1 <: R2
还要注意:
部分应用的类型构造函数如 List
被假定为等价于它的 eta 扩展。即,List = [X] =>> List[X]
。这允许将类型构造函数与类型 lambda 进行比较。
这意味着所有这些都会编译:
f[[_ <: Int] =>> List[Int],Int](List(42)) //author's compiler example
f[[_] =>> List[Int],Int](List(42)) //input type bounds can be wider,output stays the same
f[[_] =>> List[42],Int](List(42)) //input wider,output narrower
f[[x <: Int] =>> List[x],Int](List(42))//input same,output narrower
所有这些都不会:
f[[x] =>> List[x],Int](List(42)) //input type bounds can be wider but in this case it will also make the output wider
f[List,Int](List(42)) //equivalent to preceding case
f[[_ <: 42] =>> List[Int],Int](List(42)) //input type bounds cannot be narrower
在以下情况下:
def f[F[x] <: List[x],A <: Int](as: F[A]) = as
如果您从相同类型的 lambda 角度来看它,f[[x] =>> List[x],Int](List(42))
应该可以工作,因此 f[List,Int](List(42))
也可以编译(并被推断)。
基于smarter
?F := List
扩展到
?F = [X] =>> List[X]
不是约束的有效解决方案
?F <: [X <: Int] =>> List[Int]
因为我们检查
List[X] <: List[Int]
对于任意 X
。
所以关键似乎是,当涉及到类型检查类型构造函数时,编译器只会使用来自类型构造函数定义的信息,而不是来自类型子句的额外信息。所以因为 List
被定义为
trait List[+A]
其中 A
是任意的,即 A >: Nothing <: Any
,然后编译器只使用该信息,而不使用它可能从更广泛的类型子句中获取的 X <: Int
。如果类型构造函数 List
被定义为
trait List[+A <: Int]
例如,它会键入检查。至于为什么它不推断出更具体的类型 lambda,这似乎与类型构造函数统一通常是 undecidable
高阶统一一般是不可判定的,所以编译器 必须将其限制为合理的子集