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.")
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
