Type Level programming

gistfile1.scala

// 
// From https://www.parleys.com/tutorial/type-level-programming-scala-101
//

import scala.language.higherKinds

// Int type programming level

sealed trait IntType {
  type plus[that <: IntType] <: IntType
}

sealed trait Int0 extends IntType {
  override type plus[that <: IntType] = that
}

sealed trait IntN[Prev <: IntType] extends IntType {
  override type plus[that <: IntType] = IntN[Prev#plus[that]]
}

//
// List implementation with list type programming level
//

sealed trait IntList[Size <: IntType] {
  def ::(head:Int):IntList[IntN[Size]] = IntListImp(head,this)
  def ++[ThatSize <: IntType](that:IntList[ThatSize]):IntList[Size#plus[ThatSize]]
}

case object IntNil extends IntList[Int0] {
  override def ++[ThatSize <: IntType](that:IntList[ThatSize]) = that
}

case class IntListImp[TailSize <: IntType](head:Int,tail:IntList[TailSize]) extends IntList[IntN[TailSize]] {
  override def ++[ThatSize <: IntType](that:IntList[ThatSize]) = IntListImp(head,tail++that)
}

//
// Some example
//

object main {
  type Int1 = IntN[Int0]
  type Int2 = Int1#plus[Int1]
  type Int3 = Int2#plus[Int1]

  val l1:IntList[Int3] = (1 :: 2 :: 3 :: IntNil)
  val l2:IntList[Int2] = (5 :: 6 :: IntNil)
  val l3:IntList[Int3#plus[Int2]] = l1 ++ l2
}