Closures and universal quantification

Question

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[({type f[x] = A => x})#f,
                      ({type f[x] = B => x})#f]#Apply, Id] {
    def apply[C](f: A => B => C) = f(a)(b)
  }

For lists, I was able to 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)))

Cowberry

Here's one take on Church numerals in Scala: jim-mcbeath.blogspot.com/2008/11/… – Lure

Randall: Those are type-level church numerals. What I'm doing is not at the level of types. – Cowberry

For what it's worth, Scala methods effectively give you rank n types. – Rudder

Scala methods do not effectively give you rank-n types, but you can encode a great deal of rank-n types that way. – Cowberry

Answer 1

Thanks to Mark Harrah for completing this solution. The trick is that Function1 in the standard libraries is not defined in a general enough way.

My "Closure" trait in the question is actually a natural transformation between functors. This is a generalization of the concept of "function".

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

A function a -> b then ought to be a specialization of this trait, a natural transformation between two endofunctors on the category of Scala types.

trait Const[A] { type Apply[B] = A }
type ->:[A,B] = Const[A]#Apply ~>: Const[B]#Apply

Const[A] is a functor that maps every type to A.

And here's our list type:

type CList[A] = ({type f[x] = Fold[A,x]})#f ~> Endo

Here, Endo is just an alias for the type of functions that map a type onto itself (an endofunction).

type Endo[A] = A ->: A

And Fold is the type of functions that can fold a list:

type Fold[A,B] = A ->: Endo[B]

And then finally, here are our list constructors:

def cons[A](x: A) = {
  new (CList[A] ->: CList[A]) {
    def apply[C](xs: CList[A]) = new CList[A] {
      def apply[B](f: Fold[A,B]) = (b: B) => f(x)(xs(f)(b))
    }
  }
}

def nil[A] = new CList[A] {
  def apply[B](f: Fold[A,B]) = (b: B) => b
}

One caveat is the need to explicitly convert (A ->: B) to (A => B) to help Scala's type system along. So it's still terribly verbose and tedious to actually fold a list once created. Here's the equivalent Haskell for comparison:

nil p z = z
cons x xs p z = p x (xs p z)

List construction and folding in the Haskell version is terse and noise-free:

let xs = cons 1 (cons 2 (cons 3 nil)) in xs (+) 0

Cowberry

This is so out of my comfort zone! – Prehensile