Nothing - это нижний тип Scala - это тип, в котором нет членов, поэтому можно легко сказать, что каждый из его членов является членом любого другого типа, не лгая.
Сам по себе Nothing (в качестве возвращаемого типа) используется, чтобы сказать, что функция никогда не возвращает значение, что обычно означает, что она выдает исключение. Если у вас есть какой-либо контейнер / упаковщик / фабрика / однако вы звоните, если Nothing, это означает, что он не может содержать версию оболочки / независимо от того, что содержит / производит значение:
List[Nothing] - это список без каких-либо значений, Future[Nothing] - это будущее, которое выполняется в l oop или заканчивается исключением Option[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] ковариантным, тогда, если 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]
Благодаря этому нам нужен только один Nil вместо одного для каждого типа.
Вот как это работает в текущем Scala (2), и оно не изменилось в Дотти. Исчисление DOT в вашем примере показывает, как это переводится на формализм: вместо Nothing у вас есть ⊥, все остальное в основном то же самое, но с другой нотацией.