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).
A problem with ATs at the moment is that some terminating FD programs result into non-terminating AT programs. Somebody asked how to write the MonadReader class with ATs: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014489.html This requires an AT extension which may lead to undecidable type inference: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014609.html Martin Ross Paterson writes: > To ensure termination with FDs, there is a proposed restriction that > an instance that violates the coverage condition must have a trivial > instance improvement rule. Is the corresponding restriction also > required for ATs, namely that an associated type synonym definition > may only contain another associated type synonym at the outermost > level? If not, wouldn't the non-terminating example from the FD-CHR > paper (ex. 6, adapted below) also be a problem for ATs? > > class Mul a b where > type Result a b > (.*.) :: a -> b -> Result a b > > instance Mul a b => Mul a [b] where > type Result a b = [Result a b] > x .*. ys = map (x .*.) ys > > f = \ b x y -> if b then x .*. [y] else y > > _______________________________________________ > Haskell-prime mailing list > [email protected] > http://haskell.org/mailman/listinfo/haskell-prime _______________________________________________ Haskell-prime mailing list [email protected] http://haskell.org/mailman/listinfo/haskell-prime
