Re: termination for FDs and ATs

27 Apr 2006


      Ross Paterson writes:
...
On Thu, Apr 27, 2006 at 12:40:47PM +0800, Martin Sulzmann wrote:
...
Yes, FDs and ATs have the exact same problems when it comes to termination.
The difference is that ATs impose a dynamic check (the occurs check)
when performing type inference (fyi, such a dynamic check is sketched
in a TR version of the FD-CHR paper).
Isn't an occurs check unsafe when the term contains functions (type
synonyms)?  You might reject something that would have been accepted
if the function had been reduced and discarded the problematic subterm.
Correct. Any dynamic check is necessarily incomplete.

Martin