---

10.7 Substituting inside a signature

• 10.7.1 Destructive substitutions
• 10.7.2 Local substitution declarations
• 10.7.3 Module type substitutions

10.7.1 Destructive substitutions

(Introduced in OCaml 3.12, generalized in 4.06)

A “destructive” substitution (with ... := ...) behaves essentially like normal signature constraints (with ... = ...), but it additionally removes the redefined type or module from the signature.

Prior to OCaml 4.06, there were a number of restrictions: one could only remove types and modules at the outermost level (not inside submodules), and in the case of with type the definition had to be another type constructor with the same type parameters.

A natural application of destructive substitution is merging two signatures sharing a type name.

  module type Printable = sig type t val print : Format.formatter -> t -> unit end module type Comparable = sig type t val compare : t -> t -> int end module type PrintableComparable = sig include Printable include Comparable with type t := t end 

One can also use this to completely remove a field:

  module type S = Comparable with type t := int module type S = sig val compare : int -> int -> int end 

or to rename one:

  module type S = sig type u include Comparable with type t := u end module type S = sig type u val compare : u -> u -> int end 

Note that you can also remove manifest types, by substituting with the same type.

  module type ComparableInt = Comparable with type t = int ;; module type ComparableInt = sig type t = int val compare : t -> t -> int end  module type CompareInt = ComparableInt with type t := int module type CompareInt = sig val compare : int -> int -> int end 

10.7.2 Local substitution declarations

(Introduced in OCaml 4.08)

Local substitutions behave like destructive substitutions (with ... := ...) but instead of being applied to a whole signature after the fact, they are introduced during the specification of the signature, and will apply to all the items that follow.

This provides a convenient way to introduce local names for types and modules when defining a signature:

  module type S = sig type t module Sub : sig type outer := t type t val to_outer : t -> outer end end module type S = sig type t module Sub : sig type t val to_outer : t/1 -> t/2 end end 

Note that, unlike type declarations, type substitution declarations are not recursive, so substitutions like the following are rejected:

  # module type S = sig type 'a poly_list := [ `Cons of 'a * 'a poly_list | `Nil ] end ;; Error: Unbound type constructor poly_list 

10.7.3 Module type substitutions

(Introduced in OCaml 4.13)

Module type substitution essentially behaves like type substitutions. They are useful to refine an abstract module type in a signature into a concrete module type,

  # module type ENDO = sig module type T module F: T -> T end module Endo(X: sig module type T end): ENDO with module type T = X.T = struct module type T = X.T module F(X:T) = X end;; module type ENDO = sig module type T module F : T -> T end module Endo : functor (X : sig module type T end) -> sig module type T = X.T module F : T -> T end 

It is also possible to substitute a concrete module type with an equivalent module types.

  module type A = sig type x module type R = sig type a = A of x type b end end module type S = sig type a = A of int type b end module type B = A with type x = int and module type R = S 

However, such substitutions are never necessary.

Destructive module type substitution removes the module type substitution from the signature

  # module type ENDO' = ENDO with module type T := ENDO;; module type ENDO' = sig module F : ENDO -> ENDO end 

If the right hand side of the substitution is not a path, then the destructive substitution is only valid if the left-hand side of the substitution is never used as the type of a first-class module in the original module type.

  module type T = sig module type S val x: (module S) end module type Error = T with module type S := sig end Error: This `with' constraint S := sig end makes a packed module ill-formed. 

---