even nlist

gistfile1.scala

package nlist
           
sealed trait Even[A <: Nat]

object Even {
  implicit def isEven[A <: Nat](implicit e: A#IsEven =:= True): Even[A] =
    new Even[A]{}
}

sealed trait Bool {
  type Not <: Bool
}

sealed trait True extends Bool {
  type Not = False
}

sealed trait False extends Bool {
  type Not = True
}

sealed trait Nat {
  type IsEven <: Bool
  type Pred <: Nat
}

sealed trait Z extends Nat {
  type IsEven = True
  type Pred = Z
}

sealed trait S[A <: Nat] extends Nat {
  type IsEven = A#IsEven#Not
  type Pred = A
}

sealed trait NList[A <: Nat, +B] {
  type Length = A

  def zap[C](l: NList[Length, B => C]): NList[Length, C]
  def getPairs(implicit e: Even[Length]): List[(B, B)]

  def head: B
  def tail: NList[Length#Pred, B]
}

case object NNil extends NList[Z, Nothing] {
  def zap[A](l: NList[Length, Nothing => A]): NNil.type = 
    NNil

  def getPairs(implicit e: Even[Length]): List[(Nothing, Nothing)] = Nil

  def head = sys.error("empty list")
  def tail = sys.error("empty list")
}

sealed case class NCons[A <: Nat, B](h: B, t: NList[A, B])
extends NList[S[A], B] {

  def zap[C](l: NList[Length, B => C]): NList[Length, C] = 
    l match {
      case NCons(f, fs) => 
        NCons(f(head), tail zap fs)
    }

  private def predPredEven[A](e: Even[Length]): Even[Length#Pred#Pred] =
    new Even[Length#Pred#Pred]{}

  def getPairs(implicit e: Even[Length]): List[(B, B)] =
    (head, tail.head) :: tail.tail.getPairs(predPredEven(e))
  
  def head: B = h
  def tail: NList[Length#Pred, B] = t
}