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

[Joshua Ball]

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.)

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

My question is... what is the analog to an existential type?

mapInt :: exists a. (Int -> a) -> [Int] -> [a]

(I don't think this is valid syntax either. I understand that I can
rewrite this using foralls and a new type variable, doing something
that looks like double negation, but the point of my question is to
get an intuition for what exactly the universal quantifier means in
the context of function application... if this even makes sense.)

In particular:

1. If I can "instantiate" variables in a universal quantifier, what is
the corresponding word for variables in an existential quantifier?
2. If type instantiation of a universally quantified variable is
beta-reduction, what happens when existentially quantified variables
are [insert answer to question 1]?
3. Is there any analogue to existential quantifiers in the value
world? "Forall" is to "lambda" as "exists" is to what?

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?)

Josh "Ua" Ball