oleg@pobox.com writes:

Martin Sulzmann wrote:

...

Let's consider the general case (which I didn't describe in my earlier email). In case we have an n-ary type function T (or (n+1)-ary type class constraint T) the conditions says for each

type T t1 ... tn = t

(or rule T t1 ... tn x ==> t)

then rank(ti) > rank(t) for each i=1,..,n

...

...

Sorry, I left out the precise definition of the rank function in my previous email. Here's the formal definition.

rank(x) is some positive number for variable x

rank(F t1 ... tn) = 1 + rank t1 + ... + rank tn

where F is an n-ary type constructor.

rank (f t) = rank f + rank t

f is a functor variable

Yes, I was wondering what rank means exactly. But now I do have a problem with the criterion itself. The following simple and quite common code

...

newtype MyIOState a = MyIOState (Int -> IO (a,Int))

instance Monad MyIOState where return x = MyIOState (\s -> return (x,s))

instance MonadState Int MyIOState where put x = MyIOState (\s -> return ((),x))

becomes illegal then? Indeed, the class |MonadState s m| has a functional dependency |m -> s|. In our case, m = MyIOState, rank MyIOState = 1 s = Int rank Int = 1 and so rank(m) > rank(s) is violated, right?

The additional conditions I propose are only necesssary once we break the Bound Variable Condition. Recall: The Bound Variable Condition (BV Condition) says: for each instance C => TC ts we have that fv(C) subsetof fv(ts) (the same applies to (super)class declarations which I leave out here). The above MonadState instance does NOT break the BV Condition. Hence, everything's fine here, the FD-CHR results guarantee that type inference is sound, complete and decidable. Though, your earlier example breaks the BV Condition.

class Foo m a where foo :: m b -> a -> Bool

instance Foo m () where foo _ _ = True

instance (E m a b, Foo m b) => Foo m (a->()) where foo m f = undefined

class E m a b | m a -> b where tr :: m c -> a -> b instance E m (() -> ()) (m ())

In the second instance, variable b appears only in the context but not in the instance head. But variable b is "captured" by the constraint E m a b where m and a appear in the instance head and we have that class E m a b | m a -> b. We say that this instance satisfies the Weak Coverage Condition. The problem is that Weak Coverage does not guarantee termination. See this and the earlier examples we have discussed so far. To obtain termination, I propose to impose stronger conditions on improvement rules (see above). My guess is that thus we obtain termination. If we can guarantee termination, we know that Weak Coverage guarantees confluence. Hence, we can restore sound, complete and decidable type inference.

BTW, the above definition of the rank is still incomplete: it doesn't say what rank(F t1 ... tm) is where F is an n-ary type constructor and m < n. Hopefully, the rank of an incomplete type application is bounded (otherwise, I have a non-termination example in mind). If the rank is bounded, then the problem with defining an instance of MonadState persists. For example, I may wish for a more complex state (which is realistic):

...

newtype MyIOState a = MyIOState (Int -> IO (a,(Int,String,Bool))) instance MonadState (Int,String,Bool) MyIOState

Now, the rank of the state is 4...

The simple solution might be for any n-ary type constructor F rank(F t1 ... tm) = 1 + rank t1 + ... + rank tm where m<=n This might be too naive, I don't know. I haven't thought about the case where we need to compute the rank of a type constructor. Though, the style of termination proof I'm using dates back to Prolog which we know is untyped. Hence, there might not be any problem after all? Martin