modular type classes

[RobertHarper]

Unsuprisingly, I am fond of modular type classes --- the implicit application of functors along designated paths of composition to obtain a structure of a specified signature in a "standard" (by declaration) way. It's a purely elaboration-time issue, and would not disrupt old code, I don't think.

Modular type classes could then we used to displace the old equality type mechanism, which I think is pretty broken, especially because it doesn't work with abstract types (and its defaults for data types are pretty much useless).

[DemiMarie]

Does this still allow whole-program monomorphization? MLton does this very early on, and relies on it for its performance.

Also, does this allow replacing the overloaded numerical operators by library-defined operators?

[JohnReppy]

I don't think that it would break monomorphization. It is things like polymorphic recursion, where a function can have a dynamically varying set of type instantiations, that break monomorphization.

[RobertHarper]

right, i agree with john. the type class mechanism in haskell has been vastly overused because it’s all they have. it makes sense to have a convenient instantiation mechanism for modules, but we needn’t go to absurd lengths to mimic every last thing they are doing.

yes, it would eliminate ad hoc overloading, as wadler’s original paper on the topic pointed out in the title. it would also eliminate the preposterous notion of equality type variables and eqtype declarations in ml, by making it a special case of something general.

introducing a nice type class mechanism will require a re-think of library conventions, i’m afraid. the reason is that we’d like to have conventions that fit together well. for example, maybe the “main” abstract type should always be called t, with perhaps a synonym, so that every abstract type would, if sensible, be of class EQ or ORD, for example. we can’t anticipate every possible scenario, obviously, but we can try to make common cases such as orderings easy. otherwise you have to explicitly define a view of an abstract type, which in fact is not such a bad thing because it documents the sense in which you are stipulating that a bst admits equality, for example.

btw, karl crary has implemented all of this in his prototype sml+ to sml compiler. it works great! he has to target moscow, though, because nj, for unknown reasons, has long resisted implementing local structures. i cannot think of a reason why not, but there you are. if that were to be changed, karl’s prototype could target nj.

bob

On May 1, 2016, at 15:11, John Reppy notifications@github.com wrote:

I don't think that it would break monomorphization. It is things like polymorphic recursion, where a function can have a dynamically varying set of type instantiations, that break monomorphization.

— You are receiving this because you authored the thread. Reply to this email directly or view it on GitHub https://github.com/SMLFamily/Successor-ML/issues/18#issuecomment-216065031

[DemiMarie]

Could this be combined with ways to auto-generate equality, ordering, and hashing functions?

Writing equality, ordering, and hashing functions is often boring boilerplate code that is easy to get wrong.

[RobertHarper]

of course! if you read the mentioned paper, we separate out completely the idea of “deeming these functors available for backchaining, please compose a structure of this type class, a signature of a certain form.” it’s simply wrong-headed to equate the definition of a functor with deeming it the one and only way to make things of its result signature. not to mention having only type classes, and not both type classes and type abstractions as we have always had in sml since 1984.

bob

On Jul 7, 2016, at 16:31, Demi Marie Obenour notifications@github.com wrote:

Could this be combined with ways to auto-generate equality, ordering, and hashing functions?

Writing equality, ordering, and hashing functions is often boring boilerplate code that is easy to get wrong.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/SMLFamily/Successor-ML/issues/18#issuecomment-231198280, or mute the thread https://github.com/notifications/unsubscribe/ABdsdYUUsI8FD0aPG4Kez7__P7Q-GpT7ks5qTWI_gaJpZM4IDt66.

[DemiMarie]

In that case I propose adding derivation of comparison, equality, and hashing operations for data types (that don't contain functions), when so requested. On Jul 7, 2016 4:40 PM, "Robert Harper" notifications@github.com wrote:

of course! if you read the mentioned paper, we separate out completely the idea of “deeming these functors available for backchaining, please compose a structure of this type class, a signature of a certain form.” it’s simply wrong-headed to equate the definition of a functor with deeming it the one and only way to make things of its result signature. not to mention having only type classes, and not both type classes and type abstractions as we have always had in sml since 1984.

bob

On Jul 7, 2016, at 16:31, Demi Marie Obenour notifications@github.com wrote:

Could this be combined with ways to auto-generate equality, ordering, and hashing functions?

Writing equality, ordering, and hashing functions is often boring boilerplate code that is easy to get wrong.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub < https://github.com/SMLFamily/Successor-ML/issues/18#issuecomment-231198280>, or mute the thread < https://github.com/notifications/unsubscribe/ABdsdYUUsI8FD0aPG4Kez7__P7Q-GpT7ks5qTWI_gaJpZM4IDt66 .

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/SMLFamily/Successor-ML/issues/18#issuecomment-231200695, or mute the thread https://github.com/notifications/unsubscribe/AGGWB6l0MCKRrRtz2-fxALKYXEs_ENgyks5qTWRWgaJpZM4IDt66 .

[JohnReppy]

Bob: I don't think that you specified the paper, but I assume you are referring to your POPL 2007 paper with Derek, et al Is Karl's implementation available anywhere?

[DemiMarie]

Also, how do modular type classes compare to modular implicits?

[rossberg]

@DemiMarie, for one thing, they actually have a defined semantics.

[DemiMarie]

@rossberg-chromium sorry

[nilern]

Also, how do modular type classes compare to modular implicits?

Like in Haskell, modular type classes have definition-site checks to ensure canonicity, which is somewhat at odds with modularity. Modular implicits only check that every resolution is unambiguous, which is less robust because overlapping instances will lurk until you write code that actually hits the ambiguity.

To reconcile the tension between canonicity and modularity, modular type classes split the language into two layers; an explicitly typed outer layer and an inner layer where types and type class constraints can be inferred. The modular implicits paper is critical of this, but I don't find it that bad since the core language and modules are already stratified.

Because they have weaker coherence guarantees, implicits cannot infer implicit parameters, only arguments. This is fine in Scala, whose type inference is extremely limited in general. The type class approach of generalizing over type class constraints as well as type variables is more convenient and fits core ML better (at the expense of modules).

@DemiMarie, for one thing, they actually have a defined semantics.

It should be straightforward to adapt the implicit calculus semantics to modular implicits. It is disappointing that they modular implicits authors did not do that even though they were aware of that paper.

[nilern]

Does this still allow whole-program monomorphization? MLton does this very early on, and relies on it for its performance.

It should not prevent monomorphisation like polymorphic recursion or higher-rank types would. I suspect it could lead to code explosion if there is no sharing of implicit functor instantiations. Sharing the instantiations sounds a lot like applicative functors and reconciling it with the generativity of SML functors might be challenging.