Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

modular type classes #18

Open
RobertHarper opened this issue Apr 9, 2016 · 12 comments
Open

modular type classes #18

RobertHarper opened this issue Apr 9, 2016 · 12 comments

Comments

@RobertHarper
Copy link

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
Copy link

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
Copy link
Contributor

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
Copy link
Author

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 #18 (comment)

@DemiMarie
Copy link

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
Copy link
Author

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 #18 (comment), or mute the thread https://github.com/notifications/unsubscribe/ABdsdYUUsI8FD0aPG4Kez7__P7Q-GpT7ks5qTWI_gaJpZM4IDt66.

@DemiMarie
Copy link

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
#18 (comment),
or mute the thread
https://github.com/notifications/unsubscribe/AGGWB6l0MCKRrRtz2-fxALKYXEs_ENgyks5qTWRWgaJpZM4IDt66
.

@JohnReppy
Copy link
Contributor

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
Copy link

DemiMarie commented Jul 10, 2016 via email

@rossberg
Copy link
Member

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

@DemiMarie
Copy link

@rossberg-chromium sorry

@nilern
Copy link

nilern commented Jul 12, 2019

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
Copy link

nilern commented Jul 12, 2019

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

5 participants