8.8 Substituting inside a signature

• 8.8.1 Destructive substitutions
• 8.8.2 Local substitution declarations

8.8.1 Destructive substitutions

(Introduced in OCaml 3.12, generalized in 4.06)

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

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

A natural application of destructive substitution is merging twosignatures 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 thesame 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

8.8.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 areintroduced during the specification of the signature, and will apply to all theitems that follow.

This provides a convenient way to introduce local names for types and moduleswhen 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 notrecursive, 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