scala - DOT 演算中的列表编码

Question

我正在阅读依赖对象类型的本质，发现列表的以下编码：

为什么要写：

nil: sci.List ∧ {A = ⊥}

特别是，为什么我们给A型底部？类型不应该像 cons 中那样是多态的吗？

score 3 · Accepted Answer

Nothing是底层类型是 Scala - 它是一个没有成员的类型，所以你可以很容易地说它的每个成员都是其他类型的成员，而不会说谎。

就其本身Nothing而言（作为返回类型）用于表示函数从不返回值，这通常意味着它会引发异常。如果你有任何容器/包装器/工厂/但是你调用 if of Nothing，这意味着它不能包含包装器的版本/任何包含/产生值的东西：

当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更容易使用和模式匹配的对象，因为你必须在任何地方定义它的类型。所以不幸的是，你不能拥有一个Nil，但你需要Nil为每种类型提供一个单独的。

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

但是，如果你做了List[A]协变，那么 ifA是的子类型BthenList[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]

多亏了这一点，我们只需要一个Nil，而不是每种类型的一个。

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

1 回答 1