[Haskell-cafe] universal quantification is to type instantiations as existential quantification is to what

[Daniel Peebles]

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 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100812/370996ac/attachment.html