[Haskell-cafe] universal quantification is to type instantiations
as existential quantification is to what
rendel at Mathematik.Uni-Marburg.de
Thu Aug 12 15:12:03 EDT 2010
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
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
(/\ 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.
More information about the Haskell-Cafe