Type class problem

[Brandon Michael Moore]

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