Simple presentation of singletons in Scala

Dep.scala

package dep

import scala.language._

object Dep extends App {

  sealed trait Nat {
    type Plus[M <: Nat] <: Nat
    def plus[M <: Nat](m: M): Plus[M]
  }

  implicit object Z extends Nat {
    type Plus[M <: Nat] = M
    def plus[M <: Nat](m: M) = m
    override def toString = "Z"
  }

  type Z = Z.type

  case class S[N <: Nat](n: N) extends Nat {
    type Plus[M <: Nat] = S[N#Plus[M]]
    def plus[M <: Nat](m: M) = S(n plus m)
  }

  implicit def getS[N <: Nat](implicit n: N): S[N]= S(implicitly[N])

  type T0 = Z
  type T1 = S[T0]
  type T2 = S[T1]
  type T3 = S[T2]
  type T4 = S[T3]
  type T5 = S[T4]
  type T6 = S[T5]
  type T7 = S[T6]
  type T8 = S[T7]
  type T9 = S[T8]


  sealed trait Vect[+A, N <: Nat] {
    def ++[B >: A, M <: Nat](other: Vect[B, M]): Vect[B, N#Plus[M]]
    def length: N
  }

  final case object VNil extends Vect[Nothing, Z] {
    def ++[B, M <: Nat](other: Vect[B, M]) = other
    def length = implicitly
  }
  final case class VCons[A, B >: A, N <: Nat](b: B, xs: Vect[A, N]) extends Vect[B, S[N]] {
    def ++[C >: B, M <: Nat](other: Vect[C, M]) = VCons(b, xs ++ other)
    def length = S(xs.length)
  }

  val two: Vect[Int, T2] = VCons(1, VCons(2, VNil))
  val one: Vect[Int, T1] = VCons(3, VNil)
  val three: Vect[Int, T3] = two ++ one
}

This is some fantastic stuff. Thanks for taking the time to share it! I've actually turned that blog post along with some of the follow up posts into polished articles for NFJS Magazine. They've been received so well, I've decided to take them to leanpub and develop them further. I think the book will be unique having been written by someone actively learning the topic. 👍