termination for FDs and ATs

Martin Sulzmann sulzmann at comp.nus.edu.sg
Thu Apr 27 04:21:41 EDT 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.


More information about the Haskell-prime mailing list