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 <scioli...@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 >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
