Polymorphic variant

An ordinary variant constructor belongs to exactly one type, the one that declared it. A tag like `Zero belongs to no declaration, so any function can produce or consume it, and the type checker tracks which tags a value might carry and which a function can accept^[1][5]. Types of polymorphic variants are structural: two types with the same tags are the same type, whoever wrote them. Garrigue introduced them in Objective Label in 1998 and they have been part of OCaml since version 3.0 in 2000^[1]. Their type inference uses row variables, from Wand's and Rémy's work on extensible records^[3][4][7], to stand for the tags a type might contain beyond those it mentions. They support extensible data types and code reuse^[2], variants shared between libraries, and subtyping encodings with phantom types^[8].

let to_int = function `Zero -> 0 | `Succ n -> n + 1
let zero = `Zero

val to_int : [< `Succ of int | `Zero ] -> int
val zero : [> `Zero ]

Passing zero to to_int unifies [> `Zero ] with [< `Succ of int | `Zero ], which succeeds because the tag the value might carry is one the function accepts. Passing a tag it does not accept fails at compile time, with the tag named in the error.

let to_int = function `Zero -> 0 | `Succ n -> n + 1
let bad = to_int `Minus

File "minus.ml", line 2, characters 17-23:
2 | let bad = to_int `Minus
                     ^^^^^^
