User talk:ConradParker/InstantInsanity

This is a discussion page for the paper Type-Level Instant Insanity.

If you are kind enough to read this paper, you may like to jot down any thoughts it triggers off, and see what others have written. This talk-page lets you do just that.

You can identify your entries by preceding them with four tildes. Doing so adds your name, and the date. Thus:

ConradParker 03:51, 30 August 2007 (UTC) Note from Conrad

If you say who you are in this way, we'll be able to acknowledge your help in a revised version of the paper.

---

Patryk Zadarnowski offered the following during an email discussion:

> Are overlapping and undecidable instances different things?

Yep, quite different. Both try to add general programming to the type level. Overlapping instances do that by allowing things like:

       instance Foo (a, Int) where ...
       instance Foo (a, b)   where ...

and devising rules fo choosing (1) over (2) whenever possible. Right now, this is very, very clunky, under-specified and likely to go away once Manuel finishes his associated data types implementation. :) For example, what is GHC supposed to do with:

       instance Foo (a, Int) where ...
       instance Foo (Int, b) where ...

Undecidable instances basically means that general recursion is allowed at the type level. So the above will be accepted (I think) and, more likely than not, result in GHC's typechecker spinning into an infinite loop when it tries to resolve all these instance declarations. Hence the name; if the instance declarations are allowed to express any patterns, they provide a Turing complete language, and if they provide a Turing complete language, than it's impossible to decide whether any given type-level program will terminate (i.e. is OK) or not. If you're using -fallow-undecidable-instances than yes, your haskell type system is Turing-complete :)

BTW, the way GHC solves this is by declaring a fixed-depth stack for "evaluation" of instance declarations. It's something small like 5-deep by default. If it gets exceeded, GHC will bail out with an error message. You can increase the stack depth using some other -f on the command line :)

ConradParker 02:37, 10 September 2007 (UTC)

On that note, Pepe Iborra pasted a version of Instant Insanity with type families.

ConradParker 06:53, 12 September 2007 (UTC)

There was a further discussion about termination of type-checking, and about associated types in the thread Monad.Reader 8: Haskell, the new C++ on the haskell-cafe mailing list.

ConradParker 02:37, 25 September 2007 (UTC)

Alex Rubinsteyn posted Almost Solving Instant Insanity with C++ templates. This was followed up (in the proggit discussion) by a D version.

ConradParker 08:21, 12 November 2007 (UTC)