[Haskell-cafe] (Un)termination of overloading resolution

oleg at pobox.com oleg at pobox.com
Wed Feb 22 01:49:49 EST 2006

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

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

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

More information about the Haskell-Cafe mailing list