Search code examples
scalatypesdependent-typedottyscala-3

List encoding in the DOT calculus

I was reading The Essence of Dependent Object Types and found the following encoding of Lists:

enter image description here

Why would one write:

nil: sci.List ∧ {A = ⊥}

in particular, why do we give A type bottom? Shouldn't the type be polymorphic like in cons?

Solution

  • Nothing is a bottom type is Scala - it is a type, which has no members, so you can easily say that each of its members is a member of every other type without lying.

    On its own Nothing (as a return type) is used to say that function never returns value, which usually means that it throws exception. If you have any container/wrapper/factory/however you call if of Nothing, it means that it cannot contain a version of wrapper/whatever that contains/produces value:

    • List[Nothing] - is a List without any values,
    • Future[Nothing] - is a Future which runs in loop or ends up with exception
    • Option[Nothing] - is Option, that cannot contain a value

    When it comes to List if you decide on using Cons+Nil as encoding, let's say you want to do it without any weird things:

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

    You cannot simply use object Nil which would have easier usage and pattern matching, because you have to define its type everywhere. So unfortunately you cannot have one Nil, but you need a separate Nil for every type.

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

    But, it you made List[A] covariant then if A is subtype of B then List[A] would be subtype of 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]

    then we could make use of Nothing being a subtype of every other type:

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

    at this point for our own convenience (e.g. pattern matching) we could make Nil an object:

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

    Thanks to that we need only one Nil instead of one for every type.

    That is how it works in the current Scala (2) and it hasn't changed in Dotty. DOT calculus in your example shows how this translates to formalism: instead of Nothing you have ⊥, everything else is basically the same but with a different notation.