[Haskell] class assosiated types, via GADTs or FDs

[Manuel M T Chakravarty]

On Tue, 2005-02-15 at 10:16 +0000, Keean Schupke wrote:
> Perhaps i'm being dumb, but I dont see the need for either GADTs or 
> class-associated-types to do this... I am pretty sure it can be done 
> using fundeps,

Yes, you can encode this example with functional dependencies (see
Section 3.4 of [1]), but functional dependencies have three drawbacks,
which are discussed in the associated types paper [2].  In case you
don't want to read the paper, the problems are the following.  Your
class declaration with functional dependencies becomes

  class MapKey k fm | k -> fm where
    lookup :: k -> fm v -> Maybe v
    empty :: fm v
      -- NB: The signature of empty doesn't mention k, which
      --     is already problematic, but you can fix this by
      --     adding it as a dummy argument to fm.

Drawback #1:
------------
If you want to add an instance for keys of pair type, you need an
instance of the form

  data MapKeyPair fm1 fm2 v = ...
  class (MapKey k1 fm1, MapKey k2 fm2) => 
    MapKey (k1, k2) (MapKeyPair fm1 fm2) where
    ...

If you look into Section 6.1 of the functional dependencies paper [3],
you'll see that this definition is actually not admitted.  GHC allows it
nonetheless.  As a result, the type checker will on some programs, that
it ought to reject, simply not terminate - that's been pointed out by
[4].

Drawback #2:
------------
There's been an interesting study about the support for a certain form
of generic programming in six different programming languages (four OO
languages and two FP languages) [5].  In that study the not quite
satisfactory support of associated types in Haskell via functional
dependencies is cited as the *only* shortcoming of Haskell in the
summary of Table 1 (Haskell gets the best results of all six languages
in that table, btw).  The main complaint cited by the authors is that
the representation type (fm in the example above) needs to be included
in the argument list of the class.  For larger examples, with more
associated types, such as the graph library studied in [5], this is
unwieldy.

Drawback #3:
------------
The functional dependency encoding prevents you from ever making the
representation of your tries/maps (in the MapKey class example)
abstract.  It does not only prevent you from declaring it as an abstract
data type, but it actually forces users of a library built in this way
to understand the representation types and manually encode them in their
application code.  For example, assume we have an instance as follows

  instance MapKey Int (Data.IntMap v) where
    lookup k m = Data.IntMap.lookup k m 
    empty = Data.IntMap.empty

The full type of the class method lookup is

    lookup :: MapKey k fm => k -> fm v -> Maybe v

Now suppose a user wants to define a function

  lookupInt :: MapKey Int fm => k -> fm v -> Maybe v
  lookupInt = lookup

then they will find that the compiler rejects this definition.  (The
reason lies in when the type checker uses Mark Jones' improvement rule
[3].)

In fact, the only valid definition is

  lookupInt :: k -> Data.IntMap v -> Maybe v
  lookupInt = lookup

That's quite unsatisfactory, as a user of a such a tries library will
have to know how maps of Int keys are represented.  Moreover, if the
tries library ever changes that representation, all user code will have
to be changed.  This problem is aggravated by that representation types
for tries get quite complicated once you use more involved types as
keys.

This third drawback makes functional dependencies IMHO rather unsuitable
for encoding associated types in anything, but toy code.

Manuel

[1] Ralf Hinze, Johan Jeuring, and Andres Löh. Type-indexed data types. 
    Science of Computer Programming, MPC Special Issue, 51:117-151, 
    2004.
    http://www.informatik.uni-bonn.de/~ralf/publications/SCP2004.pdf

[2] Manuel M. T. Chakravarty, Gabriele Keller, Simon Peyton Jones, and 
    Simon Marlow. Associated Types with Class.  POPL'05.
    http://www.cse.unsw.edu.au/~chak/papers/papers.html#assoc

[3] Mark P. Jones. Type Classes with Functional Dependencies.
    Proceedings of the 9th European Symposium on Programming Languages
    and Systems, LNCS 1782, 2000.
    http://www.cse.ogi.edu/~mpj/pubs/fundeps-esop2000.pdf

[4] Gregory J. Duck, Simon Peyton Jones, Peter J. Stuckey, and Martin 
    Sulzmann.  Sound and Decidable Type Inference for Functional 
    Dependencies.  ESOP'04.
    http://research.microsoft.com/Users/simonpj/Papers/fd-chr/

[5] Ronald Garcia, Jaakko Järvi, Andrew Lumsdaine, Jeremy G. Siek, and 
    Jeremiah Willcock.  A Comparative Study of Language Support for 
    Generic Programming. In Proceedings of the 2003 ACM SIGPLAN 
    conference on Object-oriented programming, systems, languages, and 
    applications (OOPSLA'03), 2003.
    http://www.osl.iu.edu/publications/pubs/2003/comparing_generic_programming03.pdf