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

[Derek Dreyer]

Brian,

> The example I had in mind was (using layout + Haskell/ML mixed up syntax):
>
>  ...[example elided]...
>
>       val c : Set T = Set.union S0.s S1.s
>
> where both S0 and S1 construct sets of more than one element using different orderings, and the binding to U.c uses (perhaps) yet another ordering to implement the merge that is part of the implementation of Set.union.
>
> The problem is that the particular ordering used to construct a set is not reflected in the type of the set itself, and indeed the fact that Ord is used at all is not reflected in the Set type so the export of val s from S0 effectively causes the instance of Ord to travel (in its effects) outside its lexical scope without anyone knowing that this has happened.

This is indeed a good observation.  It is closely related to an issue
that arises in the semantics of ML functors, in particular applicative
functors.  With applicative functors, you can write a type like
"Set(IntLt).t" or "Set(IntGt).t", denoting the type of sets obtained
by applying the Set functor to the IntLt or IntGt modules, which
provide different orderings on integers.

The question is when are types resulting from applications of the same
functor equivalent.  Under a number of applicative functor proposals,
the answer is "whenever the argument modules are *statically*
equivalent", meaning that their type components are equal.  Static
equivalence is the most liberal possible answer one can give.  But, as
you've noted, this leads to "bug-friendliness" because in fact sets of
integers ordered one way are not compatible with sets of integers
ordered another way.

OCaml answers the question using "syntactic equivalence", i.e.
Set(IntLt).t only equals Set(IntLt).t.  This has the benefit of not
equating Set(IntLt).t and Set(IntGt).t, but it is also quite
restrictive.  In particular, if you happen to define a module IntLt by
"module IntLt2 = IntLt", then Set(IntLt).t is considered distinct from
Set(IntLt2).t even though they are obviously equivalent.  Furthermore,
if argument modules are allowed to be arbitrary paths involving
functor applications, such as F(X), then syntactic equivalence is
still not good enough.  In particular, in the presence of effects, one
application of F(X) could very well return IntLt, while another
returns IntGt, thus returning us to the problem with static
equivalence.  (Of course, in practice, one is unlikely to write such
code.)

In Chapter 2 of my thesis, I argued that the right answer to the
question is "contextual equivalence".  Set(IntLt).t and Set(IntGt).t
are compatible types so long as IntLt and IntGt are contextually
equivalent.  Of course, in general, contextual equivalence is
undecidable, so we must look for a conservative approximation.  But
it's not hard to get a reasonable conservative approximation of it by
attaching "stamps" (i.e. hidden abstract types) to each value
declaration.  If the language had real dependent types, that would be
even better, as Set(IntLt).t is really a dependent type.  But let's
sidestep dependent types for now.


Now, coming back to the modular type class scenario, you're completely
right that the Haskell approach of defining Set.insert to be
parameterized over an Ord class constraint doesn't work properly in
the presence of scoped instances.  The reason, as you said, is
precisely that the type "Set a" doesn't make sense if there can be
more than one ordering in the program.  What you really should do is
parameterize the Set type constructor over (some static representation
of) the ordering on the element type a.  Of course, that's exactly
what a correct (i.e. "non-bug-friendly") implementation of applicative
functors would do as well.

Unfortunately, the original modular type class paper (POPL'07) only
supports generative functors, but for the reasons given above I think
an applicative functor extension of it would be useful.  For more
detail, I would refer you to the slides from a talk I gave a couple
years ago, in which I simultaneously proposed modular type classes as
a good motivation for non-bug-friendly applicative functors, and also
sketched how an applicative functor extension to the MTC paper would
look:

http://www.iai.uni-bonn.de/~ralf/WG2.8/24/slides/derek.pdf

Some day soon, I will get around to writing up the details.

Best regards,
Derek