Suggestion: refine overlap handling for instance declarations

[Bulat Ziganshin]

Hello Claus,

Friday, March 17, 2006, 1:47:25 AM, you wrote:

CR> - consider a/=Int (that is: not (a=Int)).

CR> - consider a/=b (that is: not (a=b)).

CR> comparisons of more complicated structures reduce to these
CR> and ground comparisons. so it looks as if there isn't that much
CR> difference, but we need to be careful about when rules are
CR> suspended/woken up, or fail and are retried, and when guards 
CR> are decided. so we certainly need to be careful about which 
CR> disequality to choose as default, even if we are only interested 
CR> in replacing overlaps. 

may be we can solve all the problems just by using prolog-style
programming, with unification and backtracking? at least type
inference by itself is unification process. with overlapping instances
it turns into the unification with backtracking, i'm right?

type of function that is a part class interface can be also viewed as
partially defined term. when we start unification process, we have
partially defined terms, during the unification process we find a rule
which allows to completely define all types involved. in this respect
type class is just a Prolog-style relation:

type Ref ::
     ( m :: Monad
     , r :: **
     , newRef :: a -> m (r a)
     , readRef :: r a -> m a
     , writeRef :: r a -> a -> m ()
     )

type Ref (IO, IOURef, newIOURef, readIOURef, writeIOURef) where Unboxed(a)
     Ref (IO, IORef, newIORef, readIORef, writeIORef)
     Ref (ST s, STRef s, newSTRef, readSTRef, writeSTRef)

type specifications in first sentence define overall type structure of
each function (i mean newRef/readRef/writeRef). instance declarations
allow to find function implementations depending on context. so, in the
following definition:

test :: IO Int
test = do x <- newRef 0
          readRef x

`readRef x` should return "IO Int", so we construct partially defined
term and pass to the `Ref` relation (because readRef is a part of Ref
definition). this term matches on the first line and gives us

readRef = readIOURef
x :: IOURef Int

type of `x` determines result type of `newRef 0` expression, we again
pass this type into the Ref relation and determine that

newRef = newURef
0 :: Int



we can write type functions what uses type relations (classes):

type MonadRef :: Monad -> **
     MonadRef m | Ref (m,r...) = r

type function defined in this style can be used as any ordinal type
constructor.

data StrBuffer m = StrBuffer (MonadRef m Int)
                             (MonadRef m String)

this defines data structure that holds two references, to Int and
String, mutable in monad 'm'.



it seems that i written large text without much sense, but at least:

1) we can't live without unification, relations and backtracking. it
will be great to define type computation rules just using Prolog's
calculus. excluding for FDs, it seems that all we want to use just fit
in this old and well-known computation model.

2) we want to see type functions and use type relations in them. it
will be great to mix types and plain data in such definitions but that
is more complex question. at least, we can work in type functions with
type constructors (List in my first example). we can use classes as
"types of types"

3) after all this syntax experiments i can propose continue to use
type classes to define type relations, but allow to use plain values,
type functions and predicates together with type classes in instance
declarations:

instance Binary Int where ...
instance (Integral a, a/=Int) => Binary a where ...
instance (Enum a, !Integral a) => Binary a where ...
instance (Binary a) => Binary (MonadRef IO a) where ...
instance (Binary a, r = MonadRef IO, r/=IORef) => Binary (r a) where ...
instance (MArray a e IO) => Binary (MArray a e IO) where ...

these instances can be seen as Prolog rules that direct the search.
each type variable can be "free", "assigned", or "restricted". in the
last case it contains the list of "prohibitions", i.e. values it CAN'T
be assigned (a/=Int, a/=b, "!Integral a" and "!Ref m r" all lead to such
prohibitions). when compiler tries to assign value to restricted
type variable, it checks all the prohibitions associated with this
variable. if all ok, the variable can be assigned new value. of
course, when there is no variants, backtracking occurs and in
appropriate points assignments and restrictions are cancelled. we can
see instance searching as logical program with complete searching
algorithm, while "-fallow-undecidable-instances" switches to
depth-first searching algorithm.

another idea - priority assigned to each instance. this priorities
used to define search order for the depth-first algorithm. may be this
algorithm should be enabled on each class individually? if any
instance of this class includes "priority" clause then this algorithm
should be used for this class.

type functions still should be able to use classes as type relations:

class Ref m r ...

type MonadRef m | Ref m r = r


-- 
Best regards,
 Bulat                            mailto:Bulat.Ziganshin at gmail.com