[Haskell-cafe] Type-level naturals & multiplication

[Martin Sulzmann]

On Tue, Oct 13, 2009 at 9:37 AM, Simon Peyton-Jones
<simonpj at 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<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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20091013/02c75afa/attachment.html