On Sun, Feb 12, 2006 at 09:32:14PM +0100, Niklas Broberg wrote:

Irrelevant to the discussion above, but I wonder whether the Monoid constraint should really be there on MonadWriter. I could imagine lots of interesting applications of writer monads that don't output a monoid, an example would be a monad that iteratively computes a result of better and better precision and "tells" the result of each step until told to stop. In this case the merging would not be mplus but to always throw away the old argument (flip const).

You also need a value for return. Then the monad laws will ensure that you have another monoid.

Stefan Wehr writes:

Niklas Broberg wrote::

...

On 2/10/06, Ross Paterson wrote:

...

On Fri, Feb 10, 2006 at 05:20:47PM +0100, Niklas Broberg wrote:

...

- when looking at the definition of MonadWriter the Monoid constraint is not strictly necessary, and none of the other mtl monads have anything similar. Is it the assumption that this kind of constraint is never really necessary, and thus no support for it is needed for ATS?

I think that's right -- it's only needed for the Monad instance for WriterT. But it is a convenience. In any instance of MonadWriter, the w will be a monoid, as there'll be a WriterT in the stack somewhere, so the Monoid constraint just saves people writing general functions with MonadWriter from having to add it.

Sure it's a convenience, and thinking about it some more it would seem like that is always the case - it is never crucial to constrain a parameter. But then again, the same applies to the Monad m constraint, we could give the same argument there (all actual instances will be monads, hence...). So my other question still stands, why not allow constraints on associated types as well, as a convenience?

Manuel (Chakravarty) and I agree that it should be possible to constrain associated type synonyms in the context of class definitions. Your example shows that this feature is actually needed. I will integrate it into phrac within the next few days.

By possible you mean this extension won't break any of the existing ATS inference results? You have to be very careful otherwise you'll loose decidability. Something more controversial. Why ATS at all? Why not encode them via FDs? Example -- ATS class C a where type T a m :: a->T a instance C Int where type T Int = Int m _ = 1 -- FD encoding class T a b | a->b instance T Int Int class C a where m :: T a b => a->b instance C Int where m _ = 1 -- general recipe: -- encode type functions T a via type relations T a b -- replace T a via fresh b under the constraint C a b The FD program won't type check under ghc but this doesn't mean that it's not a legal FD program. It's wrong to derive certain conclusions about a language feature by observing the behavior of a particular implementation! Martin

Can someone explain to me why decidability is of any practical interest at all? What's the (practical) difference between a decision procedure which might never terminate and one which might take 1,000,000 years to terminate? Actually, why push it out to 1,000,000 years: in the context of a compiler for a practical programming language, a decision procedure which might take an hour to terminate might as well be undecidable ... surely all we really need is that the decision procedure _typically_ terminates quickly, and that where it doesn't we have the means of giving it hints which ensure that it will.

I'm tempted to agree with you. I don't care if the compiler terminates on all my programs, or if it sometimes quits and says: "I don't know if this is correct." However, I do think that it is of very much importance that programmers and compiler implementors know which programs are legal and which are not. If a problem is decidable, it has the nice property that the problem (*not* the algorithm) can be used as a specification. Implementors are free to implement different algorithms, as long as they all solve the problem. If the problem is undecidable, how do you make sure that different compilers accept the same programs? If you don't want to find a subproblem that is decidable, you'll have to specify an algorithm, which is usually far more complicated, error-prone, and difficult to grasp for programmers. Cheers, Andres

On Thu, Feb 16, 2006 at 12:45:03PM +0000, Miles Sabin wrote:

Andres Loeh wrote,

...

If a problem is decidable, it has the nice property that the problem (*not* the algorithm) can be used as a specification. Implementors are free to implement different algorithms, as long as they all solve the problem. If the problem is undecidable, how do you make sure that different compilers accept the same programs? If you don't want to find a subproblem that is decidable, you'll have to specify an algorithm, which is usually far more complicated, error-prone, and difficult to grasp for programmers.

Again, I'm not sure that decidability helps practically here: we're not interested in "compiler A and compiler B accept the same programs", we're interested in "compiler A and compiler B accept some well defined subset of possible programs in a reasonable amount of time and space".

