Type tree traversals [Re: Modeling multiple inheritance]

[Brandon Michael Moore]

On Tue, 4 Nov 2003, Simon Peyton-Jones wrote:

>
> | We really should change GHC rather than keep trying to work around
> stuff
> | like this. GHC will be my light reading for winter break.
>
> Maybe so.  For the benefit of those of us who have not followed the
> details of your work, could you summarise, as precisely as possible,
> just what language extension you propose, and how it would be useful?  A
> kind of free-standing summary, not assuming the reader has already read
> the earlier messages.
>
> Simon

There are two extensions here:

More overlapping:
Allow any overlapping rules, and apply the most specific rule that
matches our target. Only complain if there is a pair of matching
rules neither of which is more specific than the other.

This follow the spirit of the treatment of duplicate imports, and
lets you do more interesting computations with type classes.
For example, the sort of type class hack Oleg and I have been writing much
easier. You use nested tuples to hold a list of values your search
is working over, have a rule that expands the head to a list of
subgoals, a rule that flattens lists with a head of that form,
and an axiom that stops the search if the head has a different
form, without needing the stop form to unify with a pair.

This extension would accept the code I just posted, and seems pretty
conservative.

Backtracking search:
If several rules matched your target, and the one you picked didn't
work, go back and try another.

This isn't as well through out: you probably want to backtrack through all
the matching rules even if some are unordered by being more specific. It
would probably be godd enough to respect specificity, and make other
choices arbitrarilily (line number, filename, etc. maybe Prolog has a
solution?). This probably isn't too hard if you can just add
nondeterminism to the monad the code already lives in.

This would give you OR. The example Integral a => MyClass a,
Fractional a => MyClass a would work just fine and give you a class that
is the union of integral and fractional. This class hierarchy search
could be done by a SubClass class that had an instance linking a class
to each of it's different parents, then the search just needs to backtrack
on which parent to look at:

class SubClass super sub

instance SubClass A C
instance SubClass B C

class HasFoo cls
  foo :: cls -> Int
instance (SubClass super sub,HasFoo super) => HasFoo sub
instance HasFoo B

now look for an instance of HasFoo D
  uses first rule for HasFoo,.
  Needs an instance SubClass x D. Tries A, but can't derive HasFoo A.
  GHC backtracks to trying B as the parent, where it can
  use the second instance for HasFoo and finish the derivation.

Overloading resolution:
This one is really half-baked, but sometimes it would be nice if there was
some way to look at

class MyNumber a where
  one::a
instance MyNumber Int where
  one = 1

then see (one+1) and deduce that the 1 must have type Int, rather than
complaining about being unable to deduce MyNumber a from Num a. This is
really nice for some cases, like a lifting class I wrote for an Unlambda
interpreter, with instances for LiftsToComb Comb and (LiftsToComb a =>
LiftsToComb (a -> Comb)). With some closed world reasoning lift id and
lift const might give you I and K rather than a type error. Also, for
this work with modelling inheritance you almost always have to give type
signatures on numbers so you find the method that takes an Int, rather
than not finding anything that takes any a with Num a. This obviously
breaks down if you have instances for Int and Integer, and I don't yet
know if it is worth the trouble for the benefits in the cases where it
would help. Implementation is also a bit tricky. I think it requires
unifying from both sides when deciding if a rule matches a goal.

Improvements and better suggestions welcome. I'm only particularly
attached to the first idea.

Brandon