Closures and universal quantification

Posted by Apocalisp on Stack Overflow See other posts from Stack Overflow or by Apocalisp
Published on 2010-04-08T17:56:33Z Indexed on 2010/04/09 18:03 UTC
Read the original article Hit count: 274

I've been trying to work out how to implement Church-encoded data types in Scala. It seems that it requires rank-n types since you would need a first-class const function of type forAll a. a -> (forAll b. b -> b).

However, I was able to encode pairs thusly:

import scalaz._

trait Compose[F[_],G[_]] { type Apply = F[G[A]] }

trait Closure[F[_],G[_]] { def apply[B](f: F[B]): G[B] }

def pair[A,B](a: A, b: B) =
  new Closure[Compose[PartialApply1Of2[Function1,A]#Apply,
                      PartialApply1Of2[Function1,B]#Apply]#Apply, Identity] {
    def apply[C](f: A => B => C) = f(a)(b)
  }

For lists, I was able to get encode cons:

def cons[A](x: A) = {
  type T[B] = B => (A => B => B) => B
  new Closure[T,T] {
    def apply[B](xs: T[B]) = (b: B) => (f: A => B => B) => f(x)(xs(b)(f))
  }
}

However, the empty list is more problematic and I've not been able to get the Scala compiler to unify the types.

Can you define nil, so that, given the definition above, the following compiles?

cons(1)(cons(2)(cons(3)(nil)))

© Stack Overflow or respective owner

Related posts about scala

Related posts about quantifiers