On 13/09/2007, at 0:06, Don Stewart wrote:
ok:
In Monad.Reader 8, Conrad Parker shows how to solve the Instant
Insanity
puzzle in the "Haskell" type system. Along the way he
demonstrates very
clearly something that was implicit in Mark Jones' "Type Classes with
Functional Dependencies" paper if you read it very very carefully
(which
I hadn't, but on re-reading it is there). That is, Haskell types
plus
multiparameter type classes plus functional dependencies is a logic
programming language. In fact it is a sufficiently powerful
language to
emulate any Turing machine calculation as a type checking problem.
So we have
C++ : imperative language whose type system is a Turing-complete
functional language (with rather twisted syntax)
Haskell: functional language whose type system is a Turing-
complete logic programming language (with rather twisted
syntax)
Since not all Turing machines halt, and since the halting problem is
undecidable, this means not only that some Haskell programs will make
the type checker loop forever, but that there is no possible meta-
checker that could warn us when that would happen.
I've been told that functional dependencies are old hat and there is
now something better. I suspect that "better" here means "worse".
Better here means "better" -- a functional language on the type
system,
to type a functional language on the value level.
-- Don
For a taste, see Instant Insanity transliterated in this functional
language:
http://hpaste.org/2689
NB: it took me 5 minutes, and that was my first piece of coding ever
with Type families
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
