[Caml-list] Modular explicits in pre-OCaml 5.5

[Caml-list] Modular explicits in pre-OCaml 5.5

[oleg]

One of the notable features of the just announced OCaml 5.5 are
module-dependent functions, a.k.a. modular explicits. It is a welcome
addition: it lets us express higher-ranked types in the simplest way,
and is particularly good for typed tagless-final code.

It should be mentioned however that modular explicits could be done before,
with little or no hassle. Perhaps there is merit to remind of that old
trick~-- especially because it works also with statically unknown modules
(which are out of scope for OCaml 5.5 modular explicits).

As the running example we re-use the pretty-printing example in the
OCaml 5.5 announcement (hereafter, Ann55).

We start however with a simpler example: pretty-printing a set 
generated by the `Set.Make` functor. The example follows the 
pattern of the pp_map function from Ann55. It is simpler than 
printing a map because it involves no higher-rank types.

let pp_set (type a s) 
      (module M: Set.S with type elt = a and type t = s) 
      (pp_elt:Format.formatter->a->unit) (ppf:Format.formatter) (set:s) = 
  if M.is_empty set then Format.fprintf ppf "ø" else 
  let pp_sep ppf () = Format.fprintf ppf ",@ " in 
  Format.fprintf ppf "@[{@ %a@ }@]" 
    (Format.pp_print_seq ~pp_sep pp_elt) (M.to_seq set) 

It is almost literally the pp_map example from Ann55, with set
substituted for map. The main difference is type annotations. This is
not a bug: I insist on writing signatures or explicit type annotations
for all top-level definitions (except, perhaps, the most trivial).

The annotations could be simplified if we introduce

type ('e,'s) set = (module Set.S with type elt = 'e and type t = 's)
type 'a printer = Format.formatter->'a->unit

The example then reads

let pp_set : type e s. (e,s) set -> e printer -> s printer = 
  fun (module M) pp_elt ppf set -> (* ... as before ... *)

The signature tells at a glance what pp_set is doing (which is one of
the benefits of signatures: it is not just for, and not mainly for,
the compiler.)

We can use pp_set just like pp_map was used in the Ann55 example:

module String_set = Set.Make(String) 

let () = 
  let m = String_set.of_list ["Zero"; "Zero"; "One"; "Un"] in 
  let pp_str = Format.pp_print_string in 
  Format.printf "%a@." (pp_set (module String_set) pp_str) m 

Our rendition of modular explicits extends beyond statically known
modules like String_set. For example,

(* Abstract set of elements of types 'e. The implementation is abstract *)

type 'e aset = (module Set.S with type elt = 'e)

let f : unit -> int aset = fun () -> 
  if Random.bool () then 
    (module Set.Make(Int)) 
  else 
    (module Set.Make(struct type t = int 
      let compare x y = - Int.compare x y end))

The function f randomly returns one of two distinct Set
implementations (the Set.t types are not compatible). As an
application, we print a list of integers as a set (automatically
sorting and removing duplicates):

let print_as_set : type a. a aset -> a printer -> a list printer  = 
  fun (module M) pp ppf lst -> 
    pp_set (module M) pp ppf (M.of_list lst)

let _ = Format.printf "%a@." 
    (print_as_set (f ()) Format.pp_print_int) [1;2;3;1]

The result is indeed either "{ 1, 2, 3 }" or "{ 3, 2, 1 }", depending
on how die is cast.


Let us now tackle the pp_map example from Ann55. It is challenging because
of the higher-rank type of the map type 'a Map.S.t.

It is tempting to define the module type as

type ('k,'v,'m) map = 
    (module Map.S with type key = 'k and type 'a t = 'm constraint 'a = 'v)

Alas, it doesn't work:

2 |     (module Map.S with type key = 'k and type 'a t = 'm constraint 'a = 'v)
                                             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Syntax error: invalid package type: parametrized types are not supported

Package types and their `with' constraints come with many restrictions, which
is deeply unfortunate.

We have to resort to an encoding:

module type maps = sig
  include Map.S
  type v
  type mt
  val of_mt : mt -> v t
  val to_mt : v t -> mt 
end
type ('k,'v,'m) map = 
    (module maps with type key = 'k and type v = 'v and type mt = 'm)

One should mention that this is a strictly more general type of maps:
it supports specialized implementations for particular combination of
keys and values (e.g., if 'v is bool, we can use Set as the underlying
structure.)

The pretty-printer of maps is the same as in the Ann55, with two additions:
two occurrences of M.of_t.

let pp_map : type k v m. (k,v,m) map -> k printer -> v printer -> m printer = 
    fun (module M) pp_key pp_v ppf set -> 
  if M.is_empty (M.of_mt set) then Format.fprintf ppf "ø" else 
  let pp_sep ppf () = Format.fprintf ppf ",@ " in 
  let pp_binding ppf (k,v) = Format.fprintf ppf "@[%a@ =@ %a@]" pp_key k pp_v v 
  in 
  Format.fprintf ppf "@[{@ %a@ }@]" 
    (Format.pp_print_seq ~pp_sep pp_binding) (M.to_seq (M.of_mt set)) 

It applies to statically *unknown* modules however, unlike pp_map in Ann55

type ('k,'v) amap = (module maps with type key = 'k and type v = 'v)

let string_map : type a. unit -> (string,a) amap = fun () -> 
  (module struct
    include Map.Make(String) 
    type v = a
    type mt = v t
    let of_mt = Fun.id
    let to_mt = Fun.id
  end)

let () = 
  let md = string_map () in
  let module M = (val (md : (string,int) amap)) in
  let m = M.of_list ["Zero", 0; "One", 1] in 
  let pp_str = Format.pp_print_int in 
  Format.printf "%a@." 
    (pp_map (module M) Format.pp_print_string pp_str) (M.to_mt m)

I should mention that the functions like to_mt come naturally in case
of tagless-final interpreters: these are the observation functions.
For example:

module type lc = sig
  type 'a repr
  val int : int -> int repr
  val lam  : ('a repr -> 'b repr) -> ('a -> 'b) repr
  val app : ('a -> 'b) repr -> ('a repr -> 'b repr)
  type obst
  type obs
  val observe : obst repr -> obs
end

type ('a,'obs) lc = (module (lc with type obs = 'obs and type obst = 'a))

let ex1 : type obs. (int,obs) lc -> obs = fun (module M) -> let open M in
  let t1 = app (lam (fun x -> x)) (int 1)
  in observe t1

In conclusion, it would be great if one day the restrictions on
package types were relaxed.

Re: [Caml-list] Modular explicits in pre-OCaml 5.5

[Olivier Nicole]

Thanks for pointing this out. Does this mean that modular explicits, 
strictly speaking, bring no additional expressivity but only a simpler 
way to do these things? Or are there programs that could be expressed 
with modular explicits but not with constrained module types?

Re: [Caml-list] Modular explicits in pre-OCaml 5.5

[Samuel Vivien]

Indeed. Modular explicit does not add any expressiveness to the language 
(and does not impact the soundness of the type system). Every program 
that can be written using modular explicits could have been written with 
a functor encoded as a first-class module.

We presented this encoding in section 1.5 of this paper about modular 
explicits : https://hal.science/hal-05428136/document

On 6/25/26 14:45, Olivier Nicole wrote:
> Thanks for pointing this out. Does this mean that modular explicits, 
> strictly speaking, bring no additional expressivity but only a simpler 
> way to do these things? Or are there programs that could be expressed 
> with modular explicits but not with constrained module types?