[TYPES] Issues regarding typeclasses and modular languages like ML

[Derek Dreyer]

Dear Brian,

Thanks for reading our POPL07 paper on Modular Type Classes, and
asking some good questions!

The short answer is: Most of the potential problems that you mentioned
do not actually arise in our MTC type system.  The one problem that
does arise has nothing to do with type classes and all to do with the
"value restriction", which is orthogonal.

The long answer is:

> Although there is some literature on the issue of integrating
> Haskell-style typeclasses into modular languages such as ML, it appears
> to me that several important issues remain unresolved.

Our MTC paper is certainly not the final word on the subject (in
particular, we do not attempt to support constructor classes,
multi-parameter classes, recursive classes, etc.).  However, the
important issues that you are concerned about, to the extent that they
have to do with type classes, are resolved quite satisfactorily by our
type system.

> While this is certainly a useful contribution, there are some aspects of
> the Haskell typeclass system that do not appear to be amenable to this
> treatment. Specifically, their treatment seems (to me) to be only
> applicable to those uses of typeclasses where the overloading can be
> statically resolved at compile time, rather than the more general case
> where one wants to have restricted parametric polymorphism, perhaps in
> conjunction with polymorphic recursion and/or existential
> quantification, which involves dynamic generation of (or dispatch from)
> "dictionary arguments" at runtime, and therefore I do not see how
> functor application, which afaict is a strictly compile time activity,
> can be used to model this.

Functor application is *not* a strictly compile-time activity.  I
believe that in Standard ML there are certain restrictions on where
module bindings can occur, but in most dialects of ML, functor
applications may appear inside core-language expressions, and their
arguments may refer to "dynamic" values, e.g., values passed as
arguments to a core-language function, or extracted from a ref cell or
from an existential (for those few dialects that support first-class
modules via existentials).

Certainly in the MTC type system given in (the extended version of)
the paper, there is no static/dynamic distinction between the module
and core levels.

> Moreover their solution to the coherence problem in the face of multiple
> named instances does not appear to deal with the issue of partial
> application. This is because they seem to assume that a polymorphic
> function can be translated into a suitable functor application that
> returns a structure containing a monomorphic value, which is indeed
> suggested by the syntax of qualified types in Haskell, but is confounded
> by some experimentation with ghci, which shows that dictionary arguments
> are actually interspersed with "core" arguments so as to maximize
> polymorphism in the face of partial application:
>
>   $ ghci -fglasgow-exts -fno-monomorphism-restriction
>   GHCi, version 6.8.2: http://www.haskell.org/ghc/  :? for help
>   Loading package base ... linking ... done.
>   Prelude> let f x y = show y
>   Prelude> :t f
>   f :: forall t a. (Show a) => t -> a -> String
>   Prelude> let g = f 'c'
>   Prelude> :t g
>   g :: forall a. (Show a) => a -> String
>   Prelude> (g 1, g "hi")
>   ("1","\"hi\"")
>   Prelude>

There is a problem here, but it's not the one you mention: rather,
it's the so-called "value restriction".

First, AFAICS, there is nothing mysterious about why GHC accepts the
above code.  When f is applied to 'c', the variables t and a are
instantiated with fresh unification variables, t is unified with Char,
a is not unified with anything, and thus, at the binding to g, a is
subsequently generalized.  (That's the Algorithm W explanation, but
one could give an equivalent explanation in terms of the declarative
Hindley-Milner-style type system.)

The reason this code would not typecheck in MTC has nothing to do with
type classes and all to do with the value restriction.  Quite simply,
f('c') is not a value, and due to the value restriction, only values
(or things that are known to be "valuable") may have their types
generalized.  Like ML, our MTC type system is pretty conservative
about what is considered valuable: in particular, core-language
function applications (other than applications of data constructors)
are considered non-valuable.

The problem could be fixed in this instance by eta-expanding the
definition of g to:

