Modular Explicits

Since the last meeting, we have written a rather lengthy presentation of “modular explicits”, and their interaction with the rest of the language. You can find that technical document at http://pourquoi.parce-q.eu/modular-explicits.pdf

Here we will only give a very brief reminder of what the proposal is, and discuss the questions and concerns that were raised at the last meeting. For everything else, we refer the reader to the technical document.

The extension

The “modular explicits” project proposes to extend the core language with module-dependent functions, concretely this means:

• extending type expressions with a new kind of arrow {M:S} -> type_expr, where the type expression on the right of the arrow can refer to M, a module of type S bound on the left of the arrow
• extending expressions with
  • a new form of abstraction fun {X:S} -> expr, which constructs a module-dependent function, of type {X:S} -> _
  • a new form of application e {M}, to eliminate module-dependent functions

This construction gives access to the following features from the core-language:

• higher rank polymorphism; admittedly already available using polymorphic methods or polymorphic record fields, but in a less straightforward manner
• higher kinded polymorphism
• fine-grained polymorphism, e.g. specifying that the type you’re parametrized by is an immediate, or is injective, etc.

To get a feel for module-dependent functions, we reproduce here a canonical example: a map function parametrized by a monad:

module type Monad = sig
  type _ t
  val return : 'a -> 'a t
  val bind : ('a -> 'b t) -> 'a t -> 'b t
end

let map {M : Monad} f (x : 'a M.t) : 'b M.t =
  M.bind (fun x -> M.return (f x)) x

Section 2 of the technical document contains more detailed examples for each of the features listed above, as well as a description of a lightweight encoding of Fω in OCaml using module-dependent functions.

Semantics?

We refer to section 1 of the extended technical document for a (more) serious description of the construction and its semantics.

Here we limit ourselves to reminding everyone of the intuition given by the modular implicits paper: a module-dependent function is just a lightweight syntax for manipulating first-class functors.

Overlap with first-class modules

The overlap between module-dependent functions and (a particular use of) first-class modules has been pointed out by several people, raising the question of the usefulness of the construction, and the potential confusion for users of the language between it and what already exists.

The said overlap happens between module-dependent functions which are not actually dependent and regular functions taking a first-class module as argument.

Both constructions do indeed behave in the same way in these situations, and could be used interchangeably. We show in the document (sec 3.2.3) that we can actually use module-dependent functions to write generic coercions between the two. We could in fact directly instruct to typechecker that they are convertible, that is, tell the compiler to treat types up to the following equivalence rule:

           X \notin FTV(t)
-----------------------------------
|- {X : S} -> t === (module S) -> t

Furthermore, we explore in the document (sec 3.3) the idea of using the same syntax for both module-dependent functions, as we do for functions taking first-class module as arguments.

Going back to the map example above, it is conceivable to allow writing it as follows:

let map (module M : Monad) f (x : 'a M.t) : _ M.t =
  M.bind (fun x -> M.return (f x)) x

which would be given the type

val map : (module M : Monad) -> ('a -> 'b) -> 'a M.t -> 'b M.t

and can be applied like so:

map (module Option) succ None

This is technically feasible (details are provided in the document) and, at first glance, hides the overlap between the two constructions: there is, syntactically, just one construction.

However, despite the syntax, the two constructions remain separate, and one cannot for instance, write the following

let f (x, (module M : Some_sig)) = some_expr

and hope to have the type of some_expr depend on M.

Where do we go from here

The question of whether to use the same syntax for both constructions, or to have two different syntactic construct is still open. We (Didier and Thomas) lean towards keeping them syntactically separate, while allowing (explicit?) coercions between the two for cases which are compatible.

However decisions about syntax seem to be more a matter of taste (or intuition about good language design) than anything else. So we are expecting to hear your opinion on the matter.

Regarding the usefulness of module-dependent functions

Another question that was raised previously is whether modular-dependent functions are useful enough that it would be worth adding them to the language, even if we do not add modular implicits later on.

We believe that modular-dependent functions significantly extend the expressive power of the language. The examples we have looked at (and which we discuss in the document) also show a clear difference in usage between this new construction and first-class modules. The intersection of features is a concern for a few simple cases, and otherwise the two features do rather different things. Furthermore, some language support to move more easily between the two could be provided.

We also direct the reader to the technical document for a comprehensive discussion regarding the relationship between module-dependent functions and modular implicits.