On 27/05/07, Andrew Coppin
So... ∀x . P means that P holds for *all* x, and ∃ x . P means that x holds for *some* x? (More precisely, at least 1 possible choice of x.)
Exactly. There's also a lesser-used "there exists a unique", typically written ∃!x. P, which means that P is true for one, and only one, value of x. For some examples of how these "quantifiers" are used: ∀x in R. x^2 >= 0 (real numbers have a nonnegative square) ∃x in N. x < 3 (there is at least one natural number less than 3) ∃!x in N. x < 1 (there is only a single natural number less than 1) For the LaTeX versions, http://www.mathbin.net/11020.
Erm... oh...kay... That kind of makes *slightly* more sense now...
I wrote most of the second article, I'd appreciate any feedback you have on it.
Seriously. Haskell seems to attract weird and wonderful type system extensions like a 4 Tesla magnet attracts iron nails... And most of these extensions seem to serve no useful purpose, as far as I can determine. And yet, all nontrivial Haskell programs *require* the use of at least 3 language extensions. It's as if everyone thinks that Haskell 98 sucks so much that it can't be used for any useful programs. This makes me very sad. I think Haskell 98 is a wonderful language, and it's the language I use for almost all my stuff. I don't understand why people keep trying to take this small, simple, clean, elegant language and bolt huge, highly complex and mostly incomprehensible type system extensions onto it...
Ever tried writing a nontrivial Haskell program? Like you said, they require these type system extensions! :) Obviously they don't "require" them, Haskell 98 is a Turing-complete language, but they're useful to avoid things like code-reuse and coupling. One of Haskell's design aims is to act as a laboratory for type theory research, which is one of the reasons why there are so many cool features to Haskell's type system. Anyway, existential types (and higher-rank polymorphism), along with multi-parameter type classes, some kind of resolution to the "MPTC dliemma" -- so functional dependencies or associated types or something similar -- and perhaps GADTs are really the only large type system extensions likely to make it into Haskell-prime. They're really more part of the Haskell language than extensions now, so well-used are they. -- -David House, dmhouse@gmail.com