Type class problem

[Brandon Michael Moore]

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