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

[Martin Sulzmann]

oleg at 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