Suggestion: refine overlap handling for instance declarations

Tue Mar 14 07:54:46 EST 2006

overlapping instances with best-fit overlap resolution are useful 
because they give us an alternative way to write programs that 
we cannot write directly as long as current Haskell isn't expressive 
enough:

    (a) we can't specify that two types in an instance are not equal; 

        but we can use overlap resolution to ensure that equal types 
        are handled by another, more specific instance

    (b) we can't enable library users to add instances for their types,
        yet ensure that there will be some instance for every type;

        but we can use overlap resolution to provide a default
        instance, to be overridden by more specific instances in
        library and user code

    (c) we can't rely on mutual exclusion properties specified in instance
        contexts to be used to select the appropriate instance because
        Haskell only looks at instance heads;

        but we can sometimes wrap our types in extra constructors
        so that the mutual exclusion is reflected in more and less
        specific instance heads, with overlap resolution choosing
        the right one (this is a real pain, brittle against change, and
        not always possible..)

    (d) ..this seems to cover most uses discussed so far, but I don't
            claim this list to be complete. if you know of examples not 
            covered by a-c, please add them by reply!

there hasn't been any enthusiasm about changing (c) for Haskell',
which isn't to my liking, but nothing I can do much about. I would,
however, like to continue arguing in favour of refining overlap 
handling until we get at least some progress into Haskell' (and
addenda). so I propose to add the something like the following 
to Haskell':

---------- we know how to handle (a) [no overlap needed]:

syntax: 

    permit type inequalities as guards in instance declarations:

    <topdecls> -> ..
             | 'instance' [<ctxt> '=>'] <head> [ '|' <ineqs> ] [<body>]

    <ineqs> -> <typevar> '/=' <type> [ ',' <ineqs>]

semantics (sketch):

    - add inequality guards from an instance as guards to the 
        rules for that instance in the CHR
    - add inequality guards as attributes to the typevars
        after successful guard evaluation and rule commit

remarks:

    - we only need the extra guard syntax because of (c) above
    - we restrict inequalities to variables on lhs to simplify semantics
    - attributed variables are logic programming folklore:
        variable attributes are simply goals to be reexamined whenever
        the attributed variable is instantiated; we need them here to 
        ensure that after we have selected a CHR rule based on an 
        inequality, that inequality is not violated by later instantiations

-------------------- we can make (b) more explicit:

instead of enabling overlapping instances and overlap resolution
on a per-module or per-session basis, we can specify which
instances we want to use only as defaults:

syntax:

    <topdecls> -> ..
             | ['default'] 'instance' [<ctxt> '=>'] <head> [ '|' <ineqs> ] [<body>]

semantics (sketch):

    - default instances may be overridden by more specific instances
        including other default instances, but no such overlap is permitted
        unless there is a single most specific instance 
    - default instances only apply if there can be no more specific 
        instances; the easiest way to model this is by collecting all
        instances for the class, select those that are more specific
        than some default instance, and add type inequality guards
        that exclude those instantiations from the rule for the 
        default instance
    - no other instances are affected by overlap resolution

remarks:

    - by declaring all instances as 'default', we could recover the
        current, indiscriminate overlap handling; but we hardly ever
        want that, as declaring default instances allows us to be
        more precise, limiting the impact of overlap handling
    - once we have type inequality guards in the language, we 
        can be a bit stricter about ruling out overlaps than GHC 
        is at the moment (see Simon's earlier example)
    - default instances with ground heads (no variables) can be
        treated like non-default instances (there can't be any more
        specific instances)
    - without further analysis, application of default instances has
        to be delayed until the whole program is visible; that does
        not prevent separate compilation, it only prevents early
        application of some instances (those marked as defaults);
        in other words, separately compiled modules are 
        parameterized by the set of more specific instances for
        their default instances
    - we don't want to go through all that trouble for every
        instance in every class, which is the motivation for being
        very specific about where we want overlaps to be 
        permitted and resolved

cheers,
claus