Closures and universal quantification
- by Apocalisp
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)))
