Hello,
On 4/29/06, Manuel M T Chakravarty
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*.
Perhaps I misunderstand something, but terminating is not always an option. For example, if we are type checking something with a type signature, or an expression where the monomorphism restriction kicks in, we have to discharge the predicates or reject the program. (This is why the example on the wiki is written with lambdas).
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.
What do you think should happen if I add the following definition as well? g :: (Mul a b) => Bool -> a -> b -> [Result a b] g = f It appears that the "right" thing would be to reject this program, because we cannot solve the constraint "[Result a b] = b". However, in general this may require some fancy reasoning, which is why naive implementations simply loop.
So, clearly termination for ATs and FDs is *not* the same. I assume (appologies if this is incorrect) that when you are talking about termintion of ATs or FDs you mean the terminations of particular algorithms for solving predicates arising in both systems. I am not sure if ATs somehow make the problem simpler, but certainly choosing to delay predicates rather than solve them is an option available to both systems (modulo type signatures, as I mentioned above).
-Iavor