了解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
    }
  }
}

简化,这看起来更像是编译器错误或限制.或者我错过了什么？

Answer 1

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

你当然可以质疑"必须符合"规则的价值.我知道我有.我们通常通过向上转换scrutinee来避免这个错误,直到构造函数模式符合.特别,

// 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的当前版本 - 这仍然是它的作用.没有警告.因此,也许可以问问自己,对一种语言和实施的正确性假设是否明智,这种语言和实施在存在十多年之后是如此微不足道.

Answer 2

看起来这是一个编译器的警告.从这个,马丁·奥德斯基所说的:

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,...的预期类型...,pn.该模式匹配从构造函数调用c(v1,...,vn)创建的所有对象,其中每个元素模式pi与对应的值vi匹配.

即编译器巧妙地尝试Temp在行中进行实例化,使其符合主要构造函数this(如果上面编译成功,那么在Temp(1)类似的情况下,Exp[Int]编译器将实例化为带有参数的行-a)Int.

现在在我们的例子中:编译器正在尝试实例化B.它看到t的类型是A[Option[U],V]其中U已经是固定的,并从类参数获得,并且V是通用类型的方法.在尝试初始化时B,尝试以最终获得的方式创建A[Option[U],V].因此,B()它以某种方式试图获得A[Option[U],V].但它不能为B是A[Option[Unit],V].因此它最终无法初始化B.修复它使它工作

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