[bitc-dev] Type Classes for BitC: Instance resolution question

[Mark P Jones]

> One of the problems raised in Simon's paper is the problem of
> overloading ambiguity and type system coherence.

There's a terminology issue to address here.  In the Haskell
community, "ambiguity" and "coherence" are used to refer to
problems like the following:

   What should the expression (show []) print?  If the empty list
   here is an empty list of characters, then it should be "",
   but any empty list of any other type is suppose to be printed
   as [] ... which is the correct semantics?

In this case, the expression (show []) has type (Show a) => String;
notice that the type variable "a" appears on the left of the =>
symbol but not on the right.  Stephen Blott proved (as did I some
time later, in a more general form) that this syntactic test is
sufficient to detect semantic ambiguity:  If the inferred type of
a function is of the form  P => t  and if every type variable
that is mentioned in P also appears in t, then the function has a
well-defined semantics.  Functions that fail this test cannot be
guaranteed to have a well-defined semantics and must be rejected.

There are cases where Haskell programmers write code that has an
ambiguity.  Fortunately, such programs don't show up very often in
practice, and, when they do, it is usually quite easy to work around
the ambiguity with a type annotation.

> Consider a type class "set". We might define an instantiation for "set
> of (list 'a)". Later, we might decide that a more specialized
> instantiation would be appropriate for "set of (list char)".

This is a different problem, and is usually referred to in
Haskell as "overlapping instances."  Although it is not officially
part of the Haskell standard, both GHC and Hugs (two of the most
popular implementations) support this as an extension.  For example,
you might write:

    instance Show a => Show [a] where ...
    instance Show [Char] where ...

(this specific example is actually dealt with in standard Haskell
using a different trick, and without overlapping instances; that
trick can be used in other cases but it gets to be tricky once you
start working with more complicated examples ...)

Overlapping instances remain a somewhat controversial feature for
Haskell.  I think the Peyton Jones, Jones, Meier paper talks some
more about this ...

> Mark Miller has suggested that we adapt a rule from Joule:
> 
>   The instantiation of a type class can legally appear only
>   in one of the following interfaces:
> 
>   1. The interface defining the type class, or
>   2. The interface that defines the type that is an instance
>      of the type class.
> 
> Because the concrete type must be in scope in order to instantiate it or
> infer it, this guarantees that the necessary instantiation is in scope.
> It also guarantees that erroneous multiple instantiations are statically
> detectable.

Haskell (prior to version 1.3) had a similar rule called the "CT rule"
(google can find it if you're desperate enough: Haskell CT rule).
It was dropped because, as I recall, it proved to be awkward in some
cases, it wasn't clear that it really bought you very much, and it
wasn't clear how to generalize the rule to some of the type class
extensions that were being proposed/implemented at the time.

All the best,
Mark