termination for FDs and ATs

[Martin Sulzmann]

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
 > Haskell-prime at haskell.org
 > http://haskell.org/mailman/listinfo/haskell-prime