
On Tuesday 01 June 2010 3:40:41 pm Cory Knapp wrote:
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?
There is no first-class exists in GHC. If there were, it would work about the same as forall, like: foo :: (exists a. P a) -> T or what have you. There's potentially a little more of interest with how you make and take apart things with existential types, but that's about it. There are papers out there on type systems with this, and the UHC Haskell compiler has it, although it doesn't let you use it in conjunction with type classes, but I think SPJ is on record as saying it would add a lot of complexity to the current GHC type system, and I'm inclined to believe him. So, instead, GHC allows you to do existential quantification around data constructors, and somewhat confusingly, it uses the forall keyword. The idea behind this is that the type of such a constructor would be: C :: (exists a. ...) -> T which is isomorphic to: C :: forall a. ... -> T So, if you're using GADT syntax, that's exactly what you write: data T where C :: forall a. ... -> T but, if you're using normal-ish data syntax, instead of writing: data T = C (exists a. ...) you write: data T = forall a. C (...) which is supposed to suggest that C has the isomorphic type in question, but I think it just tends to confuse people who are new to this, especially since holding a universal inside a datatype looks like: data U = C (forall a. ...) and removing the constructors to attempt to make it a type alias makes them look identical: type T = forall a. ... type U = forall a. ... But the alias T here is not the same as the data type T above. To make them (roughly) the same, you'd need: type T = exists a. ... But I digress.
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" )?
(forall a. a -> a -> a) should type only booleans, with some caveats. The forall enforces parametricity, which means the only normal lambda terms you can write with that type are: \x y -> x \x y -> y In Haskell, you can also write stuff like: \x -> undefined \x y -> x `seq` y The first of which is arguably a boolean, if you consider _|_ to be one in Haskell (although the Church encoding contains several distinguishable bottoms, due to seq), but the second is weird. It's false, except it blows up if the true case is undefined. But if you ignore these weird corner cases (or have a language that doesn't allow them), then you get exactly the booleans.
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. :)
By contrast to the above, I said that 'CB a' is a boolean that can be used to choose between 'a' values. However, you can construct non-booleans for special cases of this type. For instance: add :: CB Int add x y = x + y This is clearly not a boolean, but it inhabits CB Int. So, the only way you can be (reasonably) sure that v :: CB T is a boolean choice between Ts is if you got it by specializing something with the type (forall a. CB a), since that is exactly the type above that contains only boolean expressions (and the weird corner cases).
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 :: *->*) ?
* is the kind of types. So, for instance: Int :: * [Int] :: * Int -> Int :: * * -> * is the kind of functions from types to types, and so on, so: Maybe :: * -> * Either :: * -> * -> * (->) :: * -> * -> * So, in particular, if T :: * -> *, then T -> T is ill-kinded, because each side of (->) expects a *, but you're trying to give it a * -> *. Hence, CB T won't work if T :: * -> *. Cheers, -- Dan