[Haskell-cafe] A question on existential types and Church
cory.m.knapp at gmail.com
Tue Jun 1 15:40:41 EDT 2010
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
> '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
> type for case analysis as a parameter of the type. Rather, they must work
> all' result types, and we can choose which result type to use when we need
> eliminate them (and you can choose multiple times when using the same
> value in multiple places).
> One may think about explicit typing and type abstraction. Suppose we have
> first type of boolean at a particular type T. We'll call said type CBT.
> 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) -> ...
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
> useful from it. It turned out a bit longer than I expected.
> It was very helpful, thanks!
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe