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

[Tillmann Rendel]

Hi,

to understand forall and exists in types, I find it helpful to look at 
the terms which have such types.

Joshua Ball wrote:
> 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]

So mapInt could be defined with a upper-case lambda /\ which takes a type:

   mapInt = /\a -> ...

Of course, in Haskell, we don't have that lambda explicitly.

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

Not quite. It is the /\ which is like \, except that \ takes a value, 
while /\ takes a type. Now, the type of

   /\ ...    is   forall ...,

and the type of

   \ ...     is   ... -> ... .

Therefore, forall is similar to ->. And indeed, both forall and -> 
describe terms which take arguments.

However, there are two differences between -> and forall. First, a term 
described by -> takes a value argument, while a term described by forall 
takes a type argument. And second, the result type of a term described 
by -> is independent from the argument taken, while the result type of a 
term described by forall may depend on the argument taken.

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

This mapInt could be defined with a version of the pair constructor (,) 
which accepts a type in the first component.

   mapInt = (SomeType, ...)

Note that the ... in that definition need to have the following type:

   (Int -> SomeType) -> [Int] -> SomeType

So exists is similar to (,). Both exists and (,) describe terms which 
represent pairs.

And again, there are two differences between (,) and exists. First, a 
term described by (,) represents a pair of two values, while a term 
described by exists represents a pair of a type and a value. And second, 
the type of the second component of a term described by (,) is 
independent of the first component, while the type of the second 
component of a term described by exists may depend on the first component.

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

If foo has an universal type, the caller of foo can choose a type to be 
used by foo's body by instantiating the type variable. That type 
variable is available to foo's body.

If foo has an existential type, the body of foo can choose a type to be 
available to the caller of foo by creating an existential pair. That 
type is available to foo's caller by unpacking the existential pair, for 
example, by pattern matching.

> 2. If type instantiation of a universally quantified variable is
> beta-reduction, what happens when existentially quantified variables
> are [insert answer to question 1]?

beta-reduction happens when the type application meets the lambda 
abstraction:

   (/\ a -> b) [T]   ~>   b [a := T]

The corresponding reduction for existentials happens when the unpacking 
meets the construction of the existential pair.

   case (T, t) of (a, x) -> b   ~>   b [a := T; x := t]

I don't know how it is called.

BTW, note how the type variable a is bound in the pattern of the case 
expression, so it scopes over b. But the type of b is also the type of 
the overall case expression. Therefore, if the type of b would mention 
the type variable a, so would the overall type of the case expression, 
and then, the type variable a would be used out of scope. This is why 
GHC complains about "escaping type variables" sometimes.

> 3. Is there any analogue to existential quantifiers in the value
> world? "Forall" is to "lambda" as "exists" is to what?

Forall is to lambda as exists is to (,), as discussed above.

HTH,
   Tillmann