# (Un)termination of overloading resolution Classic List Threaded 2 messages Reply | Threaded
Open this post in threaded view
|

## (Un)termination of overloading resolution

 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... _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## (Un)termination of overloading resolution

 [hidden email] 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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe