On Tue, Oct 13, 2009 at 9:37 AM, Simon Peyton-Jones <[email protected]>wrote:
> | > Is there any way to define type-level multiplication without requiring > | > undecidable instances? > | > | No, not at the moment. The reasons are explained in the paper "Type > | Checking with Open Type Functions" (ICFP'08): > | > | > http://www.cse.unsw.edu.au/~chak/papers/tc-tfs.pdf<http://www.cse.unsw.edu.au/%7Echak/papers/tc-tfs.pdf> > | > | We want to eventually add closed *type families* to the system (ie, > | families where you can't add new instances in other modules). For > | such closed families, we should be able to admit more complex > | instances without requiring undecidable instances. > > It's also worth noting that while "undecidable" instances sound scary, but > all it means is that the type checker can't prove that type inference will > terminate. We accept this lack-of-guarantee for the programs we *run*, and > type inference can (worst case) take exponential time which is not so > different from failing to terminate; so risking non-termination in type > inference is arguably not so bad. > > > Some further details to shed some light on this topic. "Undecidable" instances means that there exists a program for which there's an infinite reduction sequence. By "undecidable" I refer to instances violating the conditions in the icfp'08 and in the earlier jfp paper "Understanding Functional Dependencies via Constraint Handling Rules". Consider the classic example Add (Succ x) x ~ x --> Succ (Add x x) ~ x substitute for x and you'll get another redex of the form Add (Succ ..) ... and therefore the reduction won't terminate To fix this problem, i.e. preventing the type checker to non-terminate, we could either (a) spot the "loop" in Add (Succ x) x ~ x and reject this unsatisfiable constraint and thus the program (b) simply stop after n steps The ad-hoc approach (b) restores termination but risks incompleteness. Approach (a) is non-trivial to get right, there are more complicated loopy programs where spotting the loops gets really tricky. The bottom line is this: Running the type checker on "undecidable" instances means that there are programs for which - the type checker won't terminate, or - wrongly rejects the program (incompleteness) So, the situation is slightly more scary, BUT programs exhibiting the above behavior are (in my experience) rare/contrived. -Martin
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
