On Sun, 17 Aug 2003 [EMAIL PROTECTED] wrote:
> > > I defined type recursion and naturals as > > > >newtype Mu f = In {unIn :: f (Mu f)} > > >data N f = S f | Z > > >type Nat = Mu N > > > 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. > > 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 > > *Main> show (In (S (In (S (In Z))))) > "S S Z" > > This solution is akin to that of breaking the type recursion when > defining the fixpoint combinator fix. Only here we face the recursion > on constraints. I believe the same solution should work for the > Observable class. You didn't post the definition of the Observable > class, so I couldn't test my claim. > > Flags used: > ghci -fglasgow-exts -fallow-undecidable-instances /tmp/a.hs Thanks for this solution. You can get HOOD from the libraries page on haskell.org. It (Observe.lhs) defines observable. I still want the instance (Show a) => Show (N a) for showing all the intermediate values that you get with the recursion combinators, so I think I'll need to add -fallow-overlapping-instances. I still think it would be useful to add a goal as an axiom while trying to prove the anteceedents of any derivation rule that applies. Equivalently, you could consider it accepting regular derivations rather than just finite derivations. I think allowing regular derivations might make it possible to find more liberal constraints on the form of instances that would still insure the decidability of solving for instances. If types the form of types are restricted to explicit recursion, varients, and tuples: T := mu X.T | <T1|T2|..|Tn> | (T1,T2,..,Tn) Then deriving an instance is decidable so long as the context of an instance mentions only subexpressions of the head. (because there are only a finite number of distinct subexpressions, and each time we use a rule we add one to our set of axioms) Of course it breaks down if you allow type operators... Are there any papers I should read if I want to find something useful in this vein? I just finished grabbing everything relevant in the first three pages or so of googling for "type classes". The only book on type theory I have is Pierce's "Types and Programming Languages", and I have nothing on logic. I have a vauge idea coinduction might be useful, and an even hazier idea that we might be able to get away with some non-regular derivation trees. Interesting? Useful? Should go to haskell-cafe? Thanks for any advice Brandon _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell