[TYPES] A show-stopping problem for modular type classes?

[Brian Hulley]

Hi everyone,
with regards to the integration of Haskell-style typeclasses into an SML-style module system I've come across a really difficult problem caused by the interaction of GADTs and scoped type-class instances, and am wondering if anyone has any ideas on how it might be solved.

Consider the following Haskell module that compiles under ghc 6.8.2 with -fglasgow-exts enabled:

  module Test where
     data G a where
        Ok      :: forall a. Num a => a -> G ()
        Problem :: forall a. Num a => a -> G a

     analyse :: forall a. (G a, G a) -> a
     analyse (Ok x, Ok y)           = ()
     analyse (Ok x, Problem y)      = ()
     analyse (Problem x, Ok y)      = ()
     analyse (Problem x, Problem y) = x + y

  $ ghci -fglasgow-exts test.hs
  GHCi, version 6.8.2: http://www.haskell.org/ghc/  :? for help
  Loading package base ... linking ... done.
  [1 of 1] Compiling Test             ( test.hs, interpreted )
  Ok, modules loaded: Test.
  *Test> analyse (Problem (1 :: Int), Problem (2 :: Int))
  3
  *Test> Leaving GHCi.

Conceptually, the Problem constructor stores a Num dictionary for the type of its value argument, so in the above example each Problem constructor in the tuple stores a Num dictionary for the type Int (as well as an Int value).

Because type class instances in Haskell are global, so that there can only be one instance per type, in the fourth clause of (analyse) even though pattern matching makes available *two* Num dictionaries for Int, the compiler knows that they must be the same and so can just forget about one of them (I assume), allowing the arithmetic operator (+) to be resolved for example to the function stored in the first dictionary.

However in a modular setting, there is no such guarantee, so when compiling (x + y) there would be an ambiguity about which Num Int dictionary to use e.g.:


   structure P1 = struct
      instance Num Int where ...

      val p1 : G Int = Problem 1

   structure P2 = struct
      instance Num Int where ...

      val p2 : G Int = Problem 2 (* different dictionary from p1 *)

   structure Client = struct

      val x = analyse (p1, p2)   (* 2 different dicts for Num Int *)

(I've written types the same way as in Haskell to avoid confusion and used layout to avoid having to write "end".)

I've sidestepped the issue of how type class instances are defined and made canonical since this does not seem to me to be relevant: the point is that we can have two incompatible dictionaries stored in values of the same type where the types associated with the dictionaries are visible in the scope of the client, because of the way GADTs allow us to refine a type by adding extra predicates.

(In contrast, uses of the Ok constructor would be fine since the type associated with the dictionary (and value) is hidden.)

Many similar examples could be constructed e.g.

    foo :: forall a. Num a => G a -> a -> a
    foo (Problem x) y = x + y
    ...

Here the compiler must choose between the GADT dict and the dict sent into the (foo) function from the calling context.

So far the only solution I can think of to the problem of designing a modular language with typeclasses is to simply forbid the use of user-defined predicates for GADT constructors (they are fine in existentials as pointed out above with the Ok constructor).

This might be ok but it seems a bit draconian and also I'm wondering if it reveals a fundamental limitation with the whole concept of typeclasses as used in modern Haskell: are they fundamentally non-modular?

Anyway any thoughts or pointers to literature addressing any of these issues would be welcome,

Thanks, Brian.