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