@lpw25 This sounds amazing and totally awesome, but wouldn’t a language that allowed only searching finite lists of modules and not implicit functors still be a significant win over what we have now? You don’t need unification for that, so maybe that wouldn’t require doing an enormous amount of work on unification that needed to be thrown away? It would still allow for a lot of interesting day to day programming and make everyone’s life easier.
I’m not suggesting that the full plan not be executed on, just that it is easier to eat an elephant one piece at a time. Also, the presence of a mechanism to compete with Haskell’s typeclasses would bring more labor to the OCaml ecosystem, and might make it easier to execute on the full program. If you do it once piece at a time, then each time you make the language richer, you’ll have made it more useful to people, you’ll bring more people in to the community, and that will make it that much easier to do the next piece because there’s a richer ecosystem and labor pool.
My experience in other environments is that if it takes too many years to get a simple but very useful version of a feature because the totally awesome version of it requires more work, sometimes this means that you never get the community strong enough to sustain the totally awesome vision. It’s always nice to look for a way that allows incremental steps.
wouldn’t a language that allowed only searching finite lists of modules and not implicit functors still be a significant win over what we have now?
I don’t think so. It rules out using modular implicits with type constructors. I’m not aware of any use cases for which this doesn’t make them unusable.
I don’t think there is anything that easily allows incremental progress. You could make a weaker version of the unification – but then you are really creating work that must be done twice. You could try to leave out some convenience features – but they mostly don’t take much extra effort and leaving them out risks damaging people’s initial impression of what implicits are like to use.
One way to think of the problem is that we are, in a way, adding a single new operation to the language. It is a lot of work because all the cases in the language must be handled by the operation, but that work can’t really be subdivided into smaller blocks because the operation needs to be completely defined before it works at all.
May you provide a signature of a list with a length as a type parameter, how would it look like with modular implicits? How close it would be to dependent types we have in F* or coq?
Well, I’m just making up syntax as I go here – as I said these are possibilities opened up by having a full unification algorithm, not concrete plans within the modular implicits project – but I imagine something like:
module type Nat =
| Zero
| Succ of Nat
type ('a, 'L : Nat) vect =
| Nil : ('a, Zero) vect
| Cons : 'N : Nat. 'a * ('a, 'N) vect -> ('a, Succ('N)) vect
module rec Plus (X : Nat) (Y : Nat) <: Nat =
match X with
| Zero -> Y
| Succ(X) -> Succ(Plus(X)(Y))
val append : <'N : Nat> -> <'M : Nat> -> ('a, 'N) vect -> ('a, 'M) vect -> ('a, Plus('N)('M)) vect
There are all kinds of design decisions around syntax that would need to be resolved, but conceptually the above should work.
How close it would be to dependent types we have in F* or coq?
It would probably be pretty close to the core of those languages, although they obviously have all kinds of additional features. It’s worth noting that the module language is already a dependently typed language, just a crippled and extremely inconvenient one. For example, you can already construct girard’s paradox in it.
About the first part of your comment, I have a question: isn’t strange to call Zero a module (or any other module of type Nat)? There is no value (nor type) defined in it. They are like the empty module but with another module type.
I think here we need to distinguish “modules” from “structures”. For me “module” just means a value in the module language. Currently the module language only contains structures and functions (called functors for historical reasons), but there is no reason it cannot have other sorts of values in it.
For me the only fundamental differences between the module language and the core language are predicativity – every thing in the core language is “small” (in the cumulative hierarchies of universes sense) – and inference – the core language strives to have powerful type global type inference, the module system has no global inference. In an ideal world (see 1ML) the core and module languages would be separated only in their types, rather than syntactically, but that ship has sailed for OCaml.
Ok, I better understand. This is like if you say: currently in the module language we only have product and exponential types whit their values: records (or structures) and functors, but we can also add sum types and their values (like the module type Nat of your example). Hence, since there is subtyping in the module language, do you plan something similar to Stephen Dolan’s biunification in your unification algortihm?
do you plan something similar to Stephen Dolan’s biunification in your unification algortihm?
Unfortunately, biunification does not work well with the kind of subtyping in the module system. The module system’s subtyping coercions actually exist at runtime, and biunification doesn’t handle inferring when/where those should happen. It is also still work in progress to mix that approach with higher-rank types, higher-kinded types etc. So the unification will be quite weak around subtyping – although I don’t expect that to cause many problems in practice. It may encourage us to also add ordinary non-subtyping record types to the module system as well as sum types, but I suspect that they would be useful anyway.
Probably it should be named OCaml anymore, just a very powerful language that is compatible with OCaml.
Except that OCaml is currently somewhat deficient, and could really use having the module language be made smarter and more intuitive. This isn’t obvious when you evaluate OCaml in a vacuum, but when compared to its state-of-the-art competitors haskell and rust, it’s clear that the ease of use isn’t quite where it should be. The reason people have been wishing for modular implicits is that they’ve used type classes and seen how powerful and easy type-based dispatch is (another alternative is OOP mixins as implemented in Scala). If someone offered me to ditch OCaml’s current, complex module system and use type classes instead, I would instantly take that deal, and I suspect most users would, too.
And 2 months later, you would cry as you realize you have lost type abstraction, proper (fast) separate compilation and half the ecosystem because type classes really can’t do the same jobs as functors.
And 2 months later, you would cry as you realize you have lost type abstraction, proper (fast) separate compilation and half the ecosystem because type classes really can’t do the same jobs as functors.
I don’t see haskell or rust crying about these things. Separate compilation is on the way out anyway, since optimization is all about cross-module inlining. I’m willing to sacrifice some compilation time to have the power of type classes. And what advantage do functors give us that type classes cannot perform? I’ve yet to see something that makes me happy to have functors over type classes, but I’ve seen many examples of the opposite.
I don’t think we have a usable answer to backpack either, to play the devil’s advocate. Functorizing entire libraries remains too boilerplate heavy to be viable. The thought of translating everything that backpack is doing into functor applications makes me shudder.
As stated above, I’d be happy to hear about such benefits.
I understand the benefit of separate compilation, but I think this will diminish gradually as flambda becomes more crucial for getting good performance out of OCaml.
Quoting from Edward Z Young’s thesis on Backpack, where he makes the case for a more complex modular system:
Unfortunately, type classes are ill-suited for certain cases of separate modular development:
From a code perspective, type class parametric code is often harder to use than monomorphic code. For an inexperienced Haskeller, the proliferation of constraints and type parameters in the type signatures of functions can make an otherwise straightforward API impenetrable:
(=~) :: (RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target)
=> source1 → source → target – from regex-posix-0.95.2
This point is reasonable, and indeed functors removing type parameters make using said types clearer in my experience.
Furthermore, type classes work best when exactly a single type parameter is involved in instance resolution. If there aren’t any type parameters, you must introduce a proxy type to drive instance resolution; if there are multiple parameters [5], you often need to resolve ambiguity by introducing functional dependencies [12] or replacing parameters with associated types.
This has to do with limitations of typeclass inference, and in my experience in a fairly large haskell codebase, this is still worth the advantages, and is fine so long as you aren’t pushing the envelope with typeclass usage.
Type classes work best when it is clear what methods they should support. However, for many interfaces, it is not obvious what set of methods should be put into an interface; for example, there are many functions which an interface for strings might support—which ones go in the type class? It is inconvenient to define a new type class (and new instances) just to add a few more methods, and thus this is rarely done in practice.
This seems valid but it applies equally well or even more so when creating functor interfaces, while with type classes, adding functionality to a type can at least be done on a mixin basis by adding an additional type class when needed.
From a performance perspective, code which uses a type class is compiled without knowledge of how the type class’s methods are implemented. This can be quite costly in a language like Haskell, where inlining definitions is essential to achieving good performance. [20] This problem can be mitigated by specializing code to a particular type, but if this specialization occurs at use-site, the compiler ends up repeatedly reoptimizing the same function, blowing up the code size of a program. (C++ templates suffer from similar problems.)
This point seems just as valid with regard to OCaml’s functors.
BTW I would really love to understand the benefits of OCaml’s approach to modules and functors. From my experience, OCamlers who see haskell’s type classes are generally impressed (I know I was), while haskellers who see OCaml’s functor system are underwhelmed. I’d love to have a really good retort for why the OCaml way is better, I just don’t know of one. Is type abstraction the OCaml way really that valuable? If so, why? Is it worth the cost of not having easily implementable type classes? From the new description of the problem’s scope, I’m moving my forecast of modular implicits arriving to about 10 years from now, or perhaps never. Meanwhile, perfectly good projects are being written using the simple module systems of Rust and Haskell, all the while enjoying type-based dispatch, sound polymorphic comparison and serialization etc. So is it worth it?
Look at the API of ocamlgraph and you’ll see how powerful functors can be. That said, I think I’d rather have rust’s trait system and get rid of magic polymorphic operators, too
I’m a newcomer, and not nearly as deep in my understanding of the various tradeoffs. That said, I’d really love to have Modular Implicits so I won’t miss typeclass style functionality any more.
However, it sounds like Second Systems Effect is striking (one of the most dangerous problems in software design!) and I worry that a really nice feature will not appear for a very long time because a really cool but very hard goal has been added to the critical path for implementation.
I think we should be equally weary of diagnosing the situation with these software development poverbs. Many of these sound very elegant and start their life in the well written essays of various “thought leaders”, but have very little relevance once you apply them to a concrete problem.
From my own (totally uninformed) view point, the issue is not Leo’s engineering. Quite the opposite, I think we’ve simply stretched him too thin: Modular Implicits, Multicore, Effects, Namespaces, etc. Or put another way, i don’t think we need more managers on top of the scarce developer resources.
