Type tree traversals [Re: Modeling multiple inheritance]

[oleg at pobox.com]

This message illustrates how to get the typechecker to traverse
non-flat, non-linear trees of types in search of a specific type. We
have thus implemented a depth-first tree lookup at the typechecking
time, in the language of classes and instances.

The following test is the best illustration:

> instance HasBarMethod ClassA Bool Bool
> -- Specification of the derivation tree by adjacency lists
> instance SubClass (Object,()) ClassA
> instance SubClass (Object,()) ClassB
> instance SubClass (ClassA,(ClassB,())) ClassCAB
> instance SubClass (ClassB,(ClassA,())) ClassCBA
> instance SubClass (Object,(ClassCBA,(ClassCAB,(Object,())))) ClassD
> instance SubClass (Object,(ClassB,(ClassD,(Object,())))) ClassE
>
> test6::Bool = bar ClassE True

It typechecks. ClassE is not explicitly in the class HasBarMethod. But
the compiler has managed to infer that fact, because ClassE inherits
from ClassD, among other classes, ClassD inherits from ClassCBA, among
others, and ClassCBA has somewhere among its parents ClassA. The
typechecker had to traverse a notable chunk of the derivation tree to
find that ClassA.

Derivation failures are also clearly reported:

> test2::Bool = bar ClassB True
>     No instance for (HasBarMethodS () ClassA)
>     arising from use of `bar' at /tmp/m1.hs:46
>     In the definition of `test2': bar ClassB True


Brandon Michael Moore wrote:
> Your code doesn't quite work. The instances you gave only allow you to
> inherit from the rightmost parent. GHC's inference algorithm seems to pick
> one rule for a goal and try just that. To find instances in the first
> parent and in other parents it needs to try both.

The code below fixes that problem. It does the full traversal. Sorry
for a delay in responding -- it picked a lot of fights with the
typechecker.

BTW, the GHC User Manual states:

>    However the rules are over-conservative. Two instance declarations can
>     overlap, but it can still be clear in particular situations which to use.
>     For example:
>  
>       instance C (Int,a) where ...                          
>       instance C (a,Bool) where ...
>   
>     These are rejected by GHC's rules, but it is clear what to do when trying
>     to solve the constraint C (Int,Int) because the second instance cannot
>     apply. Yell if this restriction bites you.

I would like to quietly mention that the restriction has bitten me
many times during the development of this code. I did survive though.


The code follows. Not surprisingly it looks like a logical program.
Actually it does look like a Prolog code -- modulo the case of the
variables and constants. Also
	head :- ant, ant2, ant3
in Prolog is written
	instance (ant1, ant2, ant3) => head
in Haskell.

{-# OPTIONS -fglasgow-exts -fallow-overlapping-instances -fallow-undecidable-instances #-}

data Object = Object
data ClassA = ClassA
data ClassB = ClassB
data ClassCAB = ClassCAB
data ClassCBA = ClassCBA
data ClassD = ClassD
data ClassE = ClassE

class SubClass super sub | sub -> super where
  upCast:: sub -> super
  
instance SubClass (Object,()) ClassA
instance SubClass (Object,()) ClassB
instance SubClass (ClassA,(ClassB,())) ClassCAB
instance SubClass (ClassB,(ClassA,())) ClassCBA
instance SubClass (Object,(ClassCBA,(ClassCAB,(Object,())))) ClassD
-- A quite bushy tree
instance SubClass (Object,(ClassB,(ClassD,(Object,())))) ClassE


class HasBarMethod cls args result where
  bar ::  cls -> args -> result
  
instance (SubClass supers sub, 
          HasBarMethodS supers ClassA)
         => HasBarMethod sub args result where
  bar obj args = undefined -- let the JVM bridge handle the upcast

class HasBarMethodS cls c

instance HasBarMethodS (t,x) t
instance (HasBarMethodS cls t) => HasBarMethodS (Object,cls) t
instance (HasBarMethodS cls t) => HasBarMethodS ((),cls) t

instance (SubClass supers c, HasBarMethodS (supers,cls) t) => 
	HasBarMethodS (c,cls) t
instance (HasBarMethodS (a,(b,cls)) t) => HasBarMethodS ((a,b),cls) t

instance HasBarMethod ClassA Bool Bool where
  bar _ x = x


test1::Bool = bar ClassA True
--test2::Bool = bar ClassB True


test3::Bool = bar ClassCAB True
test4::Bool = bar ClassCBA True
test5::Bool = bar ClassD True
test6::Bool = bar ClassE True