Church encodings in Scala value level. Unfinished.I am not sure 'and' and 'or' could be better.

Church.scala

package fpis

/**
 * User: pedrofurla
 * Date: 11/09/13
 * Time: 08:17
 */
object Church {

  /*
  0 ≡ λf.λx. x
  1 ≡ λf.λx. f x
  2 ≡ λf.λx. f (f x)
  3 ≡ λf.λx. f (f (f x))

  succ ≡ λn.λf.λx. f (n f x)

  succ 1 ≡ λf.λx. f ( (λf.λx. f x) f x) ≡ λf.λx. f (f x) )

  plus ≡ λm.λn.λf.λx. m f (n f x)
  */

  def I[A]:A => A = x => x
  def K[A,B]: A => B => A =  x => y => x

  type  F[A,B] = (A => B) => A => B

  def zerod [A](f:A => A,x:A) = x     // A => A => A
  def oned  [A](f:A => A,x:A) = f(x)
  def twod  [A](f:A => A,x:A) = f(f(x))
  def threed[A](f:A => A,x:A) = f(f(x))


  type NUM[A] = (A => A) => A => A

  def zero  [A]: NUM[A] = f => x => x
  def one   [A]: NUM[A] = f => x => f(x)
  def two   [A]: NUM[A] = f => x => f(f(x))
  def three [A]: NUM[A] = f => x => f(f(f(x)))
  def succ  [A]: NUM[A] => NUM[A] = n => f => x => f(n(f)(x))

  def plus  [A]: (NUM[A]) => (NUM[A]) => NUM[A] = m => n => f => x => m(f)(n(f)(x))
  def times [A]: (NUM[A]) => (NUM[A]) => NUM[A] = m => n => f => x => m(n(f))(x)

  val inc: Int => Int  = _ + 1
  def four[A] = succ[A](three)

  def five  [A] = plus[A](four)(one)
  def six   [A] = plus[A](two)(four)
  def seven [A] = plus[A](one)(six)
  def eight [A] = times[A](two)(four)

  val t2=two(inc)(0)
  val t3=three(inc)(0)
  val t4=four(inc)(0)
  val t5=five(inc)(0)
  val t6=six(inc)(0)
  val t7=seven(inc)(0)
  val t8=eight(inc)(0)

  type BOOL[A] = A => A => A

  def T[A]:A => A => A = a => b => a
  def F[A]:A => A => A = a => b => b
  /*
  true ≡ λa.λb. a
  false ≡ λa.λb. b

  and ≡ λm.λn. m n m
  or ≡ λm.λn. m m n
  not1[1] ≡ λm.λa.λb. m b a
  not2[2] ≡ λm. m (λa.λb. b) (λa.λb. a)
  xor ≡ λa.λb. a (not2 b) b
  if ≡ λm.λa.λb. m a b

  and true false ≡ (λm.λn. m n m) (λa.λb. a) (λa.λb. b) ≡ (λa.λb. a) (λa.λb. b) (λa.λb. a) ≡ (λa.λb. b) ≡ false
  and true true  ≡ (λm.λn. m n m) (λa.λb. a) (λa.λb. a) ≡ (λa.λb. a) (λa.λb. a) (λa.λb. a) ≡ (λa.λb. a) ≡ false

   */

  def lif[A]: (A => A => A) => A => A => A = m => a => b => m(a)(b)
  def not[A]: (A => A => A) => A => A => A = m => a => b => m(b)(a)
  def and[A]: BOOL[BOOL[A]] => BOOL[A] => BOOL[A] = m => n => m(n)(F)
  def or [A]: BOOL[BOOL[A]] => BOOL[A] => BOOL[A] = m => n => m(T)(n)


  not[Boolean](T)(true)(false)

  not[Boolean](F)(true)(false)
 println("------")
  and[Boolean](T)(T)(true)(false)
  and[Boolean](F)(T)(true)(false)
  and[Boolean](T)(F)(true)(false)
  and[Boolean](F)(F)(true)(false)
 println("------")

  or[Boolean](T)(T)(true)(false)
  or[Boolean](F)(T)(true)(false)
  or[Boolean](T)(F)(true)(false)
  or[Boolean](F)(F)(true)(false)

    //def succ [A](n:(A => A) => A, f:A => A, x:A) = f(n(f(x)))



}