Numbers

gistfile1.txt

  type NUM[A] = (A => A) => A => A
  def succ  [A]:  NUM[A]  =>  NUM[A] = m => n => x => n(m(n)(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)
  def isZero[A]: (NUM[A]) => BOOL[A] = m => a => b => m(_ => F[A](a)(b))(T[A](a)(b))
  //
  /*
  pred ≡ λn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)
  SHIT: http://okmij.org/ftp/Computation/lambda-calc.html#predecessor
  http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=70E6927502DB038ABB1DF6AD0390312F?doi=10.1.1.26.7908&rep=rep1&type=pdf
  page 6
  */
  def pred  [A]: (NUM[A]) => NUM[A] = {
    n => f => x => n( (g:A) => (h:A) => h(g(f(x))))((u:A) => x)((u:A) => u)
    ???
  }

// crazy shit over here... trying different "simplifications"
  def numPair0[A]: NUM[A] => PAIR[NUM[A]] = m => pair(m)(m)
  def numPair1[A]: (NUM[A]) => (NUM[A]) => PAIR[NUM[A]] = m => n => pair(m)(n)
  def numPair2[A]: NUM[A] => (NUM[PAIR[A]]) = n => f => x => {
    val sp: PAIR[NUM[A]] => PAIR[NUM[A]] = p => pair(snd(p))(succ(snd(p)))
    val ps: (NUM[PAIR[A]]) => NUM[PAIR[A]] = n => f => x => n( p => pair(snd(p))(snd(p)) )(x)

    def three [A]: NUM[A] = f => x => f(f(f(x)))

    ???
  }
  def numPair3[A]: NUM[A] => PAIR[NUM[A]] = m => f => x => ???