理解Scala GADT支持的限制

12 浏览
0 Comments

理解Scala GADT支持的限制

对于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 // 构造函数无法实例化到期望的类型；找到：B[V]；要求：A[Option[U],?V1]，其中类型?V1 <: V（这是一个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 // 这个可以工作
  }
}

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

如果我们在trait A（和case class 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() => ??? // 构造函数无法实例化到期望的类型；找到：B；要求：A[U]
  }
}
object Test2 {
  def test2[U](t: A[U]) = t match {
    case B() => ??? // 这个可以工作
  }
  def test3[U] = {
    def test(t: A[U]) = t match {
      case B() => ??? // 这个可以工作
    }
  }
}

像这样简化之后，它看起来更像是一个编译器的错误或限制。或者是我漏掉了什么吗？

0