[Haskell-cafe] universal quantification is to type instantiations
as existential quantification is to what
wren ng thornton
wren at freegeek.org
Thu Aug 12 20:14:27 EDT 2010
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
More information about the Haskell-Cafe
mailing list