What does it mean to have colons ":" and arrows "->" in user defined type definitions?

I am seeing:

type 'l generic_argument =
| GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument

cross: What does it mean to have colons “:” and arrows “->” in user defined type definitions in OCaml? - Stack Overflow
but I don’t understand what that means.

I know what the typical of t1 * t2 .... * tn syntax means e.g.

type 'a list =
  | Nil
  | Cons of 'a * ('a list);;

but don’t know what the colon : and -> mean in type definitions. What does it mean?

Btw, I’ve seen -> them in pattern matching.

credit: types - In OCaml, a variant declaring its tags with a colon - Stack Overflow


copy pasted:

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 {data=x;show}) = show x

So that now we can have a heterogenous 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"]
5 Likes