[Haskell] The GHC typechecker is Turing-complete

[Robert Dockins]

On Aug 11, 2006, at 7:40 AM, Josef Svenningsson wrote:

> On 8/11/06, Robert Dockins <robdockins at fastmail.fm> wrote:
>> My purpose today is to show that the GHC typechecker with multi- 
>> parameter
>> typeclasses, functional dependencies, and undecidable instances is  
>> Turing-
>> complete.  Some time ago on this mailing list, there was a brief  
>> discussion
>> about a lambda calculus and a direct Turing-machine  
>> implementation; either
>> would be sufficient to demonstrate the Turing-completeness of the  
>> typechecker.
>> However, neither implementation was preserved on-list, and the  
>> links are
>> now dead.
>>
> Here's a link that works:
> http://www.lochan.org/keith/publications/undec.html


Ah, thanks.  This is interesting because it doesn't even require  
functional dependencies.  OTOH, he uses code generation techniques to  
create the TMs in the first place...


> All the best,
>
> /Josef



Rob Dockins

Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
           -- TMBG