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