How to unpack 'module type' packed to 'type' back to 'module type'?

Question

We can pack module to value and unpack it back to module (modules as first-class citizens). Also, we can pack module type to type, but... Is it possible to unpack module type from type? If it is - How? If it is not - Why? The following sketch shows what I mean.

module type S = sig
  type t
end

type 'a t = (module S with type t = 'a)

module type S' = sig
  include SIG_FROM ( int t )
end

or

module type S'' = SIG_FROM ( int t )

Added Note:

So why I am asking about it. Very often Ocaml can't infer the type of the first-class module instance and it should be annotated. It is possible to do in two ways:

1) by signature

module type INTERNAL_S = 
  EXTERNAL_S with type a = char
              and type b = int
              and type c = string

let f (module M : INTERNAL_S) a b c =
  M.f a b (c * 2)

2) by type

type e = 
  ( module EXTERNAL_S 
      with type a = char
       and type b = int
       and type c = string
  )

let f ((module M) : e) a b =
  M.f a (b * 2)

As common second way is shorter and easy to read especially in signatures (.mli).

val g : (module INTERNAL_S) -> (module INTERNAL_S) -> 
        char -> int -> string

val g : e -> e -> char -> int -> string

And we create types from module types to simplify code reading or in the case when it is necessary (for example when it is expected by functor). And some-time I need type only but have to declare module type too because the support of constraining new types from module types are limited

and constraining new types (bound to module type) from types (bound to module types) is missing.

(* this kind of constructing is possible *)
let x : 'a t = (module struct 
                  include A 
                  include B
                  include (val C.some_value)
                  let new_f o = o
                end) 

(* but this isn't *)
type 'a t = (module sig 
               include A with type t = t
               include B with type t := t
               include SIG_FROM ( (int, int) sig_type  )
               val new_f : t -> t
             end)

As for me, this way back makes modules more first-class. Also, it is symmetric with the relationship between instances and modules (as I understand let x = (module X) and let module X = (val x) are also bindings). Symmetry - it is good (for example it partially exists between function and functors). But as I see in this place OCaml has a border between module language and core language. I asked "how" because have hope and ask "why" because sure that this question was opened in the design process of OCaml, so this border is based on some decisions and reasons.

ivg ivg · Accepted Answer · 2020-06-10T13:58:08

The type definition

type 'a t = (module S with type t = 'a)

is not really a packing of the module of type S to type t but a type alias that gives a shorter name, 'a t to the type expression (module S with type t = 'a), which denotes modules of type S polymorphic over the type t that they define.

Anywhere where you have a value of type 'a t as long as 'a t is not abstracted and known to be equal to (module S with type t = 'a) you can unpack this value and even use it as a parameter to functor. You can even recover the module type of the packed module using the module type of construct, e.g.,

let apply : type a. a t -> unit = fun (module S) ->
  let module X = struct
    module type S' = sig
      include module type of S
    end
  end in ()

As a side-note, you can also pack modules that define signatures, e.g.,

module type Algebra = sig
  module type S = sig
    type t
    val add : t -> t -> t
    val sub : t -> t -> t
  end
end

type signature = (module Algebra)

Then we can define SIGFROM as

module SIGFROM(A : Algebra) = struct
  module type S = A.S
end

and unpack the signature from the packed module


let example : signature -> unit = fun s ->
  let module A = SIGFROM(val s) in
  let module B = struct
    module type S = A.S
    type t = (module S)
    type t0 = (module A.S)
    type 'a t1 = (module A.S with type t = 'a)
  end in
  ()

We can't, however write directly,

type t = (module SIGFROM(val s))

or even build a module type of the packaged module from existing and defined on a top-level signatures, e.g.,

type t = (module sig include module type of Int end)

doesn't work, but

module type I = sig include module type of Int end
type t = (module I)

works, though apparently it looks semantically equal (cf, that we also we can say Map.Make(Int).t but can't say Map.Make(Int).empty, we have to bind the module expression to a module name before that).¹

Syntactically, the packed module type expression should be (module <package-type>) where a packaged type is either an identifier or an identifier with a limited number of constraints. Of course, the underlying reason for this limitation is not the parser and syntax but the complexity of type-inference. The underlying problem is really hard to explain, but it comes from the power of the module system and functors so that it is very easy to introduce unsoundness if the full power of module expressions will be allowed in the module types.

This is not to say, that there is a significant theoretical limitation, basically, we're hitting the limit of the original design (which is probably fine for a language that was created in 1970 as a meta language for a proof assistant, with modules added many years later, and first class modules rather recently).

If the language were to designed from scratch, then the separation between values and modules would be less rough, if exist at all, e.g., see the 1ML language.

How to unpack 'module type' packed to 'type' back to 'module type'?

1 Answers

Further Readings