scala - 了解 Scala GADT 支持的限制

Question

Test.test 中的错误似乎不合理：

sealed trait A[-K, +V]
case class B[+V]() extends A[Option[Unit], V]

case class Test[U]() { 
  def test[V](t: A[Option[U], V]) = t match {
    case B() => null // constructor cannot be instantiated to expected type; found : B[V] required: A[Option[U],?V1] where type ?V1 <: V (this is a GADT skolem)
  }
  def test2[V](t: A[Option[U], V]) = Test2.test2(t)
}

object Test2 {
  def test2[U, V](t: A[Option[U], V]) = t match {
    case B() => null // This works
  }
}

有几种方法可以使错误更改或消失：

如果我们删除特征 A（和案例类 B）上的 V 参数，错误的“GADT-skolem”部分就会消失，但“构造函数无法实例化”部分仍然存在。

如果我们将 Test 类的 U 参数移到 Test.test 方法中，错误就会消失。为什么？（同样，Test2.test2 中不存在该错误）

以下链接也确定了该问题，但我不理解提供的解释。http://lambdalog.seanseefried.com/tags/GADTs.html

这是编译器中的错误吗？(2.10.2-RC2)

感谢您为澄清这一点提供的任何帮助。

2014/08/05：我设法进一步简化了代码，并提供了另一个示例，其中 U 绑定在立即函数之外而不会导致编译错误。我仍然在 2.11.2 中观察到这个错误。

sealed trait A[U]
case class B() extends A[Unit]

case class Test[U]() {
  def test(t: A[U]) = t match {
    case B() => ??? // constructor cannot be instantiated to expected type; found : B required: A[U]
  }
}

object Test2 {
  def test2[U](t: A[U]) = t match {
    case B() => ??? // This works
  }
  def test3[U] = {
    def test(t: A[U]) = t match {
      case B() => ??? // This works
    }
  }
}

像这样简化，这看起来更像是编译器错误或限制。还是我错过了什么？

score 12 · Accepted Answer

构造函数模式必须符合模式的预期类型，这意味着 B <: A[U]，如果 U 是当前被调用方法的类型参数，则该声明为真（因为它可以实例化为适当的类型参数) 但如果 U 是先前绑定的类类型参数，则不正确。

您当然可以质疑“必须符合”规则的价值。我知道我有。我们通常通过向上转换被检查者直到构造函数模式符合来规避这个错误。具体来说，

// Instead of this
def test1(t: A[U]) = t match { case B() => ??? }

// Write this
def test2(t: A[U]) = (t: A[_]) match { case B() => ??? }

附录：在评论中，提问者说“问题很简单，为什么它不能在类级别与类型参数一起使用，但在方法级别可以使用。” 实例化的类类型参数在外部是可见的，并且具有无限的生命周期，对于实例化的方法类型参数，这两者都不是真的。这对类型的健全性有影响。给定 Foo[A]，一旦我拥有一个 Foo[Int]，那么 A 在引用该实例时必须是 Int，永远永远都是。

原则上，您可以在构造函数调用中类似地处理类类型参数，因为类型参数仍然是未绑定的并且可以机会主义地推断出来。不过，就是这样。一旦它在世界上出现，就没有重新谈判的余地。

另一个附录：我看到人们经常这样做，假设编译器是正确性的典范，我们要做的就是思考它的输出，直到我们的理解发展到足以匹配它为止。这样的心理体操已经在那个帐篷下进行了，我们可以为太阳马戏团工作几次。

scala> case class Foo[A](f: A => A)
defined class Foo

scala> def fail(foo: Any, x: Any) = foo match { case Foo(f) => f(x) }
fail: (foo: Any, x: Any)Any

scala> fail(Foo[String](x => x), 5)
java.lang.ClassCastException: java.lang.Integer cannot be cast to java.lang.String
  at $anonfun$1.apply(<console>:15)
  at .fail(<console>:13)
  ... 33 elided

那是 scala 的当前版本 - 它仍然是它的功能。没有警告。所以也许问问自己，为一种语言和实现提供正确性假设是否明智，这种语言和实现在存在十多年后仍然非常不健全。

score 7 · Accepted Answer

看起来这是一个编译器警告。由此，马丁·奥德斯基将其描述为：

In the method case, what you have here is a GADT: 
Patterns determine the type parameters of an corresponding methods in the scope of a pattern case.     
GADTs are not available for class parameters.    

As far as I know, nobody has yet explored this combination, and it looks like it would be quite tricky to get this right.

PS：感谢@retronym ，他在这里提供了讨论的参考

关于为什么在类的情况下会引发错误：

这有效：

sealed trait A[-K, +V]
case class B[+V]() extends A[Option[Unit], V]
case class Test[U]() {

   def test[V, X <: Unit](t: A[Option[X], V]) = t match {
     case B() => null
   }
   def test2[V](t: A[Option[U], V]) = Test2.test2(t)
}

object Test2 {
      def test2[U, V](t: A[Option[U], V]) = t match {
         case B() => null // This works
       }
 }

举例说明编译器抛出错误的原因：尝试这样做：

scala> :paste
// Entering paste mode (ctrl-D to finish)

abstract class Exp[A]{
        def eval:A = this match {
            case Temp(i) => i     //line-a
          }
        }
case class Temp[A](i:A) extends Exp[A]

// Exiting paste mode, now interpreting.

要理解这一点，从§8.1.6 开始：上面Temp是一个多态类型。如果案例类是多态的，那么：

