On Tue, Oct 13, 2009 at 9:37 AM, Simon Peyton-Jones <simonpj@microsoft.com> 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
|
| 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