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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
