[Haskell-cafe] A question on existential types and Church encoding

[Dan Doel]

On Sunday 30 May 2010 12:28:36 am Cory Knapp wrote:
> >type CB a = a -> a -> a
> >
> >ct :: CB aC
> >ct x y = x
> >
> >cf :: CB a
> >cf x y = y
> >
> >cand :: CB (CB a) -> CB a -> CB a
> >cand p q = p q cf
> >
> >cor :: CB (CB a) -> CB a -> CB a
> >cor p q = p ct q

The reason these types are required is that the 'a' in your Church booleans is 
the result type. So, if you want to inspect a boolean and produce an 'a', you 
need a 'CB a', and notably, you have the result type tied to the boolean type. 
So 'CB a' isn't just a boolean, it's a boolean that only allows you to choose 
between two 'a' values.

This explains why you need to double up for your current definitions. To 
choose between two booleans (which will in turn allow you to choose between 
'a's), you need a CB (CB a). You can eliminate the asymmetric type, though, 
like so:

  cand :: CB a -> CB a -> CB a
  cand p q t f = p (q t f) f

You can probably always do this, but it will become more tedious the more 
complex your functions get.

> >type CB a = forall a . a -> a -> a

Note: this is universal quantification, not existential.

> >ctrue :: CB a
> >ctrue x y = x
> >
> >cfalse :: CB a
> >cfalse x y = y
> >
> >cand :: CB a -> CB a -> CB a
> >cand p q = p q cfalse
> >
> >cor :: CB a -> CB a -> CB a
> >cor p q = p ctrue q
> 
> which works. But I haven't the faintest idea why that "forall" in the type
> makes things work... I just don't fully understand existential type
> quantification. Could anyone explain to me what's going on that makes the
> second code work?

In the new type, the parameter 'a' is misleading. It has no connection to the 
'a's on the right of the equals sign. You might as well write:

  type CB = forall a. a -> a -> a

And now, hopefully, a key difference can be seen: we no longer have the result 
type for case analysis as a parameter of the type. Rather, they must work 'for 
all' result types, and we can choose which result type to use when we need to 
eliminate them (and you can choose multiple times when using the same boolean 
value in multiple places).

One may think about explicit typing and type abstraction. Suppose we have your 
first type of boolean at a particular type T. We'll call said type CBT. Then 
you have:

  CBT = T -> T -> T

and values look like:

  \(t :: T) (f :: T) -> ...

By contrast, values of the second CB type look like this:

  \(a :: *) (t :: a) (f :: a) -> ...

so the values accept a type (the result type) as a parameter. When you go to 
write combinators:

  cand :: CBT -> CBT -> CBT
  cand p q = p q false

This fails because p expects Ts, and q and false are not Ts, they are CBTs (so 
you need p to be a CBCBT :)).

By contrast, with the second type, we write:

  cand :: CB -> CB -> CB
  cand p q = p CB q false

where the first argument specifies what we want to produce. In GHC, types are 
not passed explicitly like this, but it's the sort of thing that's going on 
behind the scenes. And 'CB a' isn't restricted to just some program-wide 
choice of T, but from the perspective of cand and the like, 'a' is just some 
opaque variable it didn't get to choose, so it's in the same boat as if it 
were some fixed T. If we think about explicit type passing:

  cand (T :: *) (p :: CB T) (q :: CB T) = ...

cand gets told what T is; it doesn't get to choose.

Hopefully I didn't make that too over-complicated, and you can glean something 
useful from it. It turned out a bit longer than I expected.

Cheers,
-- Dan