Type class problem

[Simon Peyton-Jones]

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
|=20
| instance (Show a =3D> Show (f a)) =3D> Show (Mu f) where
|   show (In x) =3D show x
|=20
| 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)
|   ...
|=20
| 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=20
	evaluate them using call-by-value; if they could be recursively=20
	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))) =3D> Show (Mu f) where
>    show (In x) =3D show x
>
> instance Show (N (Mu N)) where
>    show Z =3D "Z"
>    show (S k) =3D "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 '=3D>' is more
complicated than the stuff after the '=3D>'.  A less carefully written
instance for Show (N (Mu N)) would make the type checker loop.

Simon