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

[Cory Knapp]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100601/620dc5ea/attachment.html