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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
