termination for FDs and ATs
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Sat Apr 29 17:49:16 EDT 2006
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
More information about the Haskell-prime
mailing list