the MPTC Dilemma (please solve)

[Claus Reinke]

here's my take on this (disclaimer: I've got a bit of experience in 
type-class-level programming, but I'm not an expert in type systems;).

Isaac pinned the problem to MPTCs and FDs, because the former 
are closely connected to when people started noticing the problem, 
and the latter are intended as a partial solution. the dilemma, as far as 
standardization is concerned, is that there are several variants of FDs, 
and their interaction with other features, and that there is no clear 
optimum in the design space yet (ghc isn't doing too badly in its
pragmatic way, but for a standard, one would prefer a consistent
story).

however, the underlying problem is not limited to MPTCs, and FDs 
are not the only attempt to tackle the problem. so I agree with Isaac: 
getting a handle on this issue is imperative for Haskell', because it will 
be the only way forward when trying to standardize at least those of 
the many extensions that have been around longer than the previous 
standard Haskell 98. and if Haskell' fails to do this, it fails.

to understand my reason for this strong opinion, it is necessary to 
understand that the problem underlying this dilemma not limited to
some optional extensions one might continue to ignore, but instead 
is part of almost all advanced type-class programming - I'll try to 
illustrate with one example.

first, here's a stripped down example of (label-type-based) 
selection of fields from records (as nested tuples):

    -- | field selection
    infixl #?

    class Select label val rec | label rec -> val where
      (#?) :: rec -> label -> val

    instance Select label val ((label,val),r) where
      ((_,val),_) #? label = val

    instance Select label val r => Select label val (l,r) where
      (_,r)       #? label = r #? label

    -- examples
    data A = A deriving Show
    data B = B deriving Show
    data C = C deriving Show
    data D = D deriving Show

    r1 = ((A,True),((B,'a'),((C,1),((D,"hi there"),((B,["who's calling"]),()))))) 

the intention is to select the first field with a matching type of
label (question: is this intention expressed in the code? how?).

this code loads and works, with ghci-6.4.1 (and -fglasgow-exts, 
-fallow-overlapping-instances), and I can select the first B field like this:

    *Main> r1 #? B
    'a'

the same code does *not even load* with Hugs 98 (Nov 2003) +98
(more recent releases seem to have left out the windows platform):

    Hugs mode: Restart with command line option +98 for Haskell 98 mode

    ERROR "C:\Documents and Settings\cr3\Desktop\haskell\haskell prime\Dilemma.hs":1
    0 - Instances are not consistent with dependencies
    *** This instance    : Select a b (c,d)
    *** Conflicts with   : Select a b ((a,b),c)
    *** For class        : Select a b c
    *** Under dependency : a c -> b

this demonstrates the dilemma, and I hope it also shows why I want these
extensions standardized, at the very least as an addendum defining all the
options out there in current use. this is not about saying that every 
implementation has to support FDs, but about clarifying what is supported.

we can modify the example a bit, to get to the underlying problem. here's
a Select', without the functional dependency:

    -- | field selection
    infixl #.

    class Select' label val rec where
      (#.) :: rec -> label -> val

    instance Select' label val ((label,val),r) where
      ((_,val),_) #. label = val

    instance Select' label val r => Select' label val (l,r) where
      (_,r)       #. label = r #. label

now this loads in both ghci and hugs, but it doesn't quite work to our
satisfaction:

    Main> r1 #. B
    ERROR - Unresolved overloading
    *** Type       : Select' B a () => a
    *** Expression : r1 #. B


    *Main> r1 #. B
    <interactive>:1:3:
        Overlapping instances for Select' B val
             ((B, Char), ((C, Integer), ((D, [Char]), ((B, [[Char]]), ()))))
          arising from use of `#.' at <interactive>:1:3-4
        Matching instances:
          Dilemma.hs:10:0: instance (Select' label val r) => 
                                        Select' label val (l, r)
          Dilemma.hs:7:0: instance Select' label val ((label, val), r)
        (The choice depends on the instantiation of `val'
         Use -fallow-incoherent-instances to use the first choice above)
        In the definition of `it': it = r1 #. B

note, btw, that ghci offers a dangerous-sounding workaround, for the 
adventurous, but this isn't actually going to help, because it only offers 
to default to the recursive instance, soon running out of record to 
select from (and no reordering of source-code seems to affect that 
choice):

    *Main> :set -fallow-incoherent-instances
    *Main> r1 #. B
    <interactive>:1:3:
        No instance for (Select' B val ())
          arising from use of `#.' at <interactive>:1:3-4
        Probable fix: add an instance declaration for (Select' B val ())
        In the definition of `it': it = r1 #. B

back to the problem: there are multiple instances matching the
context required to fulfill our selection request, and since the choice
of instance might affect the program result, neither implementation
is willing to commit to one of the choices (unless explicitly encouraged
by a daring option;).

so far, so good. we can resolve the ambiguity with a type annotation:

    Main> r1 #. B ::Char
    'a'

    *Main> r1 #. B::Char
    'a'

everybody happy? not at all! recall our original FD: we wanted the 
result to be dependent on the field selected, not the field selection 
dependent on the result requested!

    Main> r1 #. B ::[String]
    ["who's calling"]

    *Main> r1 #. B::[String]
    ["who's calling"]

oops. if we go back to the original code (and hence ghci only), we
get the error message we expected, because the first B field in r1
holds a Char value, not a [String]:

    *Main> r1 #? B::[String]
    Top level:
        Couldn't match `Char' against `[String]'
          Expected type: Char
          Inferred type: [String]
        When using functional dependencies to combine
          Select label val ((label, val), r),
            arising from the instance declaration at Dilemma.hs:20:0
          Select B
                 [String]
                 ((B, Char), ((C, Integer), ((D, [Char]), ((B, [[Char]]), ())))),
            arising from use of `#?' at <interactive>:1:3-4

by now, you'll probably have an idea what the problem is (at least,
the problem as I see it): selection from ambiguous instances, and
committing to one of several choices. 

to hammer home the point that this is not specific to MPTCs, but 
inherent in complex type-class level programming, here's the 
ambiguous version again, without any MPTCs:

    class Select' t where
      (#.) :: t

    instance Select' (((label,val),r)->label->val) where
      ((_,val),_) #. label = val

    instance Select' (r->label->val) => Select' ((l,r)->label->val) where
      (_,r)       #. label = r #. label

this version loads fine into hugs, but not into ghci:

    *Main> :r
    Compiling Main             ( Dilemma.hs, interpreted )
    Dilemma.hs:10:0:
        Non-type variables in constraint: Select' (r -> label -> val)
        (Use -fallow-undecidable-instances to permit this)
        In the context: (Select' (r -> label -> val))
        While checking the context of an instance declaration
        In the instance declaration for `Select' ((l, r) -> label -> val)'
    Failed, modules loaded: none.

undecidable instances is ghc jargon for "i don't have to care what
these instances look like. just don't blame me.". once we've signed
that disclaimer, we get the same problems, without any MPTCs
in sight:

    Main> r1 #. B ::Char
    'a'
    Main> r1 #. B ::[String]
    ["who's calling"]

    *Main> r1 #. B::Char
    'a'
    *Main> r1 #. B::[String]
    ["who's calling"]

the reason that this problem starts to show up with MPTCs is that,
with conventional limitations on instances in place, MPTCs were one
of the first extensions that permitted multiple variables to be constrained
by one type-class constraint. once those limitations are relaxed (as
well they should be), there are other uses of type classes that exhibit
the same issue.

the reason that FDs are connected with this problem is that they are
trying to address part of it, by allowing us to turn type-level relations
(type-class constraints involving multiple types) into type-level
functions, so that resolving only a subset of type variables in such a
constraint will be sufficient to commit to an instance. 

so, once again, the problem is *selection from possibly ambiguous
instances*, and *control over that selection*. and this problem seems
to be inherent in type-class-level programming, with or without
MPTCs or FDs. the problem is aggravated by the wish to support
separate compilation of modules, because it means that the 
implementation can never know that there won't be another
fitting instance just around the corner.. this leads to the slightly
ridiculous situation that the implementation will sometimes not
even select the one and only instance we ever intended to write. 

note that I said "possibly ambiguous", because, really, there 
shouldn't be any ambiguity in this case (and in many other cases).
usually, it is just that Haskell (or the Haskell+ implementation at
hand) does not give us the means to express our intentions in
an unambiguous form. and that is not for not trying, either. to wit,
have a look at some of the language features that have tried to
address parts of the problem (or that have been proposed):

- defaults (remember those?)
- functional dependencies 
- "most-specific" rule in overlapping instances
- incoherent instances (is the selection documented anywhere?)
- closed classes (yes, dear compiler, you can see *all* instances)

it may also be worth pointing out the one language feature that
does *not* try to help with the problem:

- ignoring contexts when deciding about overlaps

because, often, the contexts establish mutually exclusive 
pre-conditions to those "overlapping" instances. so, this is a lot
like ignoring guards when matching patterns.. and if we were
able to specify negation of type predicates (the characteristic
predicates of those type relations specified by MPTCs), 
avoiding overlaps by such constraints would be even easier.

well, I could go on, but that's probably more than enough for 
now. thanks for reading with us, we hope you had an enjoyable
trip!-)

cheers,
claus