church.scala

// rank 1

type num[a] = (a => a) => a => a

def zero[a]: num[a] = f => x => x
def succ[a](n: num[a]): num[a] = f => x => f(n(f)(x))

def eval(n: num[Int]): Int = n(_ + 1)(0)

// rank 2

trait forall[m[_]] {
  def apply[a]: m[a]
}

val zeroR2: forall[num] = new forall[num] {
  def apply[a] = zero[a]
}

def succR2(x: forall[num]): forall[num] = new forall[num] {
  def apply[a] = succ(x.apply[a])
}

def pred(n: forall[num]): forall[num] = new forall[num] {
  def apply[a] = f => x => n.apply[(a=>a)=>a](g => h => h(g(f)))(u => x)(u => u)
}

def evalR2(n: forall[num]) =
  eval(n.apply)