termination for FDs and ATs
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