[Haskell-cafe] A question on existential types and Church encoding
dan.doel at gmail.com
Tue Jun 1 17:21:35 EDT 2010
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. ...)
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
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 :: * -> *.
More information about the Haskell-Cafe