User talk:ConradParker/InstantInsanity

From HaskellWiki
Revision as of 06:55, 12 September 2007 by ConradParker (talk | contribs) (mnislaih -> Pepe Iborra (link to user page))

Jump to: navigation, search

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



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


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)