Error: This expression has type [> `Minus ]
       but an expression was expected of type [< `Succ of int | `Zero ]
       The second variant type does not allow tag(s) `Minus

A polymorphic variant type has the form $[<T_u>T_l]$: the value carries at most the tags $T_u$ and at least the tags $T_l$^[1][7]. [> `A ] is an open type with lower bound $\{A\}$ and no upper bound; [< `A | `B ] is a closed type with upper bound $\{A,B\}$; [ `A | `B ] has equal bounds. Unifying two such types intersects the upper bounds and unites the lower bounds, and fails if the result has a lower bound not contained in its upper bound. A row variable, shown with as when it appears twice, links the unknown part of two types.

let swap = function `A -> `B | x -> x
let tag = function `Circle r -> 3.14 *. r *. r | `Square s -> s *. s | _ -> 0.

val swap : ([> `A | `B ] as 'a) -> 'a
val tag : [> `Circle of float | `Square of float ] -> float

The type of swap says that whatever set of tags the argument may carry, as long as it may include `A and `B, the result carries the same set. The default case in tag makes it accept any tag, so only the lower bound remains.

Polymorphic variants address the expression problem, adding both new cases and new functions to a data type without editing existing code^[6][2]. The type of subexpressions is left as a parameter, and each language is closed by a recursive type abbreviation. A pattern #base matches exactly the tags of a named type and lets a new evaluator delegate the old cases to the old one.

(* An expression language written with open recursion: 'e is the type of
   subexpressions, left open so that the language can be extended later. *)
type 'e base = [ `Num of int | `Add of 'e * 'e ]
 
let eval_base (eval : 'e -> int) : 'e base -> int = function
  | `Num n -> n
  | `Add (a, b) -> eval a + eval b
 
(* A new constructor, and an evaluator that reuses the old one for the
   tags it already handles. #base matches exactly the tags of base. *)
type 'e ext = [ 'e base | `Mul of 'e * 'e | `Neg of 'e ]
 
let eval_ext (eval : 'e -> int) : 'e ext -> int = function
  | #base as e -> eval_base eval e
  | `Mul (a, b) -> eval a * eval b
  | `Neg a -> - eval a
 
(* Tying the knot: the closed types of each language. *)
type base_expr = base_expr base
type ext_expr = ext_expr ext
 
let rec eval1 (e : base_expr) = eval_base eval1 e
let rec eval2 (e : ext_expr) = eval_ext eval2 e

3 3
-15

The value `Add (`Num 1, `Num 2) belongs to both languages without conversion, since types are structural. With ordinary variants the extended language would need its own constructors and a conversion from the old type, or a single type containing all cases.

Openness has a cost. A function with a default case accepts every tag, including misspelled ones, and the mistake is not caught where it is written:

(* An open type accepts any tag, so a misspelled one is not an error. *)
let is_red = function `Red -> true | _ -> false
 
(* A closed type catches it. *)
type colour = [ `Red | `Green | `Blue ]
let is_red' : colour -> bool = function `Red -> true | _ -> false

true false
true

open Typo
let _ = is_red' `Rde

File "typo_bad.ml", line 2, characters 16-20:
2 | let _ = is_red' `Rde
                    ^^^^
Error: This expression has type [> `Rde ]
       but an expression was expected of type Typo.colour
       The second variant type does not allow tag(s) `Rde

Inferred types can also grow large, since they list every tag and may contain row variables, and error messages show them in full. Most code therefore uses ordinary variants by default, declares closed types for polymorphic variants that cross module boundaries, and uses open types where the openness is the point^[5].

A tag is represented by a hash of its name: a constant tag is an integer, and a tag with an argument is a block holding the hash and the argument. Since there is no declaration to number the tags, the hash plays that role, and the compiler reports an error if two tags in one type have the same hash^[5]. Pattern matching compares hashes, and is compiled to a binary search or a jump table as for ordinary variants.

Wand introduced row variables for type inference of extensible records and objects in 1987^[4], and Rémy developed the approach for ML records and variants^[3]. Garrigue designed polymorphic variants for the Objective Label language in 1998, where they were used among other things for the LablGTK bindings to GTK^[1]; they were merged into OCaml 3.0 in 2000, together with labeled arguments. Garrigue showed their use for code reuse and extensible programs in 2000^[2] and gave a simplified account of their type inference in 2002^[7]. Fluet and Pucella used them to encode subtyping hierarchies with phantom types^[8].

• Phantom typeA phantom type is a type parameter that appears in a type's declaration but in none of its fields, used to keep otherwise identical representations apart: lengths in metres and in feet, validated and unvalidated strings, read-only and writable handles, SQL expressions of different result types. It carries no data and costs nothing at run time. Combined with an abstract type whose constructors are hidden, it lets a library enforce invariants through the type checker. Unlike a GADT index it tells a pattern match nothing; it constrains what callers may do, not what the compiler can learn.
• GADTA generalized algebraic data type (GADT) is an algebraic data type whose constructors may each give a more specific result type than the declared one, instead of all sharing one polymorphic return type. Matching on a constructor then tells the type checker what the type parameter was, so a single well-typed eval can return an int for an Add node and a bool for an Eq node, checked at compile time rather than by a run-time tag test. GADTs express typed syntax trees, type representations and equality proofs, typed format strings and length-indexed data. The price is that type inference needs annotations.
• Value restrictionThe value restriction is the rule, in ML-family languages, that a let-bound expression has its type variables generalized only if it is a syntactic value, such as a function, a constant or a constructor applied to values. An application such as List.map f or ref [] is not a value, so its type variables stay weak and are fixed by their first use. Without the restriction, a reference could be given a polymorphic type and used to store a value at one type and read it at another. OCaml relaxes the rule for type variables that occur only covariantly.
• Algebraic data typeAn algebraic data type is a type built from sums, where a value is one of several alternatives, and products, where a value has several components at once, possibly recursively. The name comes from counting: the number of values of a sum is the sum of the counts, and of a product their product, so types obey the laws of algebra. Values are taken apart by pattern matching, which the compiler checks for missing cases.
• Type-directed disambiguationType-directed disambiguation is OCaml's rule, since version 4.01, for deciding which record type a field label, or which variant type a constructor, belongs to when several in scope share the name: if the expected type is already known at that point of type inference, it decides; otherwise the most recently defined type with that name wins. It also lets labels and constructors be used without being in scope when the type is known. Because the outcome depends on what inference knows at each point, the -principal flag warns when a choice relied on information that a different inference order might not have had.
• PrismA prism is the counterpart of a lens for sum types: a partial getter, preview, that succeeds only on one case, and a builder, review, that makes a whole value from that case's contents. Two laws make them agree. Prisms compose with each other, and a lens composed with a prism gives an affine traversal, which has at most one focus and no builder. They make deep edits into data like JSON or syntax trees safe when the path does not exist, and they are one of the standard optics, alongside lenses, isos and traversals.

• Lenses and Prisms in OCamlAn optics library whose kinds are a phantom polymorphic variant, and a ppx that derives lenses from records, prisms from variants, and both from field paths and patterns.

1. [1]J. Garrigue, “Programming with polymorphic variants”, ML Workshop (1998).
2. [2]J. Garrigue, “Code reuse through polymorphic variants”, Workshop on Foundations of Software Engineering (2000).
3. [3]D. Rémy, “Type inference for records in a natural extension of ML”, in C. A. Gunter, J. C. Mitchell (eds.), Theoretical Aspects of Object-Oriented Programming, MIT Press (1994).
4. [4]M. Wand, “Complete type inference for simple objects”, LICS (1987).
5. [5]OCaml manual, “Polymorphic variants”.
6. [6]P. Wadler, “The expression problem”, message to the java-genericity mailing list (1998).
7. [7]J. Garrigue, “Simple type inference for structural polymorphism”, FOOL (2002).
8. [8]M. Fluet, R. Pucella, “Phantom types and subtyping”, Journal of Functional Programming 16 (2006).

last updated 29 September 2026