let g y = f 'c' y

Eta-expanding bindings is the standard (often admittedly
unsatisfactory) approach to working around the value restriction.

It is worth noting, however, that the MTC proposal is not
intrinsically tied to an ML-like language with the value restriction.
One can imagine employing a very similar proposal for a Haskell-like
language with a monadic separation of effects and no value
restriction.  (The main reason we started with ML instead of Haskell
is that the point of MTC is to show how to encode Haskell-style type
classes in terms of ML-style modules; ML has ML-style modules, while
Haskell does not.)

> The salient point in the above example is that the type of (f) in
> reality is something like:
>
>   Pi (t : *) . Pi (x : t) . Pi (a : * | Show a) . Pi (y : a) . String
>
> so that the dictionary is passed only at the point where we choose how
> to instantiate the type variable (a).

I don't really understand your point here.  In MTC, there is great
flexibility in terms of exactly which type is inferred as the
principal polymorphic type (or, rather, as the principal implicit
functor signature) of an expression.  For example, your function f
could be given the "type"

Forall (X : sig type u; structure S : SHOW end). [X.u -> X.S.t -> String]

or

Forall (X : sig type shmoo; type oyvey; structure S : SHOW where type
t = oyvey end). [X.shmoo -> X.oyvey -> String]

These are both implicitly interconvertible types for f.  Given either
of these types, when we typecheck the binding

let g y = f 'c' y,

what will happen is that the occurrence of f in the body of g will
implicitly instantiate the type components of f's module argument X
with fresh unification variables, and introduce constraints
corresponding to the dictionary modules in the signature of X.
Afterwards, things proceed in much the same way as in Haskell
typechecking.  The only difference is that at the end instead of
generalizing the type of g over a bunch of type variables with some
constraints, our type system packages those things together into a
signature, e.g.

g : Forall (X : SHOW). [X.t -> String]

> (Aside: two uses of Pi above would usually just be written as arrows but
> I find it easier to understand types if everything is written uniformly
> in quantifier notation - is there a better quantifier instead of Pi for
> this case?)

We wouldn't write things out in the Pi notation you used.  I think our
Forall notation (see above) is pretty uniform.  That said, if one
wanted to allow Haskell-style notation for polymorphic types, it would
be totally straightforward to encode it as syntactic sugar.

> Of course I am not trying to criticise the above paper in any way, and
> many of these issues would not arise in an ML setting at the moment due
> to the constraints imposed on the type system by the traditional desire
> to continue to support top level HM type inference. It is just that when
> one is trying to design a new language, with different tradeoffs (e.g.
> discarding TI in favour of first class polymorphism and automatic
> type-driven namespace management), one finds that the existing
> literature does not yet provide all the answers regarding the
> integration of typeclasses with a powerful module system.

Criticizing other people's papers (rightly or wrongly) is the essence
of scientific inquiry.  No worries!

That said, I'm not sure what you're getting at here.

> Another issue that is problematic concerns the question of identity of a
>  type, for example:
>
>   signature S = sig
>      type t
>      val x : t -> int
>   end
>
>   structure M = struct
>      type t = string
>      val x = String.toInt
>   end
>
>   structure N = M :> S
>
> In the above, is N.t the same type as M.t or not (as far as any instance
> declarations inside M / outside M are concerned)? i.e. if one defines an
> instance of some typeclass for M.t would N.t also be a member of the
> class via this instance, and if so, would this not imply that
> abstraction has been broken?

No.  Here, M.t and N.t are distinct types, so after the declarations
of M and N, an instance of a class C for type M.t would not conflict
with an instance of that class for N.t.  Of course, *inside* M or N,
N.t doesn't even exist yet, so I'm not sure I entirely comprehend the
first part of your question.

For the remainder of your questions (concerning citations [2] and
[3]), I will defer to Andreas Rossberg, who will post a separate
reply.

Best regards,
Derek