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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
