termination for FDs and ATs
sulzmann at comp.nus.edu.sg
Thu Apr 27 00:40:47 EDT 2006
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:
This requires an AT extension which may lead to undecidable type
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
More information about the Haskell-prime