[Haskell-cafe] Data structure containing elements which are instances of the same type class
wren ng thornton
wren at freegeek.org
Wed Aug 15 09:20:16 CEST 2012
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.
More information about the Haskell-Cafe