Modular Implicits

Ecosystem
,
18

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.

37 Likes