termination for FDs and ATs
iavor.diatchki at gmail.com
Mon May 1 14:31:09 EDT 2006
On 4/29/06, Manuel M T Chakravarty <chak at cse.unsw.edu.au> wrote:
> 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).
More information about the Haskell-prime