8.11 Generalized algebraic datatypes

(Introduced in OCaml 4.00)

Generalized algebraic datatypes, or GADTs, extend usual sum types intwo ways: constraints on type parameters may change depending on thevalue constructor, and some type variables may be existentiallyquantified.Adding constraints is done by giving an explicit return type(the rightmost typexpr in the above syntax), where type parametersare instantiated.This return type must use the same type constructor as the type beingdefined, and have the same number of parameters.Variables are made existential when they appear inside a constructor’sargument, but not in its return type.

Since the use of a return type often eliminates the need to name typeparameters in the left-hand side of a type definition, one can replacethem with anonymous types _ in that case.

The constraints associated to each constructor can be recoveredthrough pattern-matching.Namely, if the type of the scrutinee of a pattern-matching containsa locally abstract type, this type can be refined according to theconstructor used.These extra constraints are only valid inside the corresponding branchof the pattern-matching.If a constructor has some existential variables, fresh locallyabstract types are generated, and they must not escape thescope of this branch.

Recursive functions

Here is a concrete example:

 type _ term =
   | Int : int -> int term
   | Add : (int -> int -> int) term
   | App : ('b -> 'a) term * 'b term -> 'a term
 let rec eval : type a. a term -> a = function
   | Int n    -> n                 (* a = int *)
   | Add      -> (fun x y -> x+y)  (* a = int -> int -> int *)
   | App(f,x) -> (eval f) (eval x)
           (* eval called at types (b->a) and b for fresh b *)
 

 let two = eval (App (App (Add, Int 1), Int 1))
val two : int = 2

It is important to remark that the function eval is using thepolymorphic syntax for locally abstract types. When defining a recursivefunction that manipulates a GADT, explicit polymorphic recursion shouldgenerally be used. For instance, the following definition fails with atype error:

 let rec eval (type a) : a term -> a = function
   | Int n    -> n
   | Add      -> (fun x y -> x+y)
   | App(f,x) -> (eval f) (eval x)