But it seems that well defining that subset is equivalent to the problem of finding a suitable decidable algorithm. John -- John Meacham - ⑆repetae.net⑆john⑈

Martin Sulzmann wrote::

Stefan Wehr writes:

...

[...] Manuel (Chakravarty) and I agree that it should be possible to constrain associated type synonyms in the context of class definitions. Your example shows that this feature is actually needed. I will integrate it into phrac within the next few days.

By possible you mean this extension won't break any of the existing ATS inference results?

Yes, although we didn't go through all the proofs.

You have to be very careful otherwise you'll loose decidability.

Do you have something concrete in mind or is this a more general advice? Stefan

Stefan Wehr writes:

Martin Sulzmann wrote::

...

Stefan Wehr writes:

...

[...] Manuel (Chakravarty) and I agree that it should be possible to constrain associated type synonyms in the context of class definitions. Your example shows that this feature is actually needed. I will integrate it into phrac within the next few days.

By possible you mean this extension won't break any of the existing ATS inference results?

Yes, although we didn't go through all the proofs.

...

You have to be very careful otherwise you'll loose decidability.

Do you have something concrete in mind or is this a more general advice?

I'm afraid, I think there's a real issue. Here's the AT version of Example 15 from "Understanding FDs via CHRs" class D a class F a where type T a instance F [a] where type T [a] = [[a]] instance (D (T a), F a) => D [a] ^^^^^^^ type function appears in type class Type inference (i.e. constraint solving) for D [a] will not terminate. Roughly, D [[a]] -->_instance D (T [a]), F [a]) -->_type function D [[a]], F [a] and so on Will this also happen if type functions appear in superclasses? Let's see. Consider class C a class F a where type T a instance F [a] where type T [a] = [[[a]]] class C (T a) => D a ^^^^^ type function appears in superclass context instance D [a] => C [[a]] -- satisfies Ross Paterson's Termination Conditions Consider D [a] -->_superclass C (T [a]), D [a] -->_type function C [[[a]]], D [a] -->_instance D [[a]], D [a] and so on My point: - The type functions are obviously terminating, e.g. type T [a] = [[a]] clearly terminates. - It's the devious interaction between instances/superclasss and type function which causes the type class program not to terminate. Is there a possible fix? Here's a guess. For each type definition in the AT case type T t1 = t2 (or improvement rule in the FD case rule T1 t1 a ==> a=t2 BTW, any sufficient restriction which applies to the FD case can be lifted to the AT case and vice versa!) we demand that the number of constructors in t2 is strictly smaller than the in t1 (plus some of the other usual definitions). Then, type T [a] = [[a]] although terminating, is not legal anymore. Then, there might be some hope to recover termination (I've briefly sketched a proof and termination may indeed hold but I'm not 100% convinced yet). Martin

This is not a counter-example to my conjecture. 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 Your example violates this condition

class E m a b | m a -> b instance E m (() -> ()) (m ())

