termination for FDs and ATs

older
FFI proposal: allow some control...

Ross Paterson

24 Apr 2006 24 Apr '06

11:44 a.m.

To ensure termination with FDs, there is a proposed restriction that an instance that violates the coverage condition must have a trivial instance improvement rule. Is the corresponding restriction also required for ATs, namely that an associated type synonym definition may only contain another associated type synonym at the outermost level? If not, wouldn't the non-terminating example from the FD-CHR paper (ex. 6, adapted below) also be a problem for ATs? class Mul a b where type Result a b (.*.) :: a -> b -> Result a b instance Mul a b => Mul a [b] where type Result a b = [Result a b] x .*. ys = map (x .*.) ys f = \ b x y -> if b then x .*. [y] else y

Show replies by date

Martin Sulzmann

27 Apr 27 Apr

4:40 a.m.

Yes, FDs and ATs have the exact same problems when it comes to termination. The difference is that ATs impose a dynamic check (the occurs check) when performing type inference (fyi, such a dynamic check is sketched in a TR version of the FD-CHR paper). A problem with ATs at the moment is that some terminating FD programs result into non-terminating AT programs. Somebody asked how to write the MonadReader class with ATs: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014489.html This requires an AT extension which may lead to undecidable type inference: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014609.html Martin Ross Paterson writes:

...

To ensure termination with FDs, there is a proposed restriction that an instance that violates the coverage condition must have a trivial instance improvement rule. Is the corresponding restriction also required for ATs, namely that an associated type synonym definition may only contain another associated type synonym at the outermost level? If not, wouldn't the non-terminating example from the FD-CHR paper (ex. 6, adapted below) also be a problem for ATs?

class Mul a b where type Result a b (.*.) :: a -> b -> Result a b

instance Mul a b => Mul a [b] where type Result a b = [Result a b] x .*. ys = map (x .*.) ys

f = \ b x y -> if b then x .*. [y] else y

_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime

Ross Paterson

8:18 a.m.

On Thu, Apr 27, 2006 at 12:40:47PM +0800, Martin Sulzmann wrote:

...

Yes, FDs and ATs have the exact same problems when it comes to termination. The difference is that ATs impose a dynamic check (the occurs check) when performing type inference (fyi, such a dynamic check is sketched in a TR version of the FD-CHR paper).

Isn't an occurs check unsafe when the term contains functions (type synonyms)? You might reject something that would have been accepted if the function had been reduced and discarded the problematic subterm.

Martin Sulzmann

8:21 a.m.

Ross Paterson writes:

...

On Thu, Apr 27, 2006 at 12:40:47PM +0800, Martin Sulzmann wrote:

...
Yes, FDs and ATs have the exact same problems when it comes to termination. The difference is that ATs impose a dynamic check (the occurs check) when performing type inference (fyi, such a dynamic check is sketched in a TR version of the FD-CHR paper).

Isn't an occurs check unsafe when the term contains functions (type synonyms)? You might reject something that would have been accepted if the function had been reduced and discarded the problematic subterm.

Correct. Any dynamic check is necessarily incomplete. Martin

Manuel M T Chakravarty

29 Apr 29 Apr

9:01 p.m.

Ross Paterson:

...

On Thu, Apr 27, 2006 at 12:40:47PM +0800, Martin Sulzmann wrote:

...
Yes, FDs and ATs have the exact same problems when it comes to termination. The difference is that ATs impose a dynamic check (the occurs check) when performing type inference (fyi, such a dynamic check is sketched in a TR version of the FD-CHR paper).

Isn't an occurs check unsafe when the term contains functions (type synonyms)? You might reject something that would have been accepted if the function had been reduced and discarded the problematic subterm.

We account for that, but before explaining how, please let me emphasis that the occurs check is not something newly introduced with ATs, it's already part of plain HM type inference - it's just that it gets more interesting with ATs. Hence, I don't agree with Martin's comparison to FD type inference, where people are discussing "new" dynamic checks. Now, concerning ATs, the interesting rules is (var_U) of Fig 5 of "Associated Type Synonyms" http://www.cse.unsw.edu.au/~chak/papers/CKP05.html All this rule says is that, given an equality of the form a = t we cannot simplify this to the substitution [t/a] iff a \in FV(t). However, it does *not* say that we have to reject the program at this point. If t does not contain any type functions, then we can indeed reject the program, as the equality cannot be satisfied. However, as you rightly point out, this is not generally the case in the presence of type functions; eg, (a = t) could be equivalent to (a = S a) and we might have a definition for S reading S Int = Int Then, if a is at some point instantiated to Int, the equality obviously holds. In other words, if we have (a = t) with a \in FV(t) and the occurrence of a in t is below a type function, we don't know yet whether or not to reject the program. It is no problem to account for this uncertainty in AT type inference. The crucial difference between AT type inference and inference for vanilla type classes is that the constraint context includes equalities in addition to class predicates; ie, whenever we come across an equality t1 = t2 that we cannot solve yet (by unification), we put it into the constraint context. It may be solved later after some more substitutions have been applied. If not, it may end up in the signature of whatever binding we are currently typing (during generalisation). Manuel

Manuel M T Chakravarty

11:13 p.m.

Martin Sulzmann:

...

A problem with ATs at the moment is that some terminating FD programs result into non-terminating AT programs.

Somebody asked how to write the MonadReader class with ATs: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014489.html

This requires an AT extension which may lead to undecidable type inference: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014609.html

The message that you are citing here has two problems: 1. You are using non-standard instances with contexts containing non-variable predicates. (I am not disputing the potential merit of these, but we don't know whether they apply to Haskell' at this point.) 2. You seem to use the super class implication the wrong way around (ie, as if it were an instance implication). See Rule (cls) of Fig 3 of the "Associated Type Synonyms" paper. This plus the points that I mentioned in my previous two posts in this thread leave me highly unconvinced of your claims comparing AT and FD termination. Manuel

Ross Paterson

2 May 2 May

12:01 a.m.

On Sat, Apr 29, 2006 at 07:13:28PM -0400, Manuel M T Chakravarty wrote:

...

1. You are using non-standard instances with contexts containing non-variable predicates. (I am not disputing the potential merit of these, but we don't know whether they apply to Haskell' at this point.)

