[Haskell-cafe] Monad.Reader 8: Haskell, the new C++
nominolo at googlemail.com
Thu Sep 13 19:05:32 EDT 2007
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-
> $ 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.
More information about the Haskell-Cafe