Lambda calculus interlude

adts.hs

-- Lazy System F (lazy as in -- I am too lazy to specify all the boring bits)

--- boolean (this is a popular implementation in lambda calculus)

Bool = ∀x. x -> x -> x

true : Bool
true = λt f. t

false : Bool
false = λt f. f

--- color channel

RgbChannel = ∀x. x -> x -> x -> x

red : RgbChannel
red = λr g b. r

green : RgbChannel
green = λr g b. g

blue : RgbChannel
blue = λr g b. b

--- maybe  (now we need a type parameter) 

Maybe = ∀a. ∀x. x -> (a -> x) -> x

nothing :  ∀a. Maybe a
nothing = λn j. n

just :  ∀a. a -> Maybe a
just = λa. λn j. j a

--- lists  (now we need self-reference!)

List = ∀a. ∀x. x -> (a -> x -> x) -> x

nil :  ∀a. List a
nil = λinit step. n

cons :  ∀a. a -> List a -> List a
cons = λhead tail. λinit step. step head (tail init step)