FCM and modular implicits type system

Learning
, ,
1

I was reading the implicits paper again and playing with the explicits PR, but I couldn’t find a good answer for a question. Why implicits require a new way to deal with modules, besides of the syntax improvement? Can’t we just expand inference on FCM, maybe with restrictions?

Does expanding FCM to support better HKT makes the type inference undecidable somewhere?

Comparision

Some examples that are not currently possible, but I wonder if they’re possible.

module type Show = sig
  type t
  val show: t -> string
end
module type S = sig
  val show: (module S: Show) -> S.t
  val show: {S: Show} -> S.t
end

(* maybe needs a symbol to resolve the ambiguity when `v` itself is a FCM that implements Show? *)
let show (module S: Show) v = S.show v
let show {S: Show} v = S.show v

(* can we infer this? *)
let show md v =
  let module S = (val md: Show) in
  S.show v

Code

When I was looking on the explicits PR I noticed also that a Tfunctor is essentially a Tarrow where the left type is a packed module, the AST stuff is a problem tho, because currently unpack is an express

5 Likes
2

For the record: I think this is a good question, and I have made sure to relay it to people working on modular explicits in the past (nowadays: @lpw25, @didierremy, @samsa1). After some discussions there is a new consensus that merging modular-explicits and first-class modules is the way to go, as suggested/hinted by @EduardoRFS above.

A function that takes a module as parameter may:

  • either be dependent (the name of the module is used in the right-hand-side of the arrow), and it can only be passed arguments that are module paths (“pure module expressions”)
  • or be non-dependent, and it can also be passed arguments that are dynamically computed, for example if ... then (module ...) else (module ...).

If a user does not know/understand the difference between the two, they can just write code using the same user-facing feature, and they will get an error message if they try to use the combination that is invalid (dependent type with dynamic arguments). I think that the resulting system is simpler to use, instead of having to decide a-priori which of two different mechanisms to use.

12 Likes
3

Where can we read about those modular explicits? I google it but could not find anything.
Also is there a roadmap for them? Also why do you talk about merging first-class modules,
I thought we already had first-class modules in OCaml.

1 Like
4

When I was looking on the explicits PR …

Unless I’m mistaken it is:

5

Interesting syntactic ambiguity here: "merging modular-explicits and first-class modules " in @gasche’s post is to be read as “merging modular explicits and first-class modules together” (in the common sense) and not as “merging modular explicits as well as first-class modules” (in the git sense).

6

If you want to read about modular explicits with the same syntax as first class modules it would be a bit difficult.
The reason we talk about merging modular explicits and first-class modules is because we plan to use the same syntax for both making both features really close from one-another

We haven’t done any official communication yet, however the code is available at
https://github.com/samsa1/ocaml/tree/modular-explicit2.

2 Likes
7

For people interested about the syntax of modular explicits and modular implicits you can look at the various propositions for the syntax and give your opinion.

2 Likes