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 _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell