Andrew Coppin wrote:
In my book, if it's difficult to explain what a feature even *does*, you have to wonder if that feature is really necessary...
Well, difficulty is in the eye of the beholder. For the one familiar with formal logic, ∀ and ∃ are as basic as apples and eggplants. Nobody can stop you to become familiar as well.
GADTs (um... why?)
GADTs are awesome. They're the basic tool to derive data structures from their specification and they bring dependent types in reach. http://haskell.org/haskellwiki/GADT R. Hinze. Fun with Phantom Types. http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf K. Claessen. Parallel Parsing Processes. http://www.cs.chalmers.se/~koen/pubs/entry-jfp04-parser.html (This paper is not about GADTs but about deriving data structures from their specification)
rank-N polymorphism (er... what?)
Actually, rank-N polymorphism came first and has been cut down to form the basis of Haskell. You may want to look for "System F", perhaps in the book Girard, Lafont, Taylor. Proofs and Types. http://www.cs.man.ac.uk/~pt/stable/prot.pdf
MPTC, functional dependencies
Mark P. Jones. Type Classes with Functional Dependencies. http://web.cecs.pdx.edu/~mpj/pubs/fundeps.html Regards, apfelmus