[Haskell-cafe] Type-level naturals & multiplication
Martin Sulzmann
martin.sulzmann.haskell at googlemail.com
Tue Oct 13 18:31:06 EDT 2009
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
More information about the Haskell-Cafe
mailing list