Hi Keith,
| Following recent discussions about instance declarations in Haskell-2
| on the Haskell mailing list, and the suggestion that without
| sufficient restrictions in this area Haskell's type system would
| become undecidable, I decided to demonstrate this directly. In this
| brief paper I present a construction that encodes a Turing machine
| directly in a series of instance declarations. The encoding is such
| that it forces the type checker to simulate the operation of a
| specified Turing machine in order to check the program. If the Turing
| machine terminates then the program is well-typed; if the Turing
| machine fails to terminate then it is ill-typed. The well-known
| undecidability of the Halting problem thereby carries across to the
| unrestricted version of the Haskell-2 type system.
It's great that you've done this, but I think someone ought to
point out that this result, and even the basic method, is not
actually new: You might want to find a copy of the proceedings
for FPCA 91 (in Springer LNCS 523) and take a look at the paper
called "On the Complexity of ML Typability with Overloading" by
Volpano and Smith. Even before that paper was published, I think
the result was common knowledge in the Haskell community at that
time. Gofer was announced before FPCA 91 and released a couple
of weeks later (finding a suitable ftp site was a little harder
back then), but we knew then that it's type system was undecidable,
as we do now with the March version of Hugs 1.3.
All the best,
Mark