Error: This expression has type ($App_'b -> a) term
       but an expression was expected of type 'a
       The type constructor $App_'b would escape its scope

In absence of an explicit polymorphic annotation, a monomorphic typeis inferred for the recursive function. If a recursive call occursinside the function definition at a type that involves an existentialGADT type variable, this variable flows to the type of the recursivefunction, and thus escapes its scope. In the above example, this happensin the branch App(f,x) when eval is called with f as an argument.In this branch, the type of f is ($App 'b-> a). The prefix $ in$App 'b denotes an existential type named by the compiler(see 8.11). Since the type of eval is'a term -> 'a, the call eval f makes the existential type $App_'bflow to the type variable 'a and escape its scope. This triggers theabove error.

Type inference

Type inference for GADTs is notoriously hard.This is due to the fact some types may become ambiguous when escapingfrom a branch.For instance, in the Int case above, n could have either type intor a, and they are not equivalent outside of that branch.As a first approximation, type inference will always work if apattern-matching is annotated with types containing no free typevariables (both on the scrutinee and the return type).This is the case in the above example, thanks to the type annotationcontaining only locally abstract types.

In practice, type inference is a bit more clever than that: typeannotations do not need to be immediately on the pattern-matching, andthe types do not have to be always closed.As a result, it is usually enough to only annotate functions, as inthe example above. Type annotations arepropagated in two ways: for the scrutinee, they follow the flow oftype inference, in a way similar to polymorphic methods; for thereturn type, they follow the structure of the program, they are spliton functions, propagated to all branches of a pattern matching,and go through tuples, records, and sum types.Moreover, the notion of ambiguity used is stronger: a type is onlyseen as ambiguous if it was mixed with incompatible types (equated byconstraints), without type annotations between them.For instance, the following program types correctly.

 let rec sum : type a. a term -> _ = fun x ->
   let y =
     match x with
     | Int n -> n
     | Add   -> 0
     | App(f,x) -> sum f + sum x
   in y + 1
val sum : 'a term -> int = <fun>

Here the return type int is never mixed with a, so it is seen asnon-ambiguous, and can be inferred.When using such partial type annotations we strongly suggestspecifying the -principal mode, to check that inference isprincipal.

The exhaustiveness check is aware of GADT constraints, and canautomatically infer that some cases cannot happen.For instance, the following pattern matching is correctly seen asexhaustive (the Add case cannot happen).

 let get_int : int term -> int = function
   | Int n    -> n
   | App(_,_) -> 0
 

Refutation cases

(Introduced in OCaml 4.03)

Usually, the exhaustiveness check only tries to check whether thecases omitted from the pattern matching are typable or not.However, you can force it to try harder by adding refutation cases:

In presence of a refutation case, the exhaustiveness check will firstcompute the intersection of the pattern with the complement of thecases preceding it. It then checks whether the resulting patterns canreally match any concrete values by trying to type-check them.Wild cards in the generated patterns are handled in a special way: iftheir type is a variant type with only GADT constructors, then thepattern is split into the different constructors, in order to check whetherany of them is possible (this splitting is not done for arguments of theseconstructors, to avoid non-termination). We also split tuples andvariant types with only one case, since they may contain GADTs inside.For instance, the following code is deemed exhaustive:

 type _ t =
   | Int : int t
   | Bool : bool t
 let deep : (char t * int) option -> char = function
   | None -> 'c'
   | _ -> .
 

Namely, the inferred remaining case is Some , which is split intoSome (Int, ) and Some (Bool, _), which are both untypable becausedeep expects a non-existing char t as the first element of the tuple.Note that the refutation case could be omitted here, because it isautomatically added when there is only one case in the patternmatching.

Another addition is that the redundancy check is now aware of GADTs: acase will be detected as redundant if it could be replaced by arefutation case using the same pattern.

Advanced examples

The term type we have defined above is an indexed type, wherea type parameter reflects a property of the value contents.Another use of GADTs is singleton types, where a GADT valuerepresents exactly one type. This value can be used as runtimerepresentation for this type, and a function receiving it can have apolytypic behavior.

Here is an example of a polymorphic function that takes theruntime representation of some type t and a value of the same type,then pretty-prints the value as a string:

 type _ typ =
   | Int : int typ
   | String : string typ
   | Pair : 'a typ * 'b typ -> ('a * 'b) typ
 let rec to_string: type t. t typ -> t -> string =
   fun t x ->
   match t with
   | Int -> Int.to_string x
   | String -> Printf.sprintf "%S" x
   | Pair(t1,t2) ->
       let (x1, x2) = x in
       Printf.sprintf "(%s,%s)" (to_string t1 x1) (to_string t2 x2)
 

Another frequent application of GADTs is equality witnesses.

 type (_,_) eq = Eq : ('a,'a) eq
 let cast : type a b. (a,b) eq -> a -> b = fun Eq x -> x
 

Here type eq has only one constructor, and by matching on it oneadds a local constraint allowing the conversion between a and b.By building such equality witnesses, one can make equal types whichare syntactically different.

Here is an example using both singleton types and equality witnessesto implement dynamic types.

 let rec eq_type : type a b. a typ -> b typ -> (a,b) eq option =
   fun a b ->
   match a, b with
   | Int, Int -> Some Eq
   | String, String -> Some Eq
   | Pair(a1,a2), Pair(b1,b2) ->
       begin match eq_type a1 b1, eq_type a2 b2 with
       | Some Eq, Some Eq -> Some Eq
       | _ -> None
       end
   | _ -> None
 type dyn = Dyn : 'a typ * 'a -> dyn
 let get_dyn : type a. a typ -> dyn -> a option =
   fun a (Dyn(b,x)) ->
   match eq_type a b with
   | None -> None
   | Some Eq -> Some x
 

Existential type names in error messages

(Updated in OCaml 4.03.0)

The typing of pattern matching in presence of GADT can generate manyexistential types. When necessary, error messages refer to theseexistential types using compiler-generated names. Currently, thecompiler generates these names according to the following nomenclature:

• First, types whose name starts with a $ are existentials.
• $Constr_'a denotes an existential type introduced for the typevariable 'a of the GADT constructor Constr:

 type any = Any : 'name -> any
 let escape (Any x) = x
Error: This expression has type $Any_'name
       but an expression was expected of type 'a
       The type constructor $Any_'name would escape its scope

• $Constr denotes an existential type introduced for an anonymous type variable in the GADT constructor Constr:

 type any = Any : _ -> any
 let escape (Any x) = x
Error: This expression has type $Any but an expression was expected of type
         'a
       The type constructor $Any would escape its scope

• $'a if the existential variable was unified with the type variable 'a during typing:

 type ('arg,'result,'aux) fn =
   | Fun: ('a ->'b) -> ('a,'b,unit) fn
   | Mem1: ('a ->'b) * 'a * 'b -> ('a, 'b, 'a * 'b) fn
  let apply: ('arg,'result, _ ) fn -> 'arg -> 'result = fun f x ->
   match f with
   | Fun f -> f x
   | Mem1 (f,y,fy) -> if x = y then fy else f x
Error: This pattern matches values of type
         ($'arg, 'result, $'arg * 'result) fn
       but a pattern was expected which matches values of type
         ($'arg, 'result, unit) fn
       The type constructor $'arg would escape its scope

• $n (n a number) is an internally generated existential which could not be named using one of the previous schemes.As shown by the last item, the current behavior is imperfectand may be improved in future versions.

Equations on non-local abstract types

(Introduced in OCaml4.04)

GADT pattern-matching may also add type equations to non-localabstract types. The behaviour is the same as with local abstracttypes. Reusing the above eq type, one can write:

 module M : sig type t val x : t val e : (t,int) eq end = struct
   type t = int
   let x = 33
   let e = Eq
 end
 let x : int = let Eq = M.e in M.x
 

Of course, not all abstract types can be refined, as this wouldcontradict the exhaustiveness check. Namely, builtin types (thosedefined by the compiler itself, such as int or array), andabstract types defined by the local module, are non-instantiable, andas such cause a type error rather than introduce an equation.