sized_list.scala

// I was reading through these examples: http://apocalisp.wordpress.com/2010/06/08/type-level-programming-in-scala/
// and I thought it would be nice to more quickly get to something useful, to show the power of the techniques.
object SizedListExample {
  // Type of all Non-negative integers
  sealed trait Nat
  // This is zero.
  sealed trait _0 extends Nat
  // Successor to some non-negative number
  sealed trait Succ[N <: Nat] extends Nat

  // Convert types into values:
  trait Count[N <: Nat] { def toInt: Int }
  def toInt[N <: Nat](implicit c: Count[N]): Int = c.toInt
  implicit val zCount: Count[_0] = new Count[_0] { def toInt = 0 }
  implicit def nCount[N <: Nat](implicit c: Count[N]): Count[Succ[N]] = {
    val c_1 = toInt[N]
    new Count[Succ[N]] { def toInt = c_1 + 1 }
  }

  // Make a very simple sized linked list
  sealed trait LList[N<:Nat, +T] {
    def fold[U](init: U)(fn: (U, T) => U): U
    // map preserves length, not flatMap/filter don't work
    def map[U](fn: T => U): LList[N, U]
    // Note: zip requires a list of the same length
    def zip[U](that: LList[N, U]): LList[N, (T, U)]
    // Note: size is one bigger after this
    def ::[U>:T](h: U): LList[Succ[N], U]
  }
  final case object LNil extends LList[_0, Nothing] {
    def fold[U](init: U)(fn: (U, Nothing) => U) = init
    def map[U](fn: Nothing => U) = LNil
    def zip[U](that: LList[_0, U]) = LNil
    def ::[U>:Nothing](h: U) = Cons(h, LNil)
  }
  final case class Cons[N<:Nat,+T](head: T, tail: LList[N, T]) extends LList[Succ[N], T] {
    def fold[U](init: U)(fn: (U, T) => U) = tail.fold(fn(init, head))(fn)
    def map[U](fn: T => U) = Cons(fn(head), tail.map(fn))
    def zip[U](that: LList[Succ[N], U]) = {
      that match {
        case Cons(thead, ttail) => Cons((head, thead), tail.zip(ttail))
      }
    }
    def ::[U>:T](h: U) = Cons(h, this)
  }
}

/******
 scala> import SizedListExample._
import SizedListExample._

scala> 1 :: 2 :: 3 :: LNil
res19: SizedListExample.Cons[SizedListExample.Succ[SizedListExample.Succ[SizedListExample._0]],Int] = Cons(1,Cons(2,Cons(3,LNil)))

scala> "hey" :: "you" :: LNil
res20: SizedListExample.Cons[SizedListExample.Succ[SizedListExample._0],java.lang.String] = Cons(hey,Cons(you,LNil))

scala> res19 zip res20
<console>:31: error: type mismatch;
 found   : SizedListExample.Cons[SizedListExample.Succ[SizedListExample._0],java.lang.String]
 required: SizedListExample.LList[SizedListExample.Succ[SizedListExample.Succ[SizedListExample.Succ[SizedListExample._0]]],?]
              res19 zip res20
                        ^

scala> res19 zip ("fixed" :: res20)
res22: SizedListExample.Cons[SizedListExample.Succ[SizedListExample.Succ[SizedListExample._0]],(Int, java.lang.String)] = Cons((1,fixed),Cons((2,hey),Cons((3,you),LNil)))
 */