The existential is a pair where one component is a type, and the type of the
second component depends on the value (i.e., which type went in the first
component) of the first. It's often called a sigma type when you have full
dependent types.
So your exists a. (Int -> a) -> [Int] -> [a] type might hypothetically be
represented as (assuming you write an instance for Bool):
(*, (\a -> (Int -> a) -> [Int] -> [a])) -- the type, where * is the kind of
types
(Bool,
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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe