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 ;;
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,
#moduletype ENDO = sigmoduletype T
module F: T -> T
endmodule Endo(X: sigmoduletype T end): ENDO withmoduletype T = X.T =
structmoduletype T = X.T
module F(X:T) = X
end;;
moduletype ENDO = sigmoduletype T module F : T -> T endmodule Endo :
functor (X : sigmoduletype T end) ->
sigmoduletype T = X.T module F : T -> T end
It is also possible to substitute a concrete module type with an
equivalent module types.
moduletype A = sigtype x
moduletype R = sigtype a = A of x
type b
endendmoduletype S = sigtype a = A of int
type b
endmoduletype B = A withtype x = int andmoduletype R = S
However, such substitutions are never necessary.
Destructive module type substitution removes the module type substitution
from the signature
#moduletype ENDO' = ENDO withmoduletype T := ENDO;;
moduletype ENDO' = sigmodule 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.
moduletype T = sigmoduletype S val x: (module S) endmoduletype Error = T with module type S := sig end
Error: This `with' constraint S := sig end makes a packed module ill-formed.