On Sun, 17 Aug 2003 oleg@pobox.com 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