Scalaで足し算する（ただし型レベルで）のコード例

BoolDemo.scala

import scala.language.higherKinds

object BoolDemo extends App {

  trait Bool {
    type Not <: Bool
    type And[A <: Bool] <: Bool
    type Or[A <: Bool] <: Bool
  }

  trait True extends Bool {
    type Not = False
    type And[A <: Bool] = A
    type Or[A <: Bool] = True
  }

  trait False extends Bool {
    type Not = True
    type And[A <: Bool] = False
    type Or[A <: Bool] = A
  }

  object Bools {
    type ![A <: Bool] = A#Not
    type &&[A <: Bool, B <: Bool] = A#And[B]
    type ||[A <: Bool, B <: Bool] = A#Or[B]
  }

  import Bools._

  trait ToBool[A <: Bool] {
    def apply(): Boolean
  }

  def toBool[A <: Bool](implicit f: ToBool[A]) = f()

  implicit val toTrue = new ToBool[True] {
    def apply() = true
  }

  implicit val toFalse = new ToBool[False] {
    def apply() = false
  }

  assert(toBool[True] == true)
  assert(toBool[False] == false)

  assert(toBool[![True]] == false)
  assert(toBool[![False]] == true)
  assert(toBool[![![True]]] == true)

  assert(toBool[True && True] == true)
  assert(toBool[True && False] == false)
  assert(toBool[False && True] == false)
  assert(toBool[False && False] == false)

  assert(toBool[True || True] == true)
  assert(toBool[True || False] == true)
  assert(toBool[False || True] == true)
  assert(toBool[False || False] == false)
}

NatDemo.scala

import scala.language.higherKinds

object NatDemo extends App {

  trait Nat {
    type Inc <: Nat
    type Add[A <: Nat] <: Nat
  }

  trait _0 extends Nat {
    type Inc = Suc[_0]
    type Add[A <: Nat] = A
  }

  trait Suc[A <: Nat] extends Nat {
    type Inc = Suc[Suc[A]]
    type Add[B <: Nat] = A#Add[B#Inc]
  }

  type _1 = Suc[_0]
  type _2 = Suc[_1]
  type _3 = Suc[_2]

  object Nats {
    type ++[A <: Nat] = A#Inc
    type +[A <: Nat, B <: Nat] = A#Add[B]
  }

  import Nats._

  trait ToInt[A <: Nat] {
    def apply(): Int
  }

  def toInt[A <: Nat](implicit f: ToInt[A]) = f()

  implicit val toZero = new ToInt[_0] {
    def apply() = 0
  }

  implicit def toSuc[A <: Nat](implicit f: ToInt[A]) = new ToInt[Suc[A]] {
    def apply() = 1 + f()
  }

  assert(toInt[_0] == 0)
  assert(toInt[_1] == 1)
  assert(toInt[_2] == 2)
  assert(toInt[_3] == 3)
  assert(toInt[Suc[_3]] == 4)

  assert(toInt[++[_0]] == 1)
  assert(toInt[++[_1]] == 2)
  assert(toInt[++[_2]] == 3)
  
  assert(toInt[_0 + _1] == 1)
  assert(toInt[_3 + _2] == 5)
  assert(toInt[_1 + _2 + _3] == 6)
}

スライドはこちら。

• https://backpaper0.github.io/ghosts/type-level-addition/#1