However they are under consideration for Haskell', so it would be worth knowing whether they would create future problems for ATs.

Martin Sulzmann

4:48 a.m.

Manuel M T Chakravarty writes:

...

Martin Sulzmann:

...
A problem with ATs at the moment is that some terminating FD programs result into non-terminating AT programs.

Somebody asked how to write the MonadReader class with ATs: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014489.html

This requires an AT extension which may lead to undecidable type inference: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014609.html

The message that you are citing here has two problems:

1. You are using non-standard instances with contexts containing non-variable predicates. (I am not disputing the potential merit of these, but we don't know whether they apply to Haskell' at this point.) 2. You seem to use the super class implication the wrong way around (ie, as if it were an instance implication). See Rule (cls) of Fig 3 of the "Associated Type Synonyms" paper.

I'm not arguing that the conditions in the published AT papers result in programs for which inference is non-terminating. We're discussing here a possible AT extension for which inference is clearly non-terminating (unless we cut off type inference after n number of steps). Without these extensions you can't adequately encode the MonadReader class with ATs.

...

This plus the points that I mentioned in my previous two posts in this thread leave me highly unconvinced of your claims comparing AT and FD termination.

As argued earlier by others, we can apply the same 'tricks' to make FD inference terminating (but then we still don't know whether the constraint store is consistent!). To obtain termination of type class inference, we'll need to be *very* careful that there's no 'devious' interaction between instances and type functions/improvement. It would be great if you could come up with an improved analysis which rejects potentially non-terminating AT programs. Though, note that I should immediately be able to transfer your results to the FD setting based on the following observation: I can turn any AT proof into a FD proof by (roughly) - replace the AT equation F a=b with the FD constraint F a b - instead of firing type functions, we fire type improvement and instances - instead of applying transitivity, we apply the FD rule F a b, F a c ==> b=c Similarly, we can turn any FD proof into a AT proof. Martin

Manuel M T Chakravarty

3 May 3 May

12:55 a.m.

Martin Sulzmann:

...

Manuel M T Chakravarty writes:

...
Martin Sulzmann:

...
A problem with ATs at the moment is that some terminating FD programs result into non-terminating AT programs.

Somebody asked how to write the MonadReader class with ATs: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014489.html

This requires an AT extension which may lead to undecidable type inference: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014609.html

The message that you are citing here has two problems:

1. You are using non-standard instances with contexts containing non-variable predicates. (I am not disputing the potential merit of these, but we don't know whether they apply to Haskell' at this point.) 2. You seem to use the super class implication the wrong way around (ie, as if it were an instance implication). See Rule (cls) of Fig 3 of the "Associated Type Synonyms" paper.

I'm not arguing that the conditions in the published AT papers result in programs for which inference is non-terminating.

We're discussing here a possible AT extension for which inference is clearly non-terminating (unless we cut off type inference after n number of steps). Without these extensions you can't adequately encode the MonadReader class with ATs.

This addresses the first point. You didn't address the second. let me re-formuate: I think, you got the derivation wrong. You use the superclass implication the wrong way around. (Or do I misunderstand?)

...

...
This plus the points that I mentioned in my previous two posts in this thread leave me highly unconvinced of your claims comparing AT and FD termination.

As argued earlier by others, we can apply the same 'tricks' to make FD inference terminating (but then we still don't know whether the constraint store is consistent!).

To obtain termination of type class inference, we'll need to be *very* careful that there's no 'devious' interaction between instances and type functions/improvement.

It would be great if you could come up with an improved analysis which rejects potentially non-terminating AT programs. Though, note that I should immediately be able to transfer your results to the FD setting based on the following observation:

I can turn any AT proof into a FD proof by (roughly)

- replace the AT equation F a=b with the FD constraint F a b - instead of firing type functions, we fire type improvement and instances - instead of applying transitivity, we apply the FD rule F a b, F a c ==> b=c

Similarly, we can turn any FD proof into a AT proof.

You may be able to encode AT proofs into FD proofs and vice versa, but that doesn't change the fact that some issues, as for example formation rules, are more natural, and I argue, more intuitive to the programmer in the AT setting. For example, with FDs you have to explain to the programmer the concept of weak coverage. With ATs, you don't need to do this, because the functional notation naturally leads people to write programs that obey weak coverage. Again, we want to write functional programs on the type level - after all FDs are *functional* dependencies - so, why use a relational notation? If, as you say, FDs and ATs are equivalent on some scale of type theoretic power, let us use a functional notation in a functional language. At least, that is more orthogonal language design. Manuel

Stefan Wehr

8:24 p.m.

Manuel M T Chakravarty wrote::

...

Martin Sulzmann:

...
Manuel M T Chakravarty writes:

...
Martin Sulzmann:

...
A problem with ATs at the moment is that some terminating FD programs result into non-terminating AT programs.

Somebody asked how to write the MonadReader class with ATs: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014489.html

This requires an AT extension which may lead to undecidable type inference: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014609.html

The message that you are citing here has two problems:

1. You are using non-standard instances with contexts containing non-variable predicates. (I am not disputing the potential merit of these, but we don't know whether they apply to Haskell' at this point.) 2. You seem to use the super class implication the wrong way around (ie, as if it were an instance implication). See Rule (cls) of Fig 3 of the "Associated Type Synonyms" paper.

I'm not arguing that the conditions in the published AT papers result in programs for which inference is non-terminating.

We're discussing here a possible AT extension for which inference is clearly non-terminating (unless we cut off type inference after n number of steps). Without these extensions you can't adequately encode the MonadReader class with ATs.

This addresses the first point. You didn't address the second. let me re-formuate: I think, you got the derivation wrong. You use the superclass implication the wrong way around. (Or do I misunderstand?)

I think the direction of the superclass rule is indeed wrong. But what about the following example: class C a class F a where type T a instance F [a] where type T [a] = a class (C (T a), F a) => D a where m :: a -> Int instance C a => D [a] where m _ = 42 If you now try to derive "D [Int]", you get ||- D [Int] subgoal: ||- C Int -- via Instance subgoal: ||- C (T [Int]) -- via Def. of T in F subgoal: ||- D [Int] -- Superclass Stefa

Iavor Diatchki

9:03 p.m.

Hello, On 5/3/06, Stefan Wehr wrote:

...

class C a class F a where type T a instance F [a] where type T [a] = a class (C (T a), F a) => D a where m :: a -> Int instance C a => D [a] where m _ = 42

If you now try to derive "D [Int]", you get

||- D [Int] subgoal: ||- C Int -- via Instance subgoal: ||- C (T [Int]) -- via Def. of T in F subgoal: ||- D [Int] -- Superclass

I do not follow this example. If we are trying to prove `D [Int]` we use the instance to reduce the problem to `C Int`, and then we fail because we cannot solve this goal. If we are trying to validate the second instance, then we need to prove that the context of the instance is sufficient to discharge the super class requirements: C a |- C (T [a]), F [a] We can solve `F [a]` using the instance, and (by using the definition of `T`) `C (T [a])` becomes `C a`, so we can solve it by assumption. -iavor

Stefan Wehr

9 May 9 May

8:44 a.m.

Iavor Diatchki wrote::

...

Hello,

On 5/3/06, Stefan Wehr wrote:

...
class C a class F a where type T a instance F [a] where type T [a] = a class (C (T a), F a) => D a where m :: a -> Int instance C a => D [a] where m _ = 42

If you now try to derive "D [Int]", you get

||- D [Int] subgoal: ||- C Int -- via Instance subgoal: ||- C (T [Int]) -- via Def. of T in F subgoal: ||- D [Int] -- Superclass

I do not follow this example.

If we are trying to prove `D [Int]` we use the instance to reduce the problem to `C Int`, and then we fail because we cannot solve this goal.

But there is also the equality `T [Int] = Int` which we could apply. Manuel pointed out in his reply that the inference algorithm doesn't do that, so you are right with respect to the algorithm. But it's still unclear if the algorithm is complete. Stefan

Iavor Diatchki

5:31 p.m.

Hello,

On 5/9/06, Stefan Wehr  wrote:
> >>     class C a
> >>     class F a where type T a
> >>     instance F [a] where type T [a] = a
> >>     class (C (T a), F a) => D a where m :: a -> Int
> >>     instance C a => D [a] where m _ = 42

> But there is also the equality `T [Int] = Int` which we could apply.
I think I see what you mean.  Here is what I worked out in case anyone
else didn't follow.
The axioms from the above declarations are:
1. forall a. F [a]
2. forall a. F [a] => T [a] = a
3. forall a. D a => C (T a) /\ F a
4. forall a. C a => D [a]
"proof"
goal: D [Int]
Using 4 with a = Int:
goal: C Int
Use (3 with a = [Int]) and (2 with a = Int) to get a new rule:
5. D [Int] /\ F [Int] => C Int /\ F [Int]
Using 5 and projection:
goal: F [Int], D [Int]
Using 1 with a = Int:
goal: D [Int]

Now we are back to where we started.  In this case we can notice this
and give up, but in general this might be tricky.

-Iavor

Manuel M T Chakravarty

8 May 8 May

9:38 p.m.

Stefan Wehr:

...

Manuel M T Chakravarty wrote::

...
Martin Sulzmann:

...
Manuel M T Chakravarty writes:

...
Martin Sulzmann:

...
A problem with ATs at the moment is that some terminating FD programs result into non-terminating AT programs.

Somebody asked how to write the MonadReader class with ATs: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014489.html

This requires an AT extension which may lead to undecidable type inference: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014609.html

The message that you are citing here has two problems:

1. You are using non-standard instances with contexts containing non-variable predicates. (I am not disputing the potential merit of these, but we don't know whether they apply to Haskell' at this point.) 2. You seem to use the super class implication the wrong way around (ie, as if it were an instance implication). See Rule (cls) of Fig 3 of the "Associated Type Synonyms" paper.

I'm not arguing that the conditions in the published AT papers result in programs for which inference is non-terminating.

We're discussing here a possible AT extension for which inference is clearly non-terminating (unless we cut off type inference after n number of steps). Without these extensions you can't adequately encode the MonadReader class with ATs.

This addresses the first point. You didn't address the second. let me re-formuate: I think, you got the derivation wrong. You use the superclass implication the wrong way around. (Or do I misunderstand?)

I think the direction of the superclass rule is indeed wrong. But what about the following example:

class C a class F a where type T a instance F [a] where type T [a] = a class (C (T a), F a) => D a where m :: a -> Int instance C a => D [a] where m _ = 42

If you now try to derive "D [Int]", you get

||- D [Int] subgoal: ||- C Int -- via Instance subgoal: ||- C (T [Int]) -- via Def. of T in F subgoal: ||- D [Int] -- Superclass

You are using `T [a] = a' *backwards*, but the algorithm doesn't do that. Or am I missing something? Manuel

Stefan Wehr

9 May 9 May

8:40 a.m.

Manuel M T Chakravarty wrote::

...

Stefan Wehr:

...
Manuel M T Chakravarty wrote::

...
Martin Sulzmann:

...
Manuel M T Chakravarty writes:

...
Martin Sulzmann:

...
A problem with ATs at the moment is that some terminating FD programs result into non-terminating AT programs.

Somebody asked how to write the MonadReader class with ATs: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014489.html

This requires an AT extension which may lead to undecidable type inference: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014609.html

The message that you are citing here has two problems:

1. You are using non-standard instances with contexts containing non-variable predicates. (I am not disputing the potential merit of these, but we don't know whether they apply to Haskell' at this point.) 2. You seem to use the super class implication the wrong way around (ie, as if it were an instance implication). See Rule (cls) of Fig 3 of the "Associated Type Synonyms" paper.

I'm not arguing that the conditions in the published AT papers result in programs for which inference is non-terminating.

We're discussing here a possible AT extension for which inference is clearly non-terminating (unless we cut off type inference after n number of steps). Without these extensions you can't adequately encode the MonadReader class with ATs.

This addresses the first point. You didn't address the second. let me re-formuate: I think, you got the derivation wrong. You use the superclass implication the wrong way around. (Or do I misunderstand?)

I think the direction of the superclass rule is indeed wrong. But what about the following example:

class C a class F a where type T a instance F [a] where type T [a] = a class (C (T a), F a) => D a where m :: a -> Int instance C a => D [a] where m _ = 42

If you now try to derive "D [Int]", you get

||- D [Int] subgoal: ||- C Int -- via Instance subgoal: ||- C (T [Int]) -- via Def. of T in F subgoal: ||- D [Int] -- Superclass

You are using `T [a] = a' *backwards*, but the algorithm doesn't do that. Or am I missing something?

Indeed, the equality is used backwards, so you aren't missing something. I tried to find an example for which both directions of the equality are relevant but failed. Of course, this is not a proof. Stefan

Martin Sulzmann

5 May 5 May

5:58 a.m.

Manuel M T Chakravarty writes:

...

Martin Sulzmann:

...
Manuel M T Chakravarty writes:

...
Martin Sulzmann:

...
A problem with ATs at the moment is that some terminating FD programs result into non-terminating AT programs.

Somebody asked how to write the MonadReader class with ATs: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014489.html

This requires an AT extension which may lead to undecidable type inference: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014609.html

The message that you are citing here has two problems:

1. You are using non-standard instances with contexts containing non-variable predicates. (I am not disputing the potential merit of these, but we don't know whether they apply to Haskell' at this point.) 2. You seem to use the super class implication the wrong way around (ie, as if it were an instance implication). See Rule (cls) of Fig 3 of the "Associated Type Synonyms" paper.

I'm not arguing that the conditions in the published AT papers result in programs for which inference is non-terminating.

We're discussing here a possible AT extension for which inference is clearly non-terminating (unless we cut off type inference after n number of steps). Without these extensions you can't adequately encode the MonadReader class with ATs.

This addresses the first point. You didn't address the second. let me re-formuate: I think, you got the derivation wrong. You use the superclass implication the wrong way around. (Or do I misunderstand?)

Superclass implication is reversed when performing type inference. In the same way that instance reduction is reserved. Here's the example again. 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 Of course, you'll argue that you apply some other inference methods. Though, I'm a bit doubtful whether you'll achieve any reasonably strong completeness of inference results. Martin

...

...
...
This plus the points that I mentioned in my previous two posts in this thread leave me highly unconvinced of your claims comparing AT and FD termination.

As argued earlier by others, we can apply the same 'tricks' to make FD inference terminating (but then we still don't know whether the constraint store is consistent!).

To obtain termination of type class inference, we'll need to be *very* careful that there's no 'devious' interaction between instances and type functions/improvement.

It would be great if you could come up with an improved analysis which rejects potentially non-terminating AT programs. Though, note that I should immediately be able to transfer your results to the FD setting based on the following observation:

I can turn any AT proof into a FD proof by (roughly)

- replace the AT equation F a=b with the FD constraint F a b - instead of firing type functions, we fire type improvement and instances - instead of applying transitivity, we apply the FD rule F a b, F a c ==> b=c

Similarly, we can turn any FD proof into a AT proof.

You may be able to encode AT proofs into FD proofs and vice versa, but that doesn't change the fact that some issues, as for example formation rules, are more natural, and I argue, more intuitive to the programmer in the AT setting. For example, with FDs you have to explain to the programmer the concept of weak coverage. With ATs, you don't need to do this, because the functional notation naturally leads people to write programs that obey weak coverage. Again, we want to write functional programs on the type level - after all FDs are *functional* dependencies - so, why use a relational notation?

If, as you say, FDs and ATs are equivalent on some scale of type theoretic power, let us use a functional notation in a functional language. At least, that is more orthogonal language design.

Manuel

Simon Peyton-Jones

8:25 a.m.

New subject: Superclass inference (was: termination for FDs and ATs)

| Superclass implication is reversed when performing type inference. | In the same way that instance reduction is reserved. | | Here's the example again. | | 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 | | Of course, you'll argue that you apply some other inference methods. Probably! Let me explain what GHC does today, and see if that helps. GHC tries to solve the following problem: Input: a set of "given" constraints G a set of "wanted" constraints W Output: evidence that Y can be deduced from G+instance decls During solving, GHC maintain two sets: the "given" set GG and the "wanted" set WW. XX is maintained closed under superclasses; that is, when adding a constraint (C t) to GG, I add all of C's superclasses. GG is initialised from G, closing under superclasses. WW is initialised to W, but is *not* closed under superclasses. Then we repeatedly pick a member of WW a) if it's in GG, we are done b) otherwise use an instance decl to simplify it, putting the new constraints back in WW c) if neither applies, error. In the pure inference case, the algorithm is slightly different: Input: a set of "wanted" constraints W Output: a minimal set of "wanted" constraints, G plus evidence for how to deduce W from G GG starts empty. The algorithm is the same as before, but in case (c) we add the constraint to GG (plus its superclasses). At the end, extract G from GG; we want all the things that were not the superclass-closure extras. -------------- The point of explaining this is to say that in your example, (D [a]) is part of Y, so GHC won't add D [a]'s superclasses in the first place, and the problem you describe doesn't arise. I don't know whether that is luck, good judgement, or perhaps wrong. --------------- In the presence of ATs, I think that when adding a member to XX, or to YY, we need to normalise the types wrt AT rewrites (a confluent terminating process) first. But that should do it. (Of course, I have proved nothing.) Simon

Manuel M T Chakravarty

29 Apr 29 Apr

9:49 p.m.

Ross Paterson:

...

To ensure termination with FDs, there is a proposed restriction that an instance that violates the coverage condition must have a trivial instance improvement rule. Is the corresponding restriction also required for ATs, namely that an associated type synonym definition may only contain another associated type synonym at the outermost level? If not, wouldn't the non-terminating example from the FD-CHR paper (ex. 6, adapted below) also be a problem for ATs?

class Mul a b where type Result a b (.*.) :: a -> b -> Result a b

instance Mul a b => Mul a [b] where type Result a b = [Result a b] x .*. ys = map (x .*.) ys

f = \ b x y -> if b then x .*. [y] else y

This definition is not quite correct. The instance would be instance Mul a b => Mul a [b] where type Result a [b] = [Result a b] -- second argument is different x .*. ys = map (x .*.) ys The arguments to the ATs, in an instance def, need to coincide with the class parameters. So, in f, we get the context Mul a [b], Result a [b] = b (*) which reduces to Mul a b, [Result a b] = b at which point type inference *terminates*. So, we get the following type for f f :: (Mul a b, [Result a b] = b) => Bool -> a -> b -> [Result a b] Given the instance definitions of that example, you can never satisfy the equality [Result a b] = b, and hence, never apply the function f. In other words, AT type inference sidesteps the problem by just not committing on whether f's type is satisfiable. It rather gives a condition under which f can be applied, namely [Result a b] = b. That condition will then be checked at any application site. So, clearly termination for ATs and FDs is *not* the same. It's quite interesting to have a close look at where the difference comes from. The FD context corresponding to (*) above is Mul a [b] b Improvement gives us Mul a [[c]] [c] with b = [c] which simplifies to Mul a [c] c which is where we loop. The culprit is really the new type variable c, which we introduce to represent the "result" of the type function encoded by the type relation Mul. So, this type variable is an artifact of the relational encoding of what really is a function, which brings me back to my fundamental objection to FDs: We are functional, not logic programmers. Manuel

Iavor Diatchki

1 May 1 May

6:31 p.m.

Hello, On 4/29/06, Manuel M T Chakravarty wrote:

...

instance Mul a b => Mul a [b] where type Result a [b] = [Result a b] -- second argument is different x .*. ys = map (x .*.) ys

The arguments to the ATs, in an instance def, need to coincide with the class parameters.

So, in f, we get the context

Mul a [b], Result a [b] = b (*)

which reduces to

Mul a b, [Result a b] = b

at which point type inference *terminates*.

Perhaps I misunderstand something, but terminating is not always an option. For example, if we are type checking something with a type signature, or an expression where the monomorphism restriction kicks in, we have to discharge the predicates or reject the program. (This is why the example on the wiki is written with lambdas).

...

So, we get the following type for f

f :: (Mul a b, [Result a b] = b) => Bool -> a -> b -> [Result a b]

Given the instance definitions of that example, you can never satisfy the equality [Result a b] = b, and hence, never apply the function f.

What do you think should happen if I add the following definition as well? g :: (Mul a b) => Bool -> a -> b -> [Result a b] g = f It appears that the "right" thing would be to reject this program, because we cannot solve the constraint "[Result a b] = b". However, in general this may require some fancy reasoning, which is why naive implementations simply loop.

...

So, clearly termination for ATs and FDs is *not* the same. I assume (appologies if this is incorrect) that when you are talking about termintion of ATs or FDs you mean the terminations of particular algorithms for solving predicates arising in both systems. I am not sure if ATs somehow make the problem simpler, but certainly choosing to delay predicates rather than solve them is an option available to both systems (modulo type signatures, as I mentioned above).

-Iavor

Manuel M T Chakravarty

3 May 3 May

1:41 a.m.

Iavor Diatchki:

...

On 4/29/06, Manuel M T Chakravarty wrote:

...
instance Mul a b => Mul a [b] where type Result a [b] = [Result a b] -- second argument is different x .*. ys = map (x .*.) ys

The arguments to the ATs, in an instance def, need to coincide with the class parameters.

So, in f, we get the context

Mul a [b], Result a [b] = b (*)

which reduces to

Mul a b, [Result a b] = b

at which point type inference *terminates*.

Perhaps I misunderstand something, but terminating is not always an option. For example, if we are type checking something with a type signature, or an expression where the monomorphism restriction kicks in, we have to discharge the predicates or reject the program. (This is why the example on the wiki is written with lambdas).

If we require a monomorphic signature at this point, we will reject the program, as the inferred signature quantifies over two type variables.

...

...
So, we get the following type for f

f :: (Mul a b, [Result a b] = b) => Bool -> a -> b -> [Result a b]

Given the instance definitions of that example, you can never satisfy the equality [Result a b] = b, and hence, never apply the function f.

What do you think should happen if I add the following definition as well?

g :: (Mul a b) => Bool -> a -> b -> [Result a b] g = f

It appears that the "right" thing would be to reject this program, because we cannot solve the constraint "[Result a b] = b". However, in general this may require some fancy reasoning, which is why naive implementations simply loop.

The definition of g will indeed be rejected. However, no fancy reasoning is required. Section 5.4 of the Associated Type Synonyms paper defines polytype subsumption for signatures including associated types. Subsumption is the standard way of determining whether a type signature is valid. (To cover this point, the term syntax in the Associated Type Synonym paper, Figure 1, includes signature annotations.)

...

...
So, clearly termination for ATs and FDs is *not* the same. I assume (appologies if this is incorrect) that when you are talking about termintion of ATs or FDs you mean the terminations of particular algorithms for solving predicates arising in both systems.

You are of course right. I admit that I am guilty of the same imprecision as most of the contributions to the AT-FD discussion. We are talking of ATs and FDs as if there is only one system each, although there are two families of systems.

...

I am not sure if ATs somehow make the problem simpler, but certainly choosing to delay predicates rather than solve them is an option available to both systems (modulo type signatures, as I mentioned above).

Let's say I have never seen a proposal for FDs that delays predicates in the way that we proposed for ATs. One nice property of the system proposed for ATs is that it arises form a generalisation of the occurs check that we have to do in Hindley-Milner type inference anyway. I suspect that for FDs you have to invoke some extra machinery. Manuel

Ross Paterson

1 May 1 May

11:26 p.m.

Thanks for clarifying this. On Sat, Apr 29, 2006 at 05:49:16PM -0400, Manuel M T Chakravarty wrote:

...

So, we get the following type for f

f :: (Mul a b, [Result a b] = b) => Bool -> a -> b -> [Result a b]

Given the instance definitions of that example, you can never satisfy the equality [Result a b] = b, and hence, never apply the function f.

That would be the case if the definition were f b x y = if b then x .*. [y] else y You'd assign f a type with unsatisfiable constraints, obtaining termination by deferring the check. But the definition f = \ b x y -> if b then x .*. [y] else y will presumably be rejected, because you won't infer the empty context that the monomorphism restriction demands. So the MR raises the reverse question: can you be sure that every tautologous constraint is reducible?

...

So, clearly termination for ATs and FDs is *not* the same. It's quite interesting to have a close look at where the difference comes from. The FD context corresponding to (*) above is

Mul a [b] b

Improvement gives us

Mul a [[c]] [c] with b = [c]

which simplifies to

Mul a [c] c

which is where we loop. The culprit is really the new type variable c, which we introduce to represent the "result" of the type function encoded by the type relation Mul. So, this type variable is an artifact of the relational encoding of what really is a function,

It's an artifact of the instance improvement rule, but one could define a variant of FDs without that rule. Similarly one could have a variant of ATs that would attempt to solve the equation [Result a b] = b by setting b = [c] for a fresh variable c. In both cases there is the same choice: defer reduction or try for more precise types at the risk of non-termination for instances like these.

Martin Sulzmann

2 May 2 May

4:31 a.m.

Ross Paterson writes:

...

Thanks for clarifying this.

On Sat, Apr 29, 2006 at 05:49:16PM -0400, Manuel M T Chakravarty wrote:

...
So, we get the following type for f

f :: (Mul a b, [Result a b] = b) => Bool -> a -> b -> [Result a b]

Given the instance definitions of that example, you can never satisfy the equality [Result a b] = b, and hence, never apply the function f.

That would be the case if the definition were

f b x y = if b then x .*. [y] else y

You'd assign f a type with unsatisfiable constraints, obtaining termination by deferring the check. But the definition

f = \ b x y -> if b then x .*. [y] else y

will presumably be rejected, because you won't infer the empty context that the monomorphism restriction demands. So the MR raises the reverse question: can you be sure that every tautologous constraint is reducible?

...
So, clearly termination for ATs and FDs is *not* the same. It's quite interesting to have a close look at where the difference comes from. The FD context corresponding to (*) above is

Mul a [b] b

Improvement gives us

Mul a [[c]] [c] with b = [c]

which simplifies to

Mul a [c] c

which is where we loop. The culprit is really the new type variable c, which we introduce to represent the "result" of the type function encoded by the type relation Mul. So, this type variable is an artifact of the relational encoding of what really is a function,

It's an artifact of the instance improvement rule, but one could define a variant of FDs without that rule. Similarly one could have a variant of ATs that would attempt to solve the equation [Result a b] = b by setting b = [c] for a fresh variable c. In both cases there is the same choice: defer reduction or try for more precise types at the risk of non-termination for instances like these.

I agree. At one stage, GHC (forgot which version) behaved similarly compared to Manuel's AT inference strategy. Manuel may have solved the termination problem (by stopping after n number of steps). Though, we still don't know yet whether the constraints are consistent. One of the reasons why FD *and* AT inference is tricky is because inference may be non-terminating although - type functions/FD improvements are terminating - type classes are terminating We'll need a more clever analysis (than a simple occurs check) to reject 'dangerous' programs. Martin

Ross Paterson

3 May 3 May

8:36 a.m.

On Tue, May 02, 2006 at 12:26:48AM +0100, Ross Paterson wrote:

...

So the MR raises the reverse question: can you be sure that every tautologous constraint is reducible?

I think the answer is no. Consider: class C a where type Result a method :: a -> Result a instance C (Maybe a) where { type Result (Maybe a) = Bool f = \ b x -> if b then Just (method x) else x The AT algorithm will stop after inferring the following type for f: (a = Maybe (Result a), C a) => Bool -> a -> a Since the constraint set is non-empty, this definition will be rejected by the monomorphism restriction. However, this constraint set has exactly the same set of solutions as a = Maybe Bool, which is trivially solvable. (The corresponding FD version will reduce to this, thanks to instance improvement.)

Simon Peyton-Jones

4 May 4 May

1 p.m.

| On Tue, May 02, 2006 at 12:26:48AM +0100, Ross Paterson wrote: | > So the MR raises the reverse | > question: can you be sure that every tautologous constraint is reducible? | | I think the answer is no. Consider: | | class C a where | type Result a | method :: a -> Result a | | instance C (Maybe a) where { | type Result (Maybe a) = Bool | | f = \ b x -> if b then Just (method x) else x | | The AT algorithm will stop after inferring the following type for f: | | (a = Maybe (Result a), C a) => Bool -> a -> a | | Since the constraint set is non-empty, this definition will be rejected | by the monomorphism restriction. Actually, it won't. The spec just says that the function is monomorphic in 'a'. That is, 'a' can be instantiated only one way. So if f is called, say (f True True), then that fixes 'a' to be Bool and all is well. Only if f is exported (with no calls inside the module) will the program be rejected, and even then it'll be rejected on the grounds that 'a' is ambiguous. But these are details. Your general point is well taken: the FD improvement rule will infer f :: Bool -> Bool -> Bool without seeing any calls. Simon

Ross Paterson

2:51 p.m.

On Thu, May 04, 2006 at 02:00:33PM +0100, Simon Peyton-Jones wrote:

...

Actually, it won't. The spec just says that the function is monomorphic in 'a'. That is, 'a' can be instantiated only one way. So if f is called, say (f True True), then that fixes 'a' to be Bool and all is well.

Oops. Still, if the class can have two parameters, I could define Result (Maybe a) b = [b] instead of Bool and probably get a contrast between polymorphism and monomorphism in b.

Simon Peyton-Jones

1:22 p.m.

This has been an interesting thread, starting here http://www.haskell.org//pipermail/haskell-prime/2006-April/001466.html Here is what I conclude so far. 1. As Manuel explained, in the AT formulation it's possible to avoid non-termination by suspending (leave unsolved) any equality constraint of form (a = ty) where 'a' appears free in a type argument to an associated type in 'ty'. http://www.haskell.org//pipermail/haskell-prime/2006-April/001501.html 2. This solution is not the same as stopping after a fixed number N of iterations. It's more principled than that. 3. We may thereby infer a type that can never be satisfied, so that the function cannot be called. (In Martin's vocabulary, "the constraints are inconsistent".) Not detecting the inconsistency immediately means that error messages may be postponed. Adding a type signature would fix the problem, though. 4. As Ross shows below, we may thereby infer a qualified type when there is a unique, completely un-qualified solution. But that does little harm, I think. The only time you can even tell it has happened is if (a) the defn falls under the MR (in particular, no type signature is given), (b) the function is exported, and (c) it is not called inside the module. 5. The effect is akin to dropping the instance-improvement CHR arising from the corresponding FD. But we can't drop the instance-improvement CHR because then lots of essential improvement would fail to take place. It is not obvious to me how to translate the rule I give in (1) into the CHR framework, though doubtless it is possible. 6. I don't think we yet know whether *all* non-termination is thereby eliminated from the AT-inference story. Manuel and Martin and I are starting to write down the formal story for an AT system that covers both data types, type synonyms, and various other small extensions to ATs, so we hope to find out soon. (In this world, "small extensions" are easy to describe, but sometimes have a big effect. So formalising it is important.) 7. In particular, Martin writes "We'll need a more clever analysis (than a simple occurs check) to reject 'dangerous' programs." But so far I don't see why we might need a more clever analysis than the rule I describe in (1) above. I'm not denying that such a thing might exist, but I wonder if you have anything in mind? http://www.haskell.org//pipermail/haskell-prime/2006-May/001514.html Simon | -----Original Message----- | From: haskell-prime-bounces@haskell.org [mailto:haskell-prime-bounces@haskell.org] On Behalf Of | Ross Paterson | Sent: 03 May 2006 09:37 | To: haskell-prime@haskell.org | Subject: Re: termination for FDs and ATs | | On Tue, May 02, 2006 at 12:26:48AM +0100, Ross Paterson wrote: | > So the MR raises the reverse | > question: can you be sure that every tautologous constraint is reducible? | | I think the answer is no. Consider: | | class C a where | type Result a | method :: a -> Result a | | instance C (Maybe a) where { | type Result (Maybe a) = Bool | | f = \ b x -> if b then Just (method x) else x | | The AT algorithm will stop after inferring the following type for f: | | (a = Maybe (Result a), C a) => Bool -> a -> a | | Since the constraint set is non-empty, this definition will be rejected | by the monomorphism restriction. | | However, this constraint set has exactly the same set of solutions as | a = Maybe Bool, which is trivially solvable. (The corresponding FD | version will reduce to this, thanks to instance improvement.) | | _______________________________________________ | Haskell-prime mailing list | Haskell-prime@haskell.org | http://haskell.org/mailman/listinfo/haskell-prime

Claus Reinke

3:01 p.m.

...

1. As Manuel explained, in the AT formulation it's possible to avoid non-termination by suspending (leave unsolved) any equality constraint of form (a = ty) where 'a' appears free in a type argument to an associated type in 'ty'.

as both Manuel and myself have pointed out, ensuring that the occurs check covers type-functions as well is not only possible, but implied by working on top of an HM type-system. whether to leave open constraints that run foul of this check, or whether to reject them early, knowing that they can't be fulfilled, is a separate matter. as Manuel explained, the AT system leaves them open because the unification is semantic, ie. further reduction of the type-functions in such equations might eliminate the recursive variable references. as long as the type-functions remain open, the system cannot know whether the constraints can be fulfilled (analogously for an FD system).

...

2. This solution is not the same as stopping after a fixed number N of iterations. It's more principled than that.

indeed.

...

3. We may thereby infer a type that can never be satisfied, so that the function cannot be called. (In Martin's vocabulary, "the constraints are inconsistent".) Not detecting the inconsistency immediately means that error messages may be postponed. Adding a type signature would fix the problem, though.

see above. forcing the type by a signature closes the set of type function definitions that may be used (further extension is possible, but not visible at the point of the signature), by which means delayed constraints may be turned into errors (but note that without the signature/MR, there might not be any error, just some type-function definition not yet visible).

...

5. The effect is akin to dropping the instance-improvement CHR arising from the corresponding FD. But we can't drop the instance-improvement CHR because then lots of essential improvement would fail to take place. It is not obvious to me how to translate the rule I give in (1) into the CHR framework, though doubtless it is possible.

the effect is that of conditionally disabling the instance-improvement CHR, not dropping it completely. improvement CHR introduce unifications, and HM implies that unifications are guarded by occurs-checks, so the CHRs for improvement should be guarded by occurs-checks. that should disable these CHR in the same cases in which the occurs-check disables the type-functions in the AT case. note that the FD-CHR for the class also introduce a unification, hence need to be guarded the same way. cheers, claus

Martin Sulzmann

5 May 5 May

5:58 a.m.

In more detail, here's the issue I see. The AT inference system doesn't exhaustively apply all rules, rather, the AT inferencer stops once we encounter a 'cycle' such as T a = a where T is a type function constructor. The important question is whether this will retain *complete* type inference? For example, in case of type annotations we need to test for equivalence among constraints. In the "A Theory of Overlaoding" and FD-CHR paper we develop a equivalence check by exhaustively applying rules until we reach a canonical normal form. This check is complete if the rules are terminating and confluent (roughly). If the rules are non-terminating, we obviously can't apply the rules exhaustively. Howver, then it's unclear whether the equivalence check is still complete. You'll need to convince me that the AT inferencer computes canonical (?) normal forms which are good enough to obtain a complete equivalence checker. My guess is that any positive result in this direction suggests that we should have immediately rejected a constraint such as T a = a in the first place. Martin Simon Peyton-Jones writes:

...

This has been an interesting thread, starting here

http://www.haskell.org//pipermail/haskell-prime/2006-April/001466.html

Here is what I conclude so far.

1. As Manuel explained, in the AT formulation it's possible to avoid non-termination by suspending (leave unsolved) any equality constraint of form (a = ty) where 'a' appears free in a type argument to an associated type in 'ty'.

http://www.haskell.org//pipermail/haskell-prime/2006-April/001501.html

2. This solution is not the same as stopping after a fixed number N of iterations. It's more principled than that.

3. We may thereby infer a type that can never be satisfied, so that the function cannot be called. (In Martin's vocabulary, "the constraints are inconsistent".) Not detecting the inconsistency immediately means that error messages may be postponed. Adding a type signature would fix the problem, though.

4. As Ross shows below, we may thereby infer a qualified type when there is a unique, completely un-qualified solution. But that does little harm, I think. The only time you can even tell it has happened is if (a) the defn falls under the MR (in particular, no type signature is given), (b) the function is exported, and (c) it is not called inside the module.

5. The effect is akin to dropping the instance-improvement CHR arising from the corresponding FD. But we can't drop the instance-improvement CHR because then lots of essential improvement would fail to take place. It is not obvious to me how to translate the rule I give in (1) into the CHR framework, though doubtless it is possible.

6. I don't think we yet know whether *all* non-termination is thereby eliminated from the AT-inference story. Manuel and Martin and I are starting to write down the formal story for an AT system that covers both data types, type synonyms, and various other small extensions to ATs, so we hope to find out soon. (In this world, "small extensions" are easy to describe, but sometimes have a big effect. So formalising it is important.)

7. In particular, Martin writes "We'll need a more clever analysis (than a simple occurs check) to reject 'dangerous' programs." But so far I don't see why we might need a more clever analysis than the rule I describe in (1) above. I'm not denying that such a thing might exist, but I wonder if you have anything in mind?

http://www.haskell.org//pipermail/haskell-prime/2006-May/001514.html

Simon

| -----Original Message----- | From: haskell-prime-bounces@haskell.org [mailto:haskell-prime-bounces@haskell.org] On Behalf Of | Ross Paterson | Sent: 03 May 2006 09:37 | To: haskell-prime@haskell.org | Subject: Re: termination for FDs and ATs | | On Tue, May 02, 2006 at 12:26:48AM +0100, Ross Paterson wrote: | > So the MR raises the reverse | > question: can you be sure that every tautologous constraint is reducible? | | I think the answer is no. Consider: | | class C a where | type Result a | method :: a -> Result a | | instance C (Maybe a) where { | type Result (Maybe a) = Bool | | f = \ b x -> if b then Just (method x) else x | | The AT algorithm will stop after inferring the following type for f: | | (a = Maybe (Result a), C a) => Bool -> a -> a | | Since the constraint set is non-empty, this definition will be rejected | by the monomorphism restriction. | | However, this constraint set has exactly the same set of solutions as | a = Maybe Bool, which is trivially solvable. (The corresponding FD | version will reduce to this, thanks to instance improvement.) | | _______________________________________________ | Haskell-prime mailing list | Haskell-prime@haskell.org | http://haskell.org/mailman/listinfo/haskell-prime _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime

Simon Peyton-Jones

7:42 a.m.

| The important question is whether this will retain *complete* type | inference? For example, in case of type annotations we need to | test for equivalence among constraints. An excellent question. Here's an example, adapted from Ross: class C a where type Result a method :: a -> Result a instance C (Maybe a) where type Result (Maybe a) = Bool g :: (a->a) -> Int g f = 3 w ::Int w = g (\b x -> if b then Just (method x) else x) Now, as Ross pointed out, the (\b x->...) expression has inferred type (a = Maybe (Result a), C a) => Bool -> a -> a Alas, g simply discards its argument, so there are no further constraints on 'a'. I think Martin would argue that type inference should succeed with a=Bool, since there is exactly one solution. Is this an example of what you mean? However, as a programmer I would not be in the least upset if inference failed, and I was required to add a type signature. I don't expect type inference algorithms to "guess", or to solve recursive equations, and that's what is happening here. (Notice that it's quite hard to set up this problem. First you need a program whose equality constraints become recursive. Then you need to arrange that the type variables in the recursion are not mentioned elsewhere -- if they were, they'd be instantiated there, and everything would be ok.) What I am less sure of is how to *specify* the type system so that it describes these hard-to-infer programs as illegal. Presumably it's a question of setting up the entailment system so that it has limited rules of deduction -- more limited than first order logic. Simon

Ross Paterson

8:27 a.m.

On Fri, May 05, 2006 at 08:42:12AM +0100, Simon Peyton-Jones wrote:

...

Alas, g simply discards its argument, so there are no further constraints on 'a'. I think Martin would argue that type inference should succeed with a=Bool, since there is exactly one solution. Is this an example of what you mean?

Actually a = Maybe Bool

...

However, as a programmer I would not be in the least upset if inference failed, and I was required to add a type signature. I don't expect type inference algorithms to "guess", or to solve recursive equations, and that's what is happening here.

I think Martin is assuming the current Haskell algorithm: infer the type of the function and then check that it's subsumed by the declared type, while you're assuming a bidirectional algorithm. That makes a big difference in this case, but you still do subsumption elsewhere, so Martin's requirement for normal forms will still be present.

Martin Sulzmann

10:12 a.m.

Ross Paterson writes:

...

On Fri, May 05, 2006 at 08:42:12AM +0100, Simon Peyton-Jones wrote:

...
Alas, g simply discards its argument, so there are no further constraints on 'a'. I think Martin would argue that type inference should succeed with a=Bool, since there is exactly one solution. Is this an example of what you mean?

Actually a = Maybe Bool

...
However, as a programmer I would not be in the least upset if inference failed, and I was required to add a type signature. I don't expect type inference algorithms to "guess", or to solve recursive equations, and that's what is happening here.

I think Martin is assuming the current Haskell algorithm: infer the type of the function and then check that it's subsumed by the declared type, while you're assuming a bidirectional algorithm. That makes a big difference in this case, but you still do subsumption elsewhere, so Martin's requirement for normal forms will still be present.

A quick reply: Subsumption among two type schemes boilds down to testing whether (roughly) Annotation_Constraint implies Infered_Constraint ^^^^ ^^^^ given demanded iff Annotation_Constraint <-> Annotation_Constraint /\ Infered_Constraint So, of course the latter is more suitable for testing than the former. (effectively, we push 'given' type information down the abstract syntax tree). In any case, it's entirly unclear to me whether 'stopping' the AT inference process at some stage will guarantee complete inference (in the presence of type annotations etc). Martin

6997

Age (days ago)

7012

Last active (days ago)

List overview

Download

30 comments

7 participants

participants (7)

Claus Reinke
Iavor Diatchki
Manuel M T Chakravarty
Martin Sulzmann
Ross Paterson
Simon Peyton-Jones
Stefan Wehr

termination for FDs and ATs

tags

participants (7)