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? 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...