What can be done with the keyword "restriction" in OCaml

Question

The OCaml User Guide describes the keyword "restriction" that can be used in a type definition. However, I can’t understand what use can be used with this keyword. When is this keyword useful? Can it be used to remove variable polymorphic types? (so that the type "t in the module becomes equal to t, and the module can be used in a functor argument that requires t without variables.)

Answer 1

So, the keywords constraintused in the definitions of types or classes allow you to "reduce the scope" of applicable types to a type parameter, so to speak. The documentation clearly states that type expressions on both sides of the constraint equation will be unified to “clarify” the types to which the constraint refers. Since they are type expressions, you can use all the usual level operators.

Examples:

# type 'a t = int * 'a constraint 'a * int = float * int;;
type 'a t = int * 'a constraint 'a = float

# type ('a,'b) t = 'c r constraint 'c = 'a * 'b
    and 'a r = {v1 : 'a; v2 : int };;
type ('a,'b) t = ('a * 'b) r
and 'a r = { v1 : 'a; v2 : int; }

Watch how type unification simplifies equations, in the first example, getting rid of the extraneous type of the product ( * int), and in the second case completely eliminating it. Also note that I used a type variable 'cthat appears only on the right side of the type definition.

- , . . , . :

# type sum_op = [ `add | `subtract ];;
type sum_op = [ `add | `subtract ]
# type prod_op = [ `mul | `div ];;
type prod_op = [ `mul | `div ]
# type op = [ sum_op | prod_op ];;
type op = [ `add | `div | `mul | `sub ]

op sum_op, prod_op.

, :

# type 'a t = 'a constraint [> op ] = 'a;;
type 'a t = 'a constraint 'a = [> op ]

, op: 'a 'a t.

, :

# type t' = [> op];;
Error: A type variable is unbound in this type declaration.
In type [> op ] as 'a the variable 'a is unbound

, , .

# class type ct = object method v : int end;;
class type ct =  object method v : int end
# type i = #ct;;
Error: A type variable is unbound in this type declaration.
In type #ct as 'a the variable 'a is unbound
# type 'a i = 'a constraint 'a = #ct;;
type 'a i = 'a constraint 'a = #ct