# 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)