church-encoding.groovy

// Church Encoding in Groovy
// Translated from http://meta-meta.blogspot.com/2007/06/church-code.html
def partial(c) {
  return { a -> { b -> c(a,b) } }
}

T = partial { a,b -> a }
F = partial { a,b -> b }

def toBool(f) {
  f(true)(false)
}
cand = partial { a,b -> a(b)(a) }
cor = partial { a,b -> a(a)(b) } 

def TT(fn) {
  [[F,F],[F,T],[T,F],[T,T]].collect { it ->
      toBool( fn(it[0])(it[1]) ) 
  }
}

// print truth tables to verify
println "     \tFF\tFT\tTF\tTT"
println "cand:\t" + TT(cand).join("\t")
println "cor: \t" + TT(cor).join("\t")

pair = partial { a,b -> { p -> p(a)(b) } }

cfst = { pair -> pair(T) }
csnd = { pair -> pair(F) }

def toNum(f) {
  f({ it + 1 })(0)
}

zero = partial { f,x -> x }
succ = { s -> partial { f,x -> f(s(f)(x)) } }

one = succ(zero)
two = succ(one)
three = succ(two)

plus = partial { a,b -> partial { f,x -> a(f)(b(f)(x)) } }

def toChurchNum(i, num = zero) {
   if(i <= 0) return num
   
   return toChurchNum(i-1,succ(num))
}

just = { v -> partial { f, x -> f(v) } }
nothing = partial { f,x-> x } // F

left = { v -> partial { f,g -> f(v) } }
right = { v -> partial { f,g -> g(v) } }

cons = partial { h,t-> partial { cf,ev-> cf(h)(t) } }
empty = partial { cf, ev -> ev } // F

car = { it(T)(null) } // first
cdr = { it(F)(null) } // rest

map = partial { f,l -> l( partial { h,t-> cons(f(h))(map(f)(t)) })(empty) }

list = cons(one)(cons(two)(cons(three)(empty)))

toNum(car(map({plus(it)(two)})(list))) // 3