DOT演算中的列表编码

Question

我正在阅读The Essence of Dependent Object Types，发现列表的以下编码：

为什么要写：

nil: sci.List ∧ {A = ⊥}

尤其是为什么要给A型底？类型不应该像cons一样是多态的吗？

Answer 1

[Nothing是Scala的底部类型-它是没有成员的类型，因此您可以轻松地说它的每个成员都是其他类型的成员而无需说谎。

单独使用Nothing（作为返回类型）用来表示该函数从不返回值，这通常意味着它引发异常。如果有任何容器/包装器/工厂/如何调用if Nothing，则意味着它不能包含包装器/包含或产生值的任何版本：

• List[Nothing]-是一个没有任何值的列表，
• Future[Nothing]-是循环运行或以异常结束的Future
• Option[Nothing]-是Option，不能包含值

关于List，如果您决定使用Cons + Nil作为编码，那么说您想做的没有任何奇怪的事情：

sealed trait List[A]
case class Cons[A](a: head, tail: List[A]) extends List[A]
case class Nil[A]() extends List[A]

您不能简单地使用对象Nil，因为它必须更容易使用和模式匹配，因为您必须在任何地方定义其类型。

Cons(1, Cons(2, Cons(3, Cons(4, Nil[Int]))))

但是，如果您使List[A]为协变量，那么如果A是B的子类型，那么List[A]将是List[B]的子类型。

sealed trait List[+A] // notice + before A
case class Cons[+A](a: head, tail: List[A]) extends List[A]
case class Nil[+A]() extends List[A]

然后我们可以利用Nothing作为其他所有类型的子类型：

val nil = Nil[Nothing]
Cons(1, Cons(2, Cons(3, Cons(4, nil))))
Cons("a", Cons("b", Cons("c", Cons("d", nil))))

为了方便起见（例如，模式匹配），我们可以将Nil设为对象：

sealed trait List[+A]
case class Cons[+A](a: head, tail: List[A]) extends List[A]
case object Nil extends List[Nothing]

这就是当前Scala（2）中的工作方式，并且在Dotty中没有更改。您的示例中的DOT演算说明了这是如何转化为形式主义的：除了Nothing之外，您没有⊥，其他所有内容基本上都相同，但是符号不同。