On Thu, Aug 16, 2012 at 8:07 PM, wren ng thornton <w...@freegeek.org> wrote:
> On 8/15/12 2:55 PM, Albert Y. C. Lai wrote: > >> On 12-08-15 03:20 AM, wren ng thornton wrote: >> >>> (forall a. P(a)) -> Q <=> exists a. (P(a) -> Q) >>> >> >> For example: >> >> A. (forall p. p drinks) -> (everyone drinks) >> B. exists p. ((p drinks) -> (everyone drinks)) >> >> In a recent poll, 100% of respondents think A true, 90% of them think B >> paradoxical, and 40% of them have not heard of the Smullyan drinking >> paradox. >> > > :) > > Though bear in mind we're discussing second-order quantification here, not > first-order. Can you expand on what you mean here? I don't see two kinds of quantification in the type language (at least, reflexively, in the context of what we're discussing). In particular, I don't see how to quantify over predicates for (or sets of, via the extensions of the predicates) types. Is Haskell's 'forall' doing double duty?
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
