[Haskell-cafe] Monad.Reader 8: Haskell, the new C++

[Don Stewart]

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