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