Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
even nlist
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
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment