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

[oleg@okmij.org]

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.