Implicit scope

[lpw25]

This patch is an extension of #28. It essentially adds a separate notion of implicit scope for looking up implicit modules and functors, rather than piggybacking on the ordinary scope.

Implicit scope

OCaml's ordinary scope can be thought of as a set of identifiers, from which references are looked up. When a new identifier is defined, identifiers with the same name are removed from the set, and the new identifier is added.

Similarly, the implicit scope is a set of paths from which implicit modules are looked up. Since the lookup is by type, shadowing would ideally be done by type. However, the relationship between paths and the types that they cover is complex: depending on the other paths in scope and how types have been abstracted. This makes direct type-based shadowing too difficult to reason about. So instead we use explicit weakening, separating the removal of paths from scope from the addition of new paths to the scope.

Paths can be added using the syntax:

implcit Foo.Bar

the previous syntax:

implciit module M = ...

is now short-hand for:

module M = ...
implcit M

Paths can be removed from the implicit scope using:

explicit Foo.Bar

There are also corresponding local versions:

let f () =
  let explicit IntOrd in
  let implcit IntOrdRev in
    foo 7

Module aliases

Since aliased module should ideally be interchangable, all module aliases are fully normalized before being added or removed from the implicit scope, so that:

implicit Foo.Bar
module M = Foo.Bar
explicit M

will result in no overall change to the implicit scope.

Modules and open

Modules can be thought of as capturing a change in the ordinary scope. When projecting from a module the members are looked up in the scope which results from applying this change to the empty environment. When opening a module this change is applied to the current environment.

This is the approach we take with the implicit scope. implicit and explicit declarations are components of modules and when a module is opened they are applied in order to the current scope. This maintains the ability of opening modules to completely change the environment -- the classic example being open Core.Std switching the entire standard library.

Whilst there is not currently an equivalent to projecting the implicit scope, with implicit modules one could envisage a syntax like M.? to look up a module using the implicit scope of M.

Module inclusion

When checking inclusion between modules each implicit/explicit definition in the output must be matched by an implicit/explicit definition for the same path (or an alias of it) in the input. Module aliases mean that we cannot know which implicit and explicit definitions would shadow each other. This means that all implicit definitions in the output must be in the same order, relative to the explicit definitions, as in the input -- and vice versa for explicit definitions. Implcit definitions may still be reordered relative to other implicit definitions, and likewise for explicit definitions. So:

module M : sig implicit B implicit A explicit C end = struct implicit A implicit B explicit C end

is fine, but:

module M : sig implicit A explicit C implicit B end = struct implicit A implicit B explicit C end

is not.

Implicit include

We also add a specialised form of include:

include implicit Foo

which includes only the implicit definitions in Foo. (There is currently a bug in this caused by a bug in how modules are strengthened on the version of OCaml we forked from, when we rebase to trunk it will go away).

[yallop]

I like this: resolving instances by type and adding/removing them by path seems like the right approach.

Some of the behaviour around explicit is surprising, I think because implicit sometimes means "add something to the implicit environment" and sometimes refers to both implicit and explicit operations together. For example, open implicit M can remove arbitrary instances from the environment, if M contains explicit statements. It might be better to stick with one keyword, and use a more general deletion syntax together with implicit in place of explicit:

implicit Foo.Bar
implicit -Foo.Bar  (* rather than "explicit Foo.Bar" *)

let- implicit IntOrd in  (* rather than "let explicit IntOrd" *)
let implicit IntOrdRev

(I'm not suggesting this concrete syntax, but I hope the idea is clear.)

Attaching the deletion notation to the binding keyword rather than introducing a separate keyword would make it easier to extend OCaml in a uniform way if we wanted to add similar operations to other environments.

[let-def]

I like this too.

I am not sure to understand the purpose of M.?. Is it a short-hand for let open implicit M in _ like M.(_) is a shorthand for let open M in _?

[hakuch]

I like the

include implicit Foo

syntax.

Is there an alternative like open implicit Foo for opening the implicit definitions in Foo without the other bindings in Foo, or is this addressed through some other mechanism?

[lpw25]

It might be better to stick with one keyword, and use a more general deletion syntax together with implicit in place of explicit:

Yes something like that might be better, the overloading of implicit is certainly an annoyance. Like all syntax it depends on being able to find a concrete alternative to explicit which is clear and precise. (For example - is probably too subtle and easy to miss).

I am not sure to understand the purpose of M.?

To be clear M.? is not part of this patch, it was just an idea I had that has a nice parallel with regular module projection. If we add support for functors with implicit parameters, such that:

module F {X : S} (Y : T with type t = S.t)= ...
module M = F(N)

might work. You could easily extend that to supporting a general "find a module of the right type and use it here" syntax, like:

module X : sig type t = int val x : t -> string end = ?

Which would also naturally extend to forcing an implicit application whilst still looking up the module implicitly:

let f {X : S} : X.t = ...
let foo : int = f {?}

You could then extend the idea further with M.? which would mean the same as ? but restricting the search to those implicits declared in M:

let foo : int = f {M.?}

This might be quite useful, but I'm not really proposing it at this stage.

[lpw25]

Is there an alternative like open implicit Foo

open implicit Foo was already supported before this patch.