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, <some function of type (Int -> Bool) -> [Int] -> [a]>) You can translate to and from forall and exists by currying, since one is a function and the other is a pair, but not in the form you asked. It'd look a lot more like curry/uncurry in regular haskell :) Hope I wasn't too unclear! Dan On Thu, Aug 12, 2010 at 7:32 PM, Joshua Ball <sciolizer@gmail.com> 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.)
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