Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
Simple presentation of singletons in 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 comment has been minimized.

Copy link

@joescii joescii commented Aug 20, 2014

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. 👍

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment