Church

Church.scala

package fpis

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

  /*
  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)

  println(t2,t3,t4,t5,t6,t7,t8)

  /*
  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
   */

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

  def T[A]:A => A => A = a => b => a
  def F[A]:A => A => A = a => b => b

  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)


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

  T(true)(false)

  def bool: (BOOL[Boolean]) => Boolean = a =>  a(true)(false)

  def values[A] = List(T[A],F[A])
  def tfs[A] = (for{ l <- values[A]; r <- values[A] } yield (l,r))
  
  println(values[Boolean] map { x => (bool(x) , bool(not(x))) } mkString("NOT: ", ",", "."))

  println("---AND---")
  println(tfs[Boolean] map { case (x,y) => ( (bool(x) + " AND " +bool(y)) , bool(and(x)(y))) } mkString("AND:\n", ",\n", "."))

  println("---OR---")
  println(tfs[Boolean] map { case (x,y) => ( (bool(x) + " OR " +bool(y)) , bool(or(x)(y))) } mkString("OR:\n", ",\n", "."))

  /*
  pair ≡ λx.λy.λz.z x y
  fst ≡ λp.p (λx.λy.x)
  snd ≡ λp.p (λx.λy.y)
   */

  def pair[A]: A=>A=>(A=>A=>A)=>A = x => y => z => z(x)(y)

  val p1 = pair[Int](1)(2)
  val p2 = pair(3)(4)

  def fstr[A]: A => A => A = T[A]
  def sndr[A]: A => A => A = F[A]

  println("---PAIRS---")
    println("p1:"+ ( p1(fstr), p1(sndr) ))
    println("p2:"+ ( p2(fstr), p2(sndr) ))


  def fst[A]: ((A => A => A) => A) => A = z => z(T[A])
  def snd[A]: ((A => A => A) => A) => A = z => z(F[A])
  println("p1:"+ ( fst(p1), snd(p1) ))
  println("p2:"+ ( fst(p2), snd(p2) ))


  //or[Boolean](and[Boolean](F)(F))(T)(true)(false)
    //def succ [A](n:(A => A) => A, f:A => A, x:A) = f(n(f(x)))



}