On Sunday 30 May 2010 12:28:36 am Cory Knapp wrote:
type CB a = a -> a -> a
ct :: CB aC ct x y = x
cf :: CB a cf x y = y
cand :: CB (CB a) -> CB a -> CB a cand p q = p q cf
cor :: CB (CB a) -> CB a -> CB a cor p q = p ct q
The reason these types are required is that the 'a' in your Church booleans is the result type. So, if you want to inspect a boolean and produce an 'a', you need a 'CB a', and notably, you have the result type tied to the boolean type. So 'CB a' isn't just a boolean, it's a boolean that only allows you to choose between two 'a' values. 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 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.
ctrue :: CB a ctrue x y = x
cfalse :: CB a cfalse x y = y
cand :: CB a -> CB a -> CB a cand p q = p q cfalse
cor :: CB a -> CB a -> CB a cor p q = p ctrue q
which works. But I haven't the faintest idea why that "forall" in the type makes things work... I just don't fully understand existential type quantification. Could anyone explain to me what's going on that makes the second code work?
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 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) -> ... so the values accept a type (the result type) as a parameter. When you go to write combinators: cand :: CBT -> CBT -> CBT cand p q = p q false This fails because p expects Ts, and q and false are not Ts, they are CBTs (so you need p to be a CBCBT :)). By contrast, with the second type, we write: cand :: CB -> CB -> CB cand p q = p CB q false where the first argument specifies what we want to produce. In GHC, types are not passed explicitly like this, but it's the sort of thing that's going on behind the scenes. And 'CB a' isn't restricted to just some program-wide choice of T, but from the perspective of cand and the like, 'a' is just some opaque variable it didn't get to choose, so it's in the same boat as if it were some fixed T. If we think about explicit type passing: cand (T :: *) (p :: CB T) (q :: CB T) = ... cand gets told what T is; it doesn't get to choose. 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. Cheers, -- Dan