[Haskell-cafe] A question on existential types and Church encoding

[Dan Doel]

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