In OCaml, a variant declaring its tags with a colon

Question

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.

Botulism

The definition of t is a GADT. The documentation is here: ocaml.org/releases/4.13/htmlman/gadts.html. In essence t represents a Peano model of the integers (it seems to me). So maybe z isn't such a useless type after all. – Georgeanngeorgeanna

oh I see, that's the GADT syntax. BTW isn't the constructor Z in the type z shadowed by the type s similarly named tag? – Carlinecarling

Does this answer your question? Creating GADT expression in OCaml – Alleyn

likely related: #72985872 – Abduct

related: #72972310 – Abduct

Answer 1

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

Ingenuous

Can I understand the "constraint" as kind of like the "return type" of the constructor? That's how it looks in these examples e.g. Add : int exp * int exp -> int exp means that Add (Int 1, Int 1) should return ... Int 2 I guess? – Growing

Sort of, it is the type that is ascribed to this constructor. It could be an arbitrary type, e.g., you can freely define something like Add : int exp * int exp -> string exp if you like, so it is not necessary that the constraint type has any relevance to the construction of the variant. – Ingenuous

thanks for explaining! I sort of get it, need to have a play around for myself... – Growing