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