In OCaml, a variant declaring its tags with a colon

user_231664 0
Viewed 201

Looking at the following code:

type z = Z of z

type 'a s = Z | S of 'a

type _ t = Z : z t | S : 'n t -> 'n s t

the last line contains a generic variant, or what seems like one, but instead of using the keyword of it uses the colon symbol :. Why is that? And how am I supposed to read this type?

Looking at the OCaml grammar for type declarations: https://ocaml.org/manual/types.html it doesn't seem obvious if this is really a variant, and it even looks like this is a mix of a label and a variant.

variant ocaml types
1 Answers

This is a definition of the generalized algebraic data type (GADT). This language feature was introduced in the 4.0 release of OCaml and the syntax of the regular algebraic data types (ADT) was extended with this column variant to enable constructor-specific constraints.

The regular ADT syntax <Constr> [of <args>] is used to introduce a constructor <Constr> that has the specified arguments, e.g.,

type student = Student of string * int

The generalized syntax, <Constr> : [<args>] -> <constr> uses : instead of of but adds an extra place for specifying the type constraint, e.g.,

type student = Student : string * int -> student

The constraint has to be an instance of the defined type. And it is useful when either the defined type or the constructor arguments (or both) are polymorphic, i.e., reference type variables. A better example is a type-safe abstract syntax tree of an expression language, e.g.,

type _ exp = 
  | Int : int -> int exp
  | Str : string -> string exp
  | Cat : string exp * string exp -> string exp
  | Add : int exp * int exp -> int exp

Using this representation we can write a statically typed interpreter where we will not have to deal with cases Add (Str "foo", Int 42) as it is impossible to construct such values because of the constraints on the Cat constructor, which requires that both arguments have the string type.

Another use case of GADT is to enable existential types that could be used to implement dynamic typing and ad-hoc polymorphism ala Haskell type classes. In an existential constructor, some type variables that occur in the constructor argument types are not present in the constraint type, e.g.,

type show = Show : {data : 'a; show : 'a -> string} -> show
let show (Show {show; data}) = show data

So that now we can have a heterogeneous containers,

let entries = [
    Show {data=42; show=string_of_int};
    Show {data="foo"; show=fun x -> x};
]

Which we can show,

# List.map show entries;;
- : string list = ["42"; "foo"]
user_26254420
Related