Ross Paterson: > 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
This definition is not quite correct. The instance would be instance Mul a b => Mul a [b] where type Result a [b] = [Result a b] -- second argument is different x .*. ys = map (x .*.) ys The arguments to the ATs, in an instance def, need to coincide with the class parameters. So, in f, we get the context Mul a [b], Result a [b] = b (*) which reduces to Mul a b, [Result a b] = b at which point type inference *terminates*. So, we get the following type for f f :: (Mul a b, [Result a b] = b) => Bool -> a -> b -> [Result a b] Given the instance definitions of that example, you can never satisfy the equality [Result a b] = b, and hence, never apply the function f. In other words, AT type inference sidesteps the problem by just not committing on whether f's type is satisfiable. It rather gives a condition under which f can be applied, namely [Result a b] = b. That condition will then be checked at any application site. So, clearly termination for ATs and FDs is *not* the same. It's quite interesting to have a close look at where the difference comes from. The FD context corresponding to (*) above is Mul a [b] b Improvement gives us Mul a [[c]] [c] with b = [c] which simplifies to Mul a [c] c which is where we loop. The culprit is really the new type variable c, which we introduce to represent the "result" of the type function encoded by the type relation Mul. So, this type variable is an artifact of the relational encoding of what really is a function, which brings me back to my fundamental objection to FDs: We are functional, not logic programmers. Manuel _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime