Modular Implicits

Are we going to merge this to master? If not what’s blocking it? Thanks!

8 Likes

This question comes up fairly often. Perhaps it should be in a FAQ of some sorts? r/ocaml has a stickied thread about multicore due to the endless questions of this sort. Maybe it makes sense to gather what is known about this topic in 1 place.

7 Likes

I think that’s a good idea, although to me the best place for such FAQ would be the project page on OCaml Labs website.

I’ve been following the project since its initial announcement. Sadly the modular implicits fork has not been very active in the last year, at least publicly, and, as far as I know, there has been no announcement on the project roadmap and future neither from OCaml Labs nor the core devs. A relevant question on GitHub from a couple of month ago was closed with “no roadmap because it is hard to explain to mere mortals”. While I do understand @lpw25 point there, I believe it would still benefit to the community if the work on modular implicits was a bit more open.

2 Likes

Suppose I just wanted polymorphic versions of the four common arithmetic operators that would work with both floats and ints. Is there a version of the modular implicits fork that I could use, safely, probably, now?

Some days the clutter of dots in float arithmetic really bothers me.

(I appreciate that there might be contexts where it’s safer to use different operators for float and int arithmetic, but sometimes convenience and clarity are more important.)

(I don’t assume that getting the four arithmetic operators to work with floats and ints in all situations is necessarily simple. I know that I have no idea what’s involved.)

