Thanks! That was exactly the sort of response I was looking for.

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

Right. When he was working on it, I thought of that, and seemed to have completely forgotten when I reworked it.
 
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.

As I would assume. But I always see the "forall" keyword used when discussing "existential quantification". I don't know if I've ever seen an "exists" keyword. Is there one? How would it be used?
 
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

Ah! That makes sense. Which raises a new question: Is this type "too general"? Are there functiosn which are semantically non-boolean which fit in that type, and would this still be the case with your other suggestion (i.e. "cand p q = p (q t f) f" )?

I guess it wouldn't much matter, since Church encodings are for untyped lambda calculus, but I'm just asking questions that come to mind here. :)
 
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) -> ...

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

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


I'm guessing that * has something to do with kinds, right? This is probably a silly question, but why couldn't we have (T :: *->*) ?

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.

It was very helpful, thanks!

Cory