[Haskell-cafe] universal quantification is to type instantiations as existential quantification is to what

[wren ng thornton]

Joshua Ball wrote:
> Hi,
> 
> If I have a universally quantified type
> 
> mapInt :: forall a. (Int -> a) -> [Int] -> [a]
> 
> I can instantiate that function over a type and get a beta-reduced
> version of the type
> 
> mapInt [String] :: (Int -> String) -> [Int] -> [String]
> 
> (I'm borrowing syntax from Pierce here since I don't think Haskell
> allows me to explicitly pass in a type to a function.)

The standard syntax around here is to use @ for type application. I.e., 
that's what's used in Core.


> This makes sense to me. The universal quantifier is basically a
> lambda, but it works at the type level instead of the value level.

Not quite. In standard Church-style System F it's a lambda at the value 
level, just a different one from the regular lambda. Tillmann Rendel 
covered this.

If you actually have lambdas at the type-level, then it's a higher-order 
language. System F^omega has this, but System F does not.


> My question is... what is the analog to an existential type?
> 
> mapInt :: exists a. (Int -> a) -> [Int] -> [a]

Existentials are a pair of a witness (the particular type A) and the 
thing being quantifier over. E.g., one possible implementation of mapInt is:

     mapInt = Ex A (mapPoly @A)

     where Ex :: forall f. (a :: *) -> (_ :: f a) -> (exists b. f b)

This is just part of the duality between functions and pairs. (Though 
the idea of "pairs" breaks apart once you move to full dependent types 
or various other interesting systems.)


> 1. If I can "instantiate" variables in a universal quantifier, what is
> the corresponding word for variables in an existential quantifier?

The first component of the pair with an existential type is called a 
"witness". Because this first component serves to witness the fact that, 
yes, there does indeed exist such a type; namely this one right here.


> Also (separate question), is the following statement true?
> 
> forall T :: * -> *.   (forall a. T a) -> (exists a. T a)
> 
> If so, what does the implementation look like? (What function inhabits
> it, if it is interpreted as a type?)

No, it's not true. However, this slight variation is true (using (->) 
for forall):

     foo :: (T :: * -> *)
         -> (A :: *)
         -> (x :: (B :: *) -> T B)
         -> Exists T
     foo T A x = Ex A (x @A)

That is, your statement is only true when we can independently prove 
that there is a type. Which type doesn't matter, but we must prove that 
at least one type exists. This is because we can't construct a proof of 
the existential unless we can come up with a witness; for all we know, 
the set being quantified over may be empty, in which case there doesn't 
exist an a such that T a.

-- 
Live well,
~wren