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

[Thomas Schilling]

On Fri, 2007-09-14 at 10:42 +1200, ok wrote:
> 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.")

The type system doesn't help you avoid writing non-terminating programs,
so i see no problem with it being possible giving programmers the power
to express and check more complex properties of their programs -- as
long as type-checking remains sound.  From a practical standpoint,
non-terminating type checks are just as much a bug as non-terminating
library functions.  Type systems need more thought anyways, so why not
make sure it's terminating, too?  The other extreme is to use dependent
types everywhere, but this has a bit more drastic consequences to the
accessibility and practicality of the language.

I don't think this will become a mainstream tool any time soon, but it
may turn out to be very valuable to library authors.  We also shouldn't
forget that this is a brand-new feature and requires proper evaluation;
how better could this be achieved than by having it included as an
optional feature in a mature and well-used compiler?  I am glad that
Haskellers try to integrate theory and practice that nicely.

/ Thomas