如果 case 类是多态的，则实例化其类型参数，以便 c 的实例化符合模式的预期类型。然后将 c 的主构造函数的实例化形式参数类型作为组件模式 p 1 的预期类型。. . , 点。该模式匹配从构造函数调用 c(v1 , . . . , vn ) 创建的所有对象，其中每个元素模式 pi 匹配相应的值 vi 。

即编译器巧妙地尝试Temp在 line-a 中实例化，使其符合this( 如果上面编译成功，那么在这种情况下Temp(1)将是类似的Exp[Int]，因此编译器在 line-a 中实例化 Temp ，参数为 as Int。

现在在我们的例子中：编译器正在尝试实例化B. 它看到的是已经固定并从类参数获得t的类型A[Option[U],V]，并且是方法的泛型类型。在尝试初始化时，它会尝试以最终获得. 因此，它以某种方式试图得到. 但它不能原样。因此它最终无法初始化。解决此问题使其工作UVBA[Option[U],V]B()A[Option[U],V]BA[Option[Unit],V]B

在 test-2 的情况下不需要它，因为：上述过程中解释的编译器正在尝试初始化 B 的类型参数。它知道 t 具有类型参数 [Option[U], V] 其中 U 和 V 都是通用 wrt 方法并且是从参数中获得的。它尝试根据 agrument 初始化 B。如果参数是新的 B[String]，它会尝试派生 B[String]，因此 U 会自动作为 Option[Unit] 获得。如果参数是 new A[Option[Int],String] 那么它显然不会匹配。

score 3 · Accepted Answer

不同之处在于编译器和运行时在每种情况下都有哪些信息，以及对类型的限制。通过让 U 为特征和类参数，以及 X 为方法类型参数来澄清歧义。

sealed trait A[U]
case class B(u: Unit) extends A[Unit]

class Test[U]() {
  def test(t: A[U]) = t match {
    case B(u) => u // constructor cannot be instantiated to expected type; found : B required: A[U]
  }
}

object Test2 {
  def test2[X](t: A[X]) = t match {
    case B(x) => x // This works
  }
  def test3[X] = {
    def test(t: A[X]) = t match {
      case B(x) => x // This works
    }
  }
}

Test2.test2(new B(println("yo")))

在 Test2.test2 中，编译器知道将提供一个 A[X] 的实例，对 X 没有限制。它可以生成检查提供的参数是否为 B 的代码，并处理这种情况。

在类 Test 方法 test 中，编译器不知道在调用时提供了某些 A[X]，而是提供了某些特定类型 U。这种类型的 U 可以是任何东西。但是，模式匹配是基于代数数据类型的。此数据类型只有一个有效变体，类型为 A[Unit]。但此签名适用于 A[U]，其中 U 不受 Unit 限制。这是一个矛盾。类定义说 U 是一个自由类型参数，方法说它是 Unit。

想象一下你实例化测试：

val t = new Test[Int]()

现在，在使用现场，方法是：

def test(t: A[Int])

没有这样的类型 A[Int]。B 上的模式匹配是编译器检查此条件时。任何 U 的 A[U] 都与类型不兼容，因此“构造函数无法实例化为预期类型；发现：需要 B：A[U]”

方法与类类型参数的区别在于，在运行时调用方法时，一个是绑定的，一个是空闲的。

另一种思考方式是定义方法

def test(t: A[U])

暗示 U 是 Unit，这与 U 是任何东西的类声明不一致。

score 1 · Accepted Answer

Edit: this is not an answer to the question. I'm keeping it for reference (and the comments).

The link you provided already gives the answer.

In the case of the parameterised method, U is infered from the argument of the actual method call. So, the fact that the case B() was chosen implies that U >: Unit (otherwise the method could not have been called with a B) and the compiler is happy.

In the case of the parameterized class, U is independent from the method argument. So, the fact that the case B() was chosen tells the compiler nothing about U and it can not confirm that U >: Unit. I think if you add such a type bound to U it should work. I haven't tried it, though.

score 0 · Accepted Answer

编译器的错误信息是绝对正确的。一个简单的例子应该很好地描述了这个问题：

sealed trait A[U]
class B extends A[Unit]

class T[U] {
  val b: A[Unit] = new B
  f(b) // invalid, the compiler can't know which types are valid for `U`
  g(b) // valid, the compiler can choose an arbitrary type for `V`

  def f(t: A[U]) = g(t)
  def g[V](t: A[V]) = ???
}

f并g具有不同的类型签名。g采用A[V]whereV是任意类型参数。另一方面，f接受A[U]whereU不是任意的，而是依赖于外部类T。

编译器在进行类型检查时不知道U可以是什么类型T- 它需要对实例的实例进行T类型检查以找出使用了哪些类型。可以说这U是内部的具体类型T，但外部的泛型类型。这意味着它必须拒绝每个T更具体的关于U.

g显然允许从内部调用f- 毕竟V可以选择任意类型，U在这种情况下。因为U它永远不会再被引用，g它可能有什么类型并不重要。

您的其他代码示例具有相同的限制 - 它只是一个更复杂的示例。

顺便说一句，这段代码

def test3[U] = {
  def test(t: A[U]) = t match {
    case B() => ??? // This works
  }
}

有效对我来说看起来很奇怪。是否被类或方法绑定并不重要U——在绑定范围内，我们不能保证它的类型，因此编译器也应该拒绝这个模式匹配。

scala - 了解 Scala GADT 支持的限制

5 回答 5

Related

Reference