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

Question

The OCaml manual describes the "constraint" keyword, which can be used in a type definition. However, I cannot figure out any usage that can be done with this keyword. When is this keyword is useful? Can it be used to remove polymorphic type variables? (so that a type 'a t in a module becomes just t and the module can be used in a functor argument which requires t with no variables.)

Answer 1

So, the constraint keywords, used in type or class definitions, let one "reduce the scope” of applicable types to a type parameter, so to speak. The documentation clearly announce that type expressions from both sides of the constraint equation will be unified to "refine" the types the constraint relates to. Because they are type expressions, you may use all the usual type 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; }

Observe how type unification simplifies the equations, in the first example by getting rid of the extraneous type product (* int), and in the second case eliminating it altogether. Note also that I used a type variable 'c which only appears in the right hand side of the type definition.

Two interesting uses are with polymorphic variants and class types, both based on row-polymorphism. Constraints allow to express certain subtyping relations. By subtyping, for variants, we mean a relation such that any constructor of a type is present in its subtypes. Some of these relations may already be expressed monomorphically:

# 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 ]

There, op is a subtype of both sum_op and prod_op.

But in some cases, you have to introduce polymorphism, and this is where constraints come handy:

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

The above let you denote the family of types which are subtypes of op : the type instance is 'a itself for a given instance of 'a t.

If we try to define the same type without a parameter, the type unification algorithm will complain:

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

The same sort of constraints may be expressed with class types, and the same problem may arise if the type definition is implicitly polymorphic by subtyping.

# 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