Difference between revisions of "User talk:ConradParker/InstantInsanity"
ConradParker (talk | contribs) m (cleanup) |
ConradParker (talk | contribs) (add notes about overlapping and undecidable instances from patryk z) |
||
| Line 8: | Line 8: | ||
If you say who you are in this way, we'll be able to acknowledge your help in a revised version of the paper. |
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: |
||
| + | <haskell> |
||
| + | instance Foo (a, Int) where ... |
||
| + | instance Foo (a, b) where ... |
||
| + | </haskell> |
||
| + | 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 [http://www.cse.unsw.edu.au/~chak/papers/CKPM05.html associated data types] implementation. :) For example, |
||
| + | what is |
||
| + | GHC supposed to do with: |
||
| + | <haskell> |
||
| + | instance Foo (a, Int) where ... |
||
| + | instance Foo (Int, b) where ... |
||
| + | </haskell> |
||
| + | 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 |
||
| + | <tt>-fallow-undecidable-instances</tt> |
||
| + | 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 <tt>-f</tt> on the command |
||
| + | line :) |
||
| + | |||
| + | [[User:ConradParker|ConradParker]] 02:37, 10 September 2007 (UTC) |
||
Revision as of 02:37, 10 September 2007
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)