[Gagalium blog post] Rethinking abstract module types - feedback wanted

Community
1

I’ve written a blog post on abstract module types (module type T without a definition), available on the gagalium blog. The post sums up how abstract module types can be used, what are the current issues and proposes a restriction/simplification of their semantics. The goal is to eventually update the typechecker with this simplified semantics.

Yet, as it is a restriction, it might break backwards compatibility. Therefore, the key question I’m trying to answer is whether or not the simplification I’m proposing is actually backwards compatible, because no one uses abstract module types outside of the setting I’m proposing.

I welcome any feedback from the both the pedagogical part or the proposed restriction (to simple-signatures-only instantiation), especially if you’re an user or potential user of abstract module types!

12 Likes
3

Tanjential note for now: your link to the blog uses the https version which, on my web browser (Firefox) does not load the any of the CSS files.

The console shows:

Blocked loading mixed active content "http://gallium.inria.fr/blog/style.css"
[...]

but if you use the http version of the website, it works.

2 Likes
4

Here, we would consider Fω with recursion. There are two main issues associated with recursive modules: the semantics of initialization and the typechecking (with recursive types). For now, we have no plan to solve the former. For the latter, we believe that an extension of Fω should cover current OCaml. This extension would contain general iso-recursive types and equi-recursive types restricted to the star kind and should be doable from a theoretical perspective.

1 Like
5

Can be fixed on server side by updating all the links to https.

6

Indeed, I have updated the blog generator to point to the https version by default.

1 Like
8
  1. Could you describe which subtleties of modular implicit the simple abstract signatures will resolve? I heard that modular explicits are stalled by typechecker of module language too.
  2. How far OCaml moved away from module language in the SML? Do they have similar issues too?
9
  1. The simplification of abstract signatures is part of a general effort of specification of the module language that will ultimately help modular implicits or transparent ascription. As I understand it, it’s more the lack of specification and the complexity of the typechecker that slows down extensions than a specific problematic interaction.
  2. OCaml module language is close to SML, but with some key differences. The main one is that OCaml provides both applicative and generative functors (while SML only has the latter). Abstract signatures are also a distinctive feature of OCaml. Overall, the core difference might be that SML is fully specified but does not evolve much, while OCaml lacks a specification but receives frequently updates and new features. We aim at having the best of both worlds ! (and, in passing, proving that the specification makes the typechecking sound)
4 Likes
10

I’d suggest to deprecate abstract module types in the next compiler release (I assume the deprecation itself would be a small change to implement, without actually removing code that handles it? ).

Can that be determined by running a version of the compiler that turns the deprecation into a fatal error on the entire opam repository (or as much as is compilable with 5.x, or maybe try as a small patch on top of 4.14.x for testing purposes to give you more coverage). Although not all OCaml code is in opam, a substantial amount is.

11

@blement I was trying to understand your example of module polymorphism by writing it out concretely (took me a bit to realize what the ...'s were leaving out) and I think I might have found a compiler bug?

The following code causes ocamlc to encounter a fatal error Fatal error: exception Ctype.Nondep_cannot_erase(_) on 4.14.1:

module HashPair (T : sig type t val equal : t -> t -> bool end) : Hashtbl.HashedType = struct
  type t = T.t * T.t
  let equal (a, b) (c, d) =
    (T.equal a b) && (T.equal c d) 
  let hash = Hashtbl.hash
end
    
module type Type = sig module type T end
module MakeApply
    (A:Type) (X: A.T)
    (B:Type) (F: A.T -> B.T)
    (C:Type) (H: sig module Make : B.T -> C.T end) = H.Make(F(X))
    
module HashtblPair = MakeApply
    (struct module T = Int end) (*this should be struct module type T = module type of Int *)
    (Int)
    (struct module type T = Hashtbl.HashedType end)
    (HashPair)
    (struct module type T = Hashtbl.S end)
    (Hashtbl)
1 Like
12

That is indeed a bug! I’m quite surprised that the typechecker is confusing module and module types with the same name (or is it something else ?)… I guess it supports my point that a new clean specification could help improve the typechecker, let alone adding new features.
For reference, here is the issue you’ve opened for this bug and another related issue with a minimal example.

13

I’ve not tested over the whole opam, but it would absolutely give a good idea on how much the feature is used in the wild. I’ve searched the opam codebase using sherlocode, but to little success (outside of compiler tests). However, my proposition is not to deprecate the feature completely, as I think that there are use-cases. I’m also interested in uses outside of opam (maybe at JaneStreet ?)

14

Yeah sorry, I’ve been searching for them too and I can sadly confirm there are very few real world use cases of abstract module types in opam, which I think are captured by this regex module type \w\+\$ on sherlocode, in a sea of tests…

  • base applicative has a lot of “forall” examples!
  • omigrate to expose a first class module type (? but the code looks wrong)
  • varray to hide a private interface, constrained by the functor arguments (… I’m proud of this, please don’t take them away!)

I’m hoping your work will help shed some light on why and when they are useful! (it’s definitively an advanced feature for larger projects, but their practical uses are under documented)

2 Likes