[Haskell-cafe] Language extensions [was: Memoization]
David House
dmhouse at gmail.com
Sun May 27 09:47:13 EDT 2007
On 27/05/07, Andrew Coppin <andrewcoppin at btinternet.com> wrote:
> 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 at gmail.com
More information about the Haskell-Cafe
mailing list