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.
moduletype Printable = sigtype t
val print : Format.formatter -> t -> unit
endmoduletype Comparable = sigtype t
val compare : t -> t -> int
endmoduletype PrintableComparable = siginclude Printable
include Comparable withtype t := t
end
One can also use this to completely remove a field:
moduletype S = Comparable withtype t := int
moduletype S = sigval compare : int -> int -> int end
or to rename one:
moduletype S = sigtype u
include Comparable withtype t := u
end
moduletype S = sigtype u val compare : u -> u -> int end
Note that you can also remove manifest types, by substituting with the
same type.
moduletype ComparableInt = Comparable withtype t = int ;;
moduletype ComparableInt = sigtype t = int val compare : t -> t -> int end
moduletype CompareInt = ComparableInt withtype t := int
moduletype CompareInt = sigval compare : int -> int -> int end
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:
moduletype S = sigtype t
module Sub : sigtype outer := t
type t
val to_outer : t -> outer
endend
moduletype S =
sigtype t module Sub : sigtype t val to_outer : t/1 -> t/2 endend
Note that, unlike type declarations, type substitution declarations are not
recursive, so substitutions like the following are rejected:
#moduletype S = sigtype 'a poly_list := [ `Cons of 'a * 'a poly_list | `Nil ]
end ;;