Can someone explain the type syntax used in this OCaml program?

Question

The types below are taken from this question

(* contains an error, later fixed by the OP *)
type _ task =
| Success : 'a -> 'a task
| Fail : 'a -> 'a task
| Binding : (('a task -> unit) -> unit) -> 'a task
| AndThen : ('a -> 'b task) * 'a task -> 'b task
| OnError : ('a -> 'b task) * 'a task -> 'b task

type _ stack =
| NoStack : 'a stack
| AndThenStack : ('a -> 'b task) * 'b stack -> 'a stack
| OnErrorStack : ('a -> 'b task) * 'b stack -> 'a stack

type 'a process = 
{ root: 'a task 
; stack: 'a stack 
}

I'm relatively new to OCaml, but I've never seen : syntax used like that before. For example, I've seen polymorphic types defined like this, using the of syntax

type 'a expr =
    | Base  of 'a
    | Const of bool
    | And   of 'a expr list
    | Or    of 'a expr list
    | Not   of 'a expr

In the original question, It's not obvious to me how the variants are even constructed, since it looks like each one does not accept an argument. Take this simplified example

type 'a stack =
  | Foo : int stack
  | Bar : string stack
;;
type 'a stack = Foo : int stack | Bar : string stack

Try making an int stack using Foo

Foo 5;;
Error: The constructor Foo expects 0 argument(s),
       but is applied here to 1 argument(s)

However, without an argument

Foo;;
- : int stack = Foo

Ok, but where's the int? How to store data in this type?

In the OP's program below, he/she is matching on the types "normally", eg Success value -> ... or Fail value -> .... Again, how is this value constructed if the variant constructor doesn't accept an argument?

let rec loop : 'a. 'a process -> unit = fun proc ->
match proc.root with
| Success value -> 
    let rec step = function
    | NoStack -> ()
    | AndThenStack (callback, rest) -> loop {proc with root = callback value; stack = rest }
    | OnErrorStack (_callback, rest) -> step rest  <-- ERROR HERE
    in
    step proc.stack
| Fail value -> 
    let rec step = function
    | NoStack -> ()
    | AndThenStack (_callback, rest) -> step rest
    | OnErrorStack (callback, rest) -> loop {proc with root = callback value; stack = rest }
    in
    step proc.stack
| Binding callback -> callback (fun task -> loop {proc with root = task} )
| AndThen (callback, task) -> loop {root = task; stack = AndThenStack (callback, proc.stack)}
| OnError (callback, task) -> loop {root = task; stack = OnErrorStack (callback, proc.stack)}

Can someone help me filling in my knowledge gap?

Answer 1

Those types are Generalized Algebraic Data Types. Also known as GADTs . GADTs make it possible to refine the relationship between constructors and types.

In your example, GADTs are used as a way to introduce existentially quantified type: removing irrelevant constructors, one could write

type 'a task =
| Done of 'a
| AndThen : ('a -> 'b task) * 'a task -> 'b task

Here, AndThen is a constructor that takes two arguments: a callback of type 'a -> 'b task and a 'a task and returns a task of type 'b task. A striking feature of this definition is that the type variable 'a only appears inside the arguments of the constructor. A natural question is then if I have a value AndThen(f,t): 'a task, what is the type of f?

And the answer is that the type of f is partially unknown, I only know that there is a type ty such that both f: ty -> 'a task and t: ty. But at this point all information beyond the mere existence of ty has been lost. For this reason, the type ty is called an existentially quantified type.

But here, this small information is still enough to manipulate meaningfully such value. I can define a function step

let rec step: type a. a task -> a task = function
| Done _ as x -> x
| AndThen(f,Done x) -> f x
| AndThen(f, t) -> AndThen(f, step t)

which try to apply the function f in the constructor AndThen if possible, using the information than the constructor AndThen always stores pair of callback and task that are compatible.

For instance

let x: int task = Done 0
let f: int -> float task =  fun x -> Done (float_of_int (x + 1))
let y: float task = AndThen(f,x)
;; step y = Done 1.