类型级别的`F[_ <: A] <: B` 和值级别的`f: A => B` 之间的类比

如何解决类型级别的`F[_ <: A] <: B` 和值级别的`f: A => B` 之间的类比

假设 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

高阶统一一般是不可判定的，所以编译器必须将其限制为合理的子集