[Haskell-cafe] Data structure containing elements which are instances of the same type class

[wren ng thornton]

On 8/13/12 9:25 PM, Jay Sulzberger wrote:
> I did suspect that, in some sense, "constraints" in combination
> with "forall" could give the quantifier "exists".

It's even easier than that.

     (forall a. P(a)) -> Q  <=>  exists a. (P(a) -> Q)

Where P and Q are metatheoretic/schematic variables. This is just the 
usual thing about antecedents being in a "negative" position, and thus 
flipping as you move into/out of that position.

The duality mentioned previously is just for the case where you don't 
have that handy "-> Q" there. How do we get the universal quantifier 
into a negative position when there's no implication? Why, we add an 
implication, of course. Even better, add two.

-- 
Live well,
~wren