Polymorphic variant

also: polymorphic variants, open variant, row type

A variant whose constructors, called tags and written with a backquote, exist independently of any type declaration. Their types are sets of tags with bounds: [> `A] means at least `A, [< `A | `B] at most those two, and unification works out unions and intersections of those sets.

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.

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 `Minus would fail at compile time, with the tag named in the error.

The same machinery works as a type-level set with no values at all: a phantom parameter can be an open polymorphic variant, so that unifying two of them computes a union. Error messages are longer than for ordinary variants, and a typo in a tag inside an open type is not caught where it is written, which is why most code keeps them for the places that need the openness.

• Phantom typeA type parameter that appears in a type's signature but in none of its fields, used purely to keep two otherwise identical representations from being mixed up. Unlike a GADT it adds no information at pattern-match time: it constrains what the caller may do, not what the compiler can learn.
• GADTGeneralized Algebraic Data Type: an ADT whose constructors may each refine the type parameter of the value they build, instead of every constructor sharing one polymorphic return type. This lets a single well-typed eval return an int for an Add node and a bool for an Eq node, checked at compile time rather than by an unchecked cast.
• Value restrictionThe rule that only syntactic values have their type variables generalized in a let. An application such as List.map f is not a value, so its type variables stay weak, fixed by the first use. OCaml relaxes the rule for type variables that occur only covariantly.
• PrismThe counterpart of a lens for sum types: a partial getter that succeeds only on one constructor, and a builder that makes a whole value from that constructor's contents. A lens composed with a prism has at most one focus and no builder, which is called an affine traversal.
• Type-directed disambiguationOCaml's rule, since 4.01, for deciding which record type a field label or which variant a constructor belongs to when several in scope share the name: if the expected type is already known at that point, it decides; otherwise the most recently defined type with that name wins.

• 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.

• J. Garrigue, “Programming with polymorphic variants”, ML Workshop (1998).
• J. Garrigue, “Code reuse through polymorphic variants”, Workshop on Foundations of Software Engineering (2000).