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

[Stefan Holdermans]

> 	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.

Do not forget that both functional dependencies and associated types  
come with syntactic restrictions that are there just to "tame" the  
Turing completeness, i.e., to guarantee that type checking will  
actually terminate. (I do agree that these restrictions, for  
functional dependencies anyway, can be thought of as twisted in their  
own right, but then again, there's no such thing as a free lunch.)

Admittedly, it's my experience that whenever one wants to do  
something interesting (and here I mean "interesting" in a way that  
you would probably label as "rather twisted" ;-)), one has to bypass  
these restrictions (and, hence, allow for potentially undecidable  
instances). Now, I haven't really worked with associated types (or,  
for that matter, associated type synonyms), but my hope is that, when  
using those, turning off the checks is needed less often. We'll see.

Another option would be not to care that much about looping type  
checkers: when it loops, you'll probabely notice it quite soon  
already :-). That said, that would not be the option I'd pick though:  
being restricted to, say, structural recursion on the type-level  
could well cause your type-level programs to be better organised.

Cheers,

   Stefan