Brandon writes | An application of Mu should be showable if the functor maps showable types | to showable types, so the most natural way to define the instance seemed | to be | | instance (Show a => Show (f a)) => Show (Mu f) where | show (In x) = show x | | Of course that constraint didn't work Interesting. This point is coming up more often! You'll find another example of the usefulness of constraints like the one in your instance decl in "Derivable Type Classes" (towards the end). http://research.microsoft.com/~simonpj/Papers/derive.htm Valery Trifonov has a beautiful paper at the upcoming Haskell workshop 2003 that shows how to code around the lack of universally quantified constraints. I strongly suggest you take a look at it, but it doesn't seem to be online yet. | Constraint Stack Overflow: | Observable (N (Mu N)) | Observable (Mu N) | Observable (N (Mu N)) | Observable (Mu N) | ... | | I expected that that constraint solver would realize it could construct a | dictionary transformer with a type like Observer Nat -> Observer Nat and | take the fixed point to get an instance for Nat. I haven't looked at the | implementation, but it seems like it would be easy to add the constraint | we are trying to derive to the list of assumptions when trying to | construct all the anteceedents of an instance declaration. That's true, I believe, but a) it's a bit fragile (a sort of half-way house to solving the halting problem) b) at the moment dictionaries have the property that you can always evaluate them using call-by-value; if they could be recursively defined (as you suggest) that would no longer be the case Mind you, GHC doesn't currently take advantage of (b), so maybe it should be ignored. Adding the current goal as an axiom would not be difficult, but I don't have time to do it today! Is anyone else interested in such a feature? Oleg wrote
Well, it can if we write it in a bit different way:
instance (Show (f (Mu f))) => Show (Mu f) where show (In x) = show x
instance Show (N (Mu N)) where show Z = "Z" show (S k) = "S "++show k
That's very clever, Oleg; I hadn't thought of that. But again, it's fragile isn't it? You are dicing with non-termination if you have instance declarations where the stuff before the '=>' is more complicated than the stuff after the '=>'. A less carefully written instance for Show (N (Mu N)) would make the type checker loop. Simon
On Fri, 22 Aug 2003, Simon Peyton-Jones wrote:
Brandon writes
| An application of Mu should be showable if the functor maps showable types | to showable types, so the most natural way to define the instance seemed | to be | | instance (Show a => Show (f a)) => Show (Mu f) where | show (In x) = show x | | Of course that constraint didn't work
Interesting. This point is coming up more often! You'll find another example of the usefulness of constraints like the one in your instance decl in "Derivable Type Classes" (towards the end). http://research.microsoft.com/~simonpj/Papers/derive.htm
Valery Trifonov has a beautiful paper at the upcoming Haskell workshop 2003 that shows how to code around the lack of universally quantified constraints. I strongly suggest you take a look at it, but it doesn't seem to be online yet.
| Constraint Stack Overflow: | Observable (N (Mu N)) | Observable (Mu N) | Observable (N (Mu N)) | Observable (Mu N) | ... | | I expected that that constraint solver would realize it could construct a | dictionary transformer with a type like Observer Nat -> Observer Nat and | take the fixed point to get an instance for Nat. I haven't looked at the | implementation, but it seems like it would be easy to add the constraint | we are trying to derive to the list of assumptions when trying to | construct all the anteceedents of an instance declaration.
That's true, I believe, but a) it's a bit fragile (a sort of half-way house to solving the halting problem) b) at the moment dictionaries have the property that you can always evaluate them using call-by-value; if they could be recursively defined (as you suggest) that would no longer be the case
Mind you, GHC doesn't currently take advantage of (b), so maybe it should be ignored. Adding the current goal as an axiom would not be difficult, but I don't have time to do it today! Is anyone else interested in such a feature?
I would like to try making this change, but I couldn't puzzle out enough of the type class system the last time I looked. I would appreciate advice, references, or even just a list of the relevant modules. With regard to a), taking our goal as an axiom while searching for a derivation can be expressed in language that sounds less ad-hoc: accept regular instance declarations. Unfortunately I don't have a useful syntatic condition on instance declarations that insures termination of typechecking. If types are restriced to products, sums, and explicit recursion, then termination is ensured if we restrict the assumtions of a declaration to instances for subexpressions of the type we are declaring an instance for (there are only a finite number of subexpressions times a finite number of classes, and one is added each time we apply a rule). I haven't made any progress if type operators are allowed, and I don't have any simple check whether a Haskell type expression can be represented without type operators. I was hoping to get normalization of type expressions from the simple kinding, but recursive operator definitions break that. On the other hand, allowing implications in a context is more general. Adding the conclusion of a rule as an axiom while trying to derive the context is equivalent to modifying every declaration instance (ct1,ct2,ct3) => goal to read instance (goal=>ct1,goal=>ct2,goal=>ct3) => goal. The methods defined in the instance should still typecheck, if we use the context and the conclusion of the instance declaration when checking the method definitions. It's worth noting that if we have a restriction on the form of instance declarations that ensures decidability of type checking, then generalizing the form of instance declarations from (conclusion, .., conclusion) => instance conclusion to (ctx => conclusion, .. , ctx => conclusion) => instance conclusion doesn't break decidability, as long as 1) the instance would still be syntactically valid if we replaced all the implications in the context with their right hand side 2) all the implications in the context also satisfy the syntatctic validity rule. Unfortunately the only restriction I know of (the one from the Haskell Report) isn't very useful even with generalized contexts. On the other hand, allowing regular derivation widens the space of safe instances, but doesn't give any guidance toward restrictions that ensure safety. Allowing implications in contexts even allows us to derive instances for some irregular types: data Twice f x = T (f (f x)) data Growing f = G (f (Growing (Twice f))) data Id x = Id x Suppose we want to define instances that will imply Show (Growing Id). Growing Id is an irregular type so allowing irregular derivations isn't enough, but the following instances are acceptable instance (forall a.Show a => Show f a,Show x) => Show (Twice f x) where show (T ffx) = show "T "++show ffx instance (forall a.Show a => Show f a) => Show (Growing f) where show (G fgtf) = show "G "++show fgtf instance (Show a) => Show (Id a) where show (Id x) = show "Id "++show x
Oleg wrote
Well, it can if we write it in a bit different way:
instance (Show (f (Mu f))) => Show (Mu f) where show (In x) = show x
instance Show (N (Mu N)) where show Z = "Z" show (S k) = "S "++show k
That's very clever, Oleg; I hadn't thought of that. But again, it's fragile isn't it? You are dicing with non-termination if you have instance declarations where the stuff before the '=>' is more complicated than the stuff after the '=>'. A less carefully written instance for Show (N (Mu N)) would make the type checker loop.
Simon
For "nice" f, Mu f can be represented by a mu type (now I understand what was meant by "arbitrary (regular) base functor"), and the instance satisfies the safety condition for mu types, so it's relatively safe. Of course, if you use a pathological value of F the typechecker can still diverge. Brandon
On Thu, 2003-08-28 at 13:10, Brandon Michael Moore wrote:
Unfortunately I don't have a useful syntatic condition on instance declarations that insures termination of typechecking. If types are restriced to products, sums, and explicit recursion, then termination is ensured if we restrict the assumtions of a declaration to instances for subexpressions of the type we are declaring an instance for (there are only a finite number of subexpressions times a finite number of classes, and one is added each time we apply a rule). I haven't made any progress if type operators are allowed, and I don't have any simple check whether a Haskell type expression can be represented without type operators. I was hoping to get normalization of type expressions from the simple kinding, but recursive operator definitions break that.
I think some of David McAllester's papers from about 1990-1994 may be relevant here. He has several papers on deciding when sets of inference rules are terminating, or terminating in polynomial time. (He applies this in the context of automated theorem proving, but it should apply perfectly well to type class inference as well.) Carl Witty
On 28 Aug 2003, Carl Witty wrote:
On Thu, 2003-08-28 at 13:10, Brandon Michael Moore wrote:
Unfortunately I don't have a useful syntatic condition on instance declarations that insures termination of typechecking. If types are restriced to products, sums, and explicit recursion, then termination is ensured if we restrict the assumtions of a declaration to instances for subexpressions of the type we are declaring an instance for (there are only a finite number of subexpressions times a finite number of classes, and one is added each time we apply a rule). I haven't made any progress if type operators are allowed, and I don't have any simple check whether a Haskell type expression can be represented without type operators. I was hoping to get normalization of type expressions from the simple kinding, but recursive operator definitions break that. Rather, regularity of the resulting types, or something like that. We can always evaluate a type expression to head normal form, but the complete expansion of a type can be irregular.
I think some of David McAllester's papers from about 1990-1994 may be relevant here. He has several papers on deciding when sets of inference rules are terminating, or terminating in polynomial time. (He applies this in the context of automated theorem proving, but it should apply perfectly well to type class inference as well.)
Thanks, this is interesting work. I've read "New Results on Local Inference Relations", and skimmed a few other papers. Too bad I can't see how to use it. Determining locality seemed to require a global analysis, and superficial rules look too restrictive for instance declarations. Some of the ideas could probably be adapted to prove termination (and bounds) for sets of rules if the anteceedents of rules mention only subterms of the conclusion. It's pretty trivial to prove that regular terms have regular derivations if any, but I haven't looked for good bounds. It looked to me like most of the results assumed that terms were finite, but most of it should carry over to regular terms. I don't think it would be easy to extend to irregular terms, even if I had a good characterication of Haskell types. Does anyone know of any results in that direction? Simple kinds give you head normalization, but I don't know how to describe the sorts of terms that end up as constructor arguments as you evaluate type expressions. I want some reasonable characterization of the sort of trees you get when you evaluate type expressions completely. Does anyone know of papers or books on this? Thanks Brandon
participants (3)
-
Brandon Michael Moore -
Carl Witty -
Simon Peyton-Jones