(One of several reasons I decided to learn OCaml even though I was very happy doing what I was doing in Clojure was that, even though I’m extremely comfortable with Lisp syntax, for arithmetic, prefix notation will never be as easy to read as infix notation. Decades of math notation has its effect. But I find Clojure arithmetic easier to read that OCaml float arithmetic!

Don’t make me use Haskell or F# ! Just kidding. I have other reasons to avoid them.)

2 Likes

I agree that for computation-heavy code doubling the size of common operators can be too much. However, even without modular implicts, I find that local opens combined with local redefinition of these operators, e.g.

 module Float = struct
   let (+) = (+.)
   let (-) = (-.)
   …
end
let normal mu sigma2 x = let open Float in
  exp ( - (x-mu) ** 2. / (2. * sigma2) ) / sqrt ( 2. * sigma2 * pi )

alleviate much of this pain. The main exception being functions which heavily mix integer and float arithmetic for which modular implicits would be useful. However, in my experience, these cases are not that common.

12 Likes

Oh, very nice. I didn’t think of that. I’m going to start using it immediately.

2 Likes

If it is reading rather than typing the dots that bothers you, Tuareg can help you with that thanks to prettify-symbols-mode:
Tuareg

P.S. you must be careful with the expression as written in the original post: -(x)**2.parses as (-x)**2. not as -(x**2) — which is the mathematically correct way. This is an quirk in OCaml syntax that unfortunately has not been fixed for fear that this would affect people using that “feature”.

Interesting, and very nice. I’m not sure it’s right for me at the moment. I like knowing exactly what I’m typing, and although my fingers were once Emacs-linked, they’re now Vim fingers. :slight_smile:

I asked the relevant people (Leo White, Jacques Garrigue and Frédéric Bour) at ICFP in early September, and I thought that people may be interested in a summary of “where we are right now”. Please remember however that (1) I am not personally working on modular implicits, so I may very well be wrong on various points and (2) Leo, who is working on modular implicits, has provided an explicit non-response indicating in particular that giving detailed explanations on a work-in-progress is taxing. For these reasons, please be considerate in how you respond and whether to ask further questions.

My understanding of the current status is that:

  1. there is wide consensus that the feature is important and desirable
  2. there is no consensus, or even clear picture, of whether the type system (module system) changes implied by the feature preserve the desirable properties of the OCaml type system (soundness and principality); Leo says they do, but no one else knows.

The plan for the future is to have (1) a theory of the feature that people agree on and (2) a type-checker that implements this theory. Right now, Leo provided a draft of (1), but it is substantially more powerful/complex than what the OCaml type-checker currently implements. We need to bridge that gap, by making the theory simpler, or the type-checker beefier, probably a bit of both.

One reason why this takes time is that this is very specialized work, with only a handful of people with both (1) the skillset to work on this and (2) time they are willing to volunteer for this. They are effectively working at the time scale of research, which is a long time scale.

20 Likes

I stand by my non-response in that I’m not about to get involved in a detailed discussion here. But I just wanted to point out that with:

(soundness and principality); Leo says they do, but no one else knows

I think soundness is generally accepted as not really an issue – they basically elaborate into existing OCaml constructs. It is on principality, and more generally on similar properties of the inference itself where things are less clear.

5 Likes

@lpw25 : Did you have some discussion with the Coq Team on this subject ? In Coq, there is canonical structures, since more than 15 years, which are analogous to Modular Implicit. The system is explained in the article Canonical Structures for the working Coq user by Assia Mahboubi and Enrico Tassi. There is also a mechanism of implicit arguments. Both are based on the Coq’s unification algorithm.

The article’s abstract is :

This paper provides a gentle introduction to the art of programming type inference with the mechanism of Canonical Structures. Programmable type inference has been one of the key ingredients for the successful formalization of the Odd Order Theorem using the Coq proof assistant. The paper concludes comparing the language of Canonical Structures to the one of Type Classes and Unification Hints.

Hope this will also give some guarantee to @gasche about the type soudness of such a system.

1 Like

There’s plenty of prior work on a variety of similar systems. I’m fairly confident I’m familiar with all the relevant literature. As I said, the interesting question is not soundness but predictability of inference.

3 Likes

Given that there is a working prototype of modular implicits, is the problem simply proving principality in the general case, or have actual problematic examples been found?

The problem isn’t really with proving things. The prototype is just that – a prototype – it is not a full implementation. There are plenty of parts not yet implemented and most of these parts are not yet precisely specified. They need a precise specification, producing that specification and making sure that it has predictable inference is the thing that still needs to be done. Obviously the most reassuring way to “make sure that it has predictable inference” is to prove it – but we’re not at that point yet.

7 Likes

I’m curious as to whether there’s any news on Modular Implicits…

1 Like

We (a subgroup of OCaml developers including Leo and myself) met in November to discuss many things, including modular implicits. Leo’s plan is fairly ambitious, basically it involves making the module system of OCaml as powerful as general dependent types (has been done for module systems before, is not such a jump from the current system, but still requires quite some work to implement unification correctly), and there are still some orthogonal implementation questions that are still open for discussion. So more work is required, and since November everyone has been fairly busy with plenty of other things, so not much progress has been done I think.

(If you know someone interested in both the metatheory of module systems and implementation questions, willing to do an internship or some other form of short-term contract paid on research salaries, I would wildly guess that there is space for a year of work on these questions.)

15 Likes

Is it possible that a more limited implementation that was not so ambitious but was compatible with a future more general version would be feasible? It would be a shame if it took many years before the feature appeared, though I would understand concerns about not knowing if a simpler version would be syntactically and semantically compatible with a more ambitious version.

2 Likes

Is it possible that a more limited implementation that was not so ambitious but was compatible with a future more general version would be feasible?

Much of the work for a limited version would need to be redone from scratch for the more complete version. Given our very limited man power, doubling the amount of work we have to do is probably not a good idea. The more limited version would still be a huge amount of work, so it is not like it would appear any time soon anyway.

My plan is certainly ambitious, but the potential pay offs are pretty large. I think I can give some idea of them with a relatively short description…

The key mechanism of modular implicits is the ability to search for a module from a list of possible modules based on a module type. For example, given:

module type PP : sig
  type t
  val print : Format.formatter -> t -> unit
end
let print {P : PP} ppf x = P.print ppf x
...
let () = print Format.std_formatter [1; 2; 3]

we will be searching the implicit modules for a module with type:

sig
  type t = int list
  val print : Format.formatter -> t -> unit
end

Now OCaml already knows how to check if a module has a particular module type. So if we just had a finite list of possible modules, it would be easy to check each of them against this module type. However, we also have implicit functors like:

implicit module Print_list {X : PP} = struct
  type t = X.t list
  let print ppf x = Format.pp_print_list X.print x
end

which means that there are an infinite number of possible implicit modules. We require that our solution be unique to avoid ambiguity – so we need to know that all but one of this infinite collection of modules does not have the required module type.

This requires us to answer questions like: “Is there any module X such that the result of Print_list(X) would be of the required module type?”. Which is actually just
a unification problem at the module level, essentially can we unify = Print_list(?X) with sig type t = int list val print : ..., where ?X is a unification variable and = ... is a singleton type/module alias.

So implementing modular implicits requires us to implement a unification algorithm at the module level. Now the prototype uses a very naive algorithm which is very weak and quite unpredictable. My more ambitious plan is to implement a higher-order pattern unification, of the sort found in languages like Agda, and to do so for the full module language. My plan also includes strengthening the module language with additional equalities – in particular module aliases on functor applications and eta-equality on structures – in order for unification to have some more desirable properties.

In addition to giving a more expressive and predictable implementation of modular implicits, having a powerful unification algorithm for the module system opens up a number of possibilities:

  1. As well as implicit module arguments, we can support inferred module arguments, where the required module is found entirely by unification. Allowing parametric polymorphism over a module, to go with the ad-hoc polymorphism provided by implicit arguments.
  2. Inferred module arguments, combined with eta-equalities at the module level, allow us to have the equivalent of polymorphic type class instances in Haskell.
  3. Unification is apparently the hardest part of implementing dependent pattern matching. This opens up the possibility of supporting inductive families and dependent matching in the module language.
  4. Similarly, we should be able to support ordinary types parameterised and indexed by modules. Combined with the above this would allow e.g. a vector type indexed by a length of module type Nat defined as you would expect – no more silly games pretending that that the types z and 'a s are the natural numbers.
  5. It should allow a full and predictable solution to the problem of “double vision” in recursive modules.
  6. It should also allow the inference of definitions in an .ml file based on the contents of the .mli – so you could just write type t = _ in the .ml and avoid having to write the definitions twice.

Of course all of those are large amounts of work, and they are not going to be included as part of the modular implicits project, but I think that they definitely help to justify having a more complete solution to the unification issue in modular implicits.

The curious can see a formal description of a module system that includes the “additional equalities” I mentioned here.

As Gabriel said, everyone is very busy at the moment, so not much has been done since November. Personally, I’ve been using my free time on the algebraic effects work, but I hope to get back to looking at implicits in the second half of the year.

36 Likes

Honestly, this sounds like a completely different language (though compatible with OCaml). This new language should get a completely new standard library and will enforce different paradigms of programming, i.e., using lot’s abstractions and making everything generic. Probably it should be named OCaml anymore, just a very powerful language that is compatible with OCaml.

4 Likes

It would be difficult to find it a name. It will be a mix between a camel, a lion (leo in latin) and a rooster (coq in french). Very strange animal, isn’t it? :smiley:

4 Likes