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

[ok]

I wrote:
>> 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.

On 13 Sep 2007, at 4:27 pm, Stefan Holdermans wrote:
> 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 don't know anything about associated types, so can't comment on those.
But on the subject of functional dependencies, you and the author of the
article in Monad.Reader 8 *cannot* both be right, because the whole
point of that article is to explain how to program in the type system,
using, amongst other things, conditionals and recursion, in such a way
that a Turing machine can surely be simulated.  If there is some
restriction to guarantee termination, then those techniques can't work.
>

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

Ah, now we have it.  To quote Conrad Parker:
     This tutorial uses the Haskell98 type system extended with
     multi-parameter typeclasses and undecidable instances.
     We need to enable some GHC extensions to play with this type- 
hackery:
     $ ghci -fglasgow-exts -fallow-undecidable-instances

That is the combination I'm talking about.

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

If you hope that, then we probably agree more than you might think.
My point is that the combination exists and is being explained so that
people can use it, and that the result is comparable in C++.  (Imagine
Dame Edna Everage saying "I mean that in a loving way, possums.")