<br><br><div class="gmail_quote">On Tue, Oct 13, 2009 at 9:37 AM, Simon Peyton-Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div class="im">| > Is there any way to define type-level multiplication without requiring<br>
| > undecidable instances?<br>
|<br>
| No, not at the moment. The reasons are explained in the paper "Type<br>
| Checking with Open Type Functions" (ICFP'08):<br>
|<br>
| <a href="http://www.cse.unsw.edu.au/%7Echak/papers/tc-tfs.pdf" target="_blank">http://www.cse.unsw.edu.au/~chak/papers/tc-tfs.pdf</a><br>
|<br>
| We want to eventually add closed *type families* to the system (ie,<br>
| families where you can't add new instances in other modules). For<br>
| such closed families, we should be able to admit more complex<br>
| instances without requiring undecidable instances.<br>
<br>
</div>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.<br>
<font color="#888888"><br>
<br></font></blockquote><div><br>Some further details to shed some light on this topic.<br><br>"Undecidable" instances means that there exists a program for which there's<br>an infinite reduction sequence. <br>
By "undecidable" I refer to instances violating the conditions in the icfp'08<br>and in the earlier jfp paper "Understanding Functional Dependencies via<br>Constraint Handling Rules".<br><br>Consider the classic example<br>
<br> Add (Succ x) x ~ x <br>--> Succ (Add x x) ~ x <br><br> substitute for x and you'll get another redex of the form<br><br> Add (Succ ..) ... and therefore the reduction won't terminate<br><br>To fix this problem, i.e. preventing the type checker to non-terminate,<br>
we could either<br><br> (a) spot the "loop" in Add (Succ x) x ~ x and reject this<br> unsatisfiable constraint and thus the program<br> (b) simply stop after n steps<br><br>The ad-hoc approach (b) restores termination but risks incompleteness.<br>
<br>Approach (a) is non-trivial to get right, there are more complicated loopy programs<br>where spotting the loops gets really tricky.<br><br>The bottom line is this:<br><br>Running the type checker on "undecidable" instances means that<br>
there are programs for which<br><br> - the type checker won't terminate, or<br> - wrongly rejects the program (incompleteness)<br><br>So, the situation is slightly more scary, BUT<br>programs exhibiting the above behavior are (in my experience) rare/contrived.<br>
<br>-Martin<br><br></div></div><br>