The improvement rule says: rule E m (() -> ()) x ==> x=(m ()) but rank m < rank (m ()) Your example shows that the condition rank(t1)+...+rank(tn) > rank(t) is not sufficient (but that's not a surprise). Program text

test = foo (\f -> (f ()) :: ()) (\f -> (f ()) :: ()) gives rise to

Foo ((->) (() -> ())) ((() -> ()) -> ()) via

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

this constraint reduces to E ((->) (() -> ())) (()->()) x Foo ((->) (() -> ())) x the above improvement yields x = (((->) (() -> ()))) () this leads to Foo ((->) (() -> ())) ((((->) (() -> ()))) ()) and so on (the second component is increasing). So, I'll stick to my claim. I don't think I have time at the moment to work out the details of my claim/proof sketch. But if somebody is interested. The following is a good reference how to attack the problem: @inproceedings{thom-term, author = "T. Fr{\"u}hwirth", title = "Proving Termination of Constraint Solver Programs", booktitle = "Proc.\ of New Trends in Constraints: Joint {ERCIM/Compulog} Net Workshop", volume = "1865", series = "LNAI", publisher = "Springer-Verlag", year = "2000" } Martin oleg@pobox.com writes:

Martin Sulzmann wrote:

...

- The type functions are obviously terminating, e.g. type T [a] = [[a]] clearly terminates. - It's the devious interaction between instances/superclasss and type function which causes the type class program not to terminate.

Is there a possible fix? Here's a guess. For each type definition in the AT case

type T t1 = t2

(or improvement rule in the FD case

rule T1 t1 a ==> a=t2

we demand that the number of constructors in t2 is strictly smaller than the in t1 (plus some of the other usual definitions).

I'm afraid that may still be insufficient, as the following counter-example shows. It causes GHC 6.4.1 to loop in the typechecking phase. I haven't checked the latest GHC. The example corresponds to a type function (realized as a class E with functional dependencies) in the context of an instance. The function in question is

class E m a b | m a -> b instance E m (() -> ()) (m ())

We see that the result of the function, "m ()" is smaller (in the number of constructors) that the functions' arguments, "m" and "() -> ()" together. Plus any type variable free in the result is also free in at least one of the arguments. And yet it loops.

{-# OPTIONS -fglasgow-exts #-} -- Note the absence of the flag -fallow-undecidable-instances

module F where

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

-- There is only one instance of the class with functional dependencies instance E m (() -> ()) (m ()) where tr x = undefined

-- GHC(i) loops

test = foo (\f -> (f ()) :: ()) (\f -> (f ()) :: ())

oleg@pobox.com writes:

...

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

I didn't know what condition you meant for the general form. But the condition above is not sufficient either, as a trivial modification of the example shows. The only modification is

instance E ((->) (m ())) (() -> ()) (m ()) where

and test = foo (undefined::((() -> ()) -> ()) -> ()) (\f -> (f ()) :: ())

Now we have t1 = ((->) (m ())) : two constructors, one variable t2 = () -> () : three constructors t = m () : one constructor, one variable

and yet GHC 6.4.1 loops in the typechecking phase as before.

rank (() ->()) > rank (m ()) does NOT hold. 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 Hence, rank (()->()) = 3 rank (m ()) = rank m + 1 We cannot verify that 3 > rank m + 1. So, I still claim my conjecture is correct. Martin P. S. Oleg, can you next time please provide more details why type inference does not terminate. This will help others to follow our discussion.

The following not only answers Roman's question but also includes a short summary (at the end) of the discussion we had so far. Roman Leshchinskiy writes:

On Wed, 2006-02-22 at 12:33 +0800, Martin Sulzmann wrote:

...

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

I'm probably misunderstanding something but doesn't this imply that we cannot declare any instances for

class C a b | a -> b, b -> a

which do not break the bound variable condition? This would remove one of the main advantages fundeps have over associated types.

Sure you can. For example, class C a b | a->b, b->a instance C [a] [a] The above class/instance declarations satisfy the Consistency, Coverage, Basic Bound Variable Conditions. See "Understanding FDs via CHRs" paper (see Sect 4, 4.1). Under these conditions, we know that type inference is sound, complete and decidable. In your example below, you are not only breaking the Bound Variable Condition, but you are also breaking the Coverage Condition.

{-# OPTIONS -fglasgow-exts #-} data X data App t u data Lam t

class Subst s t u | s t -> u instance Subst X u u instance (Subst s u s', Subst t u t') => Subst (App s t) u (App s' t') breaks Coverage instance Subst (Lam t) u (Lam t)

class Apply s t u | s t -> u instance (Subst s t u, Eval u u') => Apply (Lam s) t u'

class Eval t u | t -> u instance Eval X X instance Eval (Lam t) (Lam t) instance (Eval s s', Apply s' t u) => Eval (App s t) u breaks Coverge and Bound Variable

x = undefined :: Eval (App (Lam (App X X)) (Lam (App X X))) u => u

It's no surprise that the ghc inferencer does not terminate. We know that breaking the Coverage Condition alone (not breaking any of the other conditions) will break termination. Well, not always but for certain examples.See Example 15, Sect 5.2 in the paper. We also know that breaking the Bound Variable Condition will break termination. See Example 16, Sect 5.2. All this may be surprising, cause the instances are terminating. It's the devious interaction between instance reduction and improvement. In case we break the Coverage Condition we need to find some "weaker" conditons which guarantee confluence (i.e. complete inference) *if* we know that inference is decidable. See Sect 6. So, it's really termination that's the trouble maker and there's really not hope to maintain termination in general. Though, if we can verify termination, e.g. for a particular inference goal, we obtain completeness. Hence, inference is sound, complete but semi-decidable. How/why did we need up talking about decidable FD inference? Well, somebody (can't remember who) asked how to translate the following FD program to ATs. class D b class D b => C a b | a->b In the AT system, FDs are expressed via type relations. class D b class D (T a) => C a where type T a The point here is that to encode the FD program the AT system (as described in ICFP'05) needs to be extended. Specifically, associated type synonyms may now constrain the types of type classes in the instance/superclass context. I've pointed out that this easily leads to undecidable type inference. I've appended my *old email* below. My main point were: - The type functions are obviously terminating, e.g. type T [a] = [[a]] clearly terminates. - It's the devious interaction between instances/superclasss and type function which causes the type class program not to terminate. The problem with decidable AT inference is very similar to the FD case where we break the Bound Variable Condition. Here's a "rough" FD encoding of the above AT program. class T a b | a->b class D b class (D b, T a b) => C a ^^^^^^^^^^^ Notice that the superclass context contains the unbound variable b. This observation allowed me to lift the "critical" FD examples to the AT world. As a remedy to the undecidability issue, I proposed to impose stronger conditions on AT type relations (we know the AT type relations are terminating but that's still not enough). I'm not reproducing here the details, see my earlier emails. Also note that similar conditions can be applied to FD programs (to recover decidability). Here's now the summary: - Decidable type inference for ATs and FDs is an equally hard problem. - There's a huge design space which additional conditions will recover decidability, e.g. impose ranking conditions on type relations, dynamic termination checks etc. It's very likely that similar conditions apply to FDs and ATs. - To encode certain FD programs the AT system needs extensions which may threaten decidable type inference. Martin *old email*

...

Stefan Wehr writes:

...

[...] Manuel (Chakravarty) and I agree that it should be possible to constrain associated type synonyms in the context of class definitions. Your example shows that this feature is actually needed. I will integrate it into phrac within the next few days.

By possible you mean this extension won't break any of the existing ATS inference results?

Yes, although we didn't go through all the proofs.

...

You have to be very careful otherwise you'll loose decidability.

Do you have something concrete in mind or is this a more general advice?

I'm afraid, I think there's a real issue. Here's the AT version of Example 15 from "Understanding FDs via CHRs" class D a class F a where type T a instance F [a] where type T [a] = [[a]] instance (D (T a), F a) => D [a] ^^^^^^^ type function appears in type class Type inference (i.e. constraint solving) for D [a] will not terminate. Roughly, D [[a]] -->_instance D (T [a]), F [a]) -->_type function D [[a]], F [a] and so on Will this also happen if type functions appear in superclasses? Let's see. Consider class C a class F a where type T a instance F [a] where type T [a] = [[[a]]] class C (T a) => D a ^^^^^ type function appears in superclass context instance D [a] => C [[a]] -- satisfies Ross Paterson's Termination Conditions Consider D [a] -->_superclass C (T [a]), D [a] -->_type function C [[[a]]], D [a] -->_instance D [[a]], D [a] and so on

I was talking about *static* termination. Hence, the conditions in the paper and the new one I proposed are of course incomplete. I think that's your worry, isn't it? There are reasonable type-level programs which are rejected but will terminate for certain goals. I think what you'd like is that each instance specifies its own termination condition which can then be checked dynamically. Possible but I haven't thought much about it. The simplest and most efficient strategy seems to stop after n number of steps. Martin Roman Leshchinskiy writes:

On Mon, 27 Feb 2006, Martin Sulzmann wrote:

...

...

...

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

I'm probably misunderstanding something but doesn't this imply that we cannot declare any instances for

class C a b | a -> b, b -> a

which do not break the bound variable condition? This would remove one of the main advantages fundeps have over associated types.

Sure you can. For example,

class C a b | a->b, b->a instance C [a] [a]

Ah, sorry, my question was very poorly worded. What I meant to say was that there are no instances declarations for C which satisfy your rule above and, hence, all instances of C (or of any other class with bidirectional dependencies) must satisfy the other, more restrictive conditions. Is that correct?

...

In your example below, you are not only breaking the Bound Variable Condition, but you are also breaking the Coverage Condition.

Yes, but I'm breaking the rule you suggested only once :-) It was only intended as a cute example. My worry, however, is that there are many useful type-level programs similar to my example which are guaranteed to terminate but which nevertheless do not satisfy the rules in your paper or the one you suggested here. I think ruling those out is unavoidable if you want to specify termination rules which every instance must satisfy individually. But why not specify rules for sets of instances instead? This is, for instance, what some theorem provers do for recursive functions and it allows them to handle a wide range of those without giving up decidability.

Roman

On Tue, Feb 21, 2006 at 07:13:17PM -0800, oleg@pobox.com wrote:

I'm afraid that may still be insufficient, as the following counter-example shows. It causes GHC 6.4.1 to loop in the typechecking phase. I haven't checked the latest GHC.

The HEAD is more cautious: F.hs:12:0: Variable occurs more often in a constraint than in the instance head in the constraint: E m a b (Use -fallow-undecidable-instances to permit this) In the instance declaration for `Foo m (a -> ())' This is required for all instances. GHC 6.4 relaxed it in the presence of FDs on the classes in the context, but as you've shown that is dangerous.

Claus Reinke writes:

The main argument for ATS is that the extra parameter for the functionally dependend type disappears, but as you say, that should be codeable in FDs. I say should be, because that does not seem to be the case at the moment.

My approach for trying the encoding was slightly different from your's, but also ran into trouble with implementations.

First, I think you need a per-class association, so your T a b would be specific to C. Second, I'd use a superclass context to model the necessity of providing an associated type, and instance contexts to model the provision of such a type. No big difference, but it seems closer to the intension of ATS: associated types translate into type association constraints.

(a lot like calling an auxiliary function with empty accumulator, to hide the extra parameter from the external interface)

...

Example

-- ATS class C a where type T a m :: a->T a instance C Int where type T Int = Int m _ = 1

-- alternative FD encoding attempt

class CT a b | a -> b instance CT Int Int

class CT a b => C a where m :: a-> b

instance CT Int b => C Int where m _ = 1::b

Hm, I haven't thought about this. Two comments. You use scoped variables in class declarations. Are they available in ghc? How do you encode? --AT instance C a => C [a] where type T [a] = [T a] m xs = map m xs Via the following I guess? instance CT a b => CT a [b] instance C a => C [a] where m xs = map m xs It seems your solution won't suffer from the problem I face. See below.

...

-- FD encoding class T a b | a->b instance T Int Int

class C a where m :: T a b => a->b

instance C Int where m _ = 1

-- general recipe: -- encode type functions T a via type relations T a b -- replace T a via fresh b under the constraint C a b

My AT encoding won't work with ghc/hugs because the class declaration of C demands that the output type b is univeral. Though, in the declaration instance C Int we return an Int. Hence, the above cannot be translated to System F. Things would be different if we'd translate to an untyped back-end.

referring to the associated type seems slightly awkward in these encodings, so the special syntax for ATS would still be useful, but I agree that an encoding into FDs should be possible.

...

The FD program won't type check under ghc but this doesn't mean that it's not a legal FD program.

glad to hear you say that. but is there a consistent version of FDs that allows these things - and if not, is that for lack of trying or because it is known not to work?

The FD framework in "Understanding FDs via CHRs" clearly subsumes ATs (based on my brute-force encoding). My previous email showed that type inference for FDs and ATs can be equally tricky. Though, why ATs? Well, ATs are still *very useful* because they help to structure programs (they avoid redundant parameters). On the other hand, FDs provide the user with the convenience of 'automatic' improvement. Let's do a little test. Who can translate the following FD program to AT? zip2 :: [a]->[b]->[(a,b)] zip2 (a:as) (b:bs) = (a,b) : (zip2 as bs) zip2 _ _ = [] class Zip a b c | c -> a, c -> b where mzip :: [a] -> [b] -> c instance Zip a b [(a,b)] where mzip = zip2 instance Zip (a,b) c e => Zip a b ([c]->e) where mzip as bs cs = mzip (zip2 as bs) cs Martin