Need help to understand GADTs

Learning
1

Hi,

The following snippet from The Manual,

type _ term =
    | Int : int -> int term
    | Add : (int -> int -> int) term
    | App : ('b -> 'a) term * 'b term -> 'a term ;;

I am having a hard time to understand that App (Add, Int 1) is of type (int -> int) term.

Please help me to understand it. Thanks.

Regards

1 Like
2

Let’s use the typing rules:

The definition of Int says that if n has type int them Int n has type int term.
The definition of Add (the constructor) says that Add (the expression) has type (int -> int -> int) term.
The definition of App says that if f has type ('b -> 'a) term and x has type 'b term (for some 'a and 'b) then App (f, x) has type 'a term.

So Int 1 has type int term (first rule)
And in the third rule, replacing f by Add and x by Int 1 (using int for b and int -> int for 'a) we get that App (f, x) (ie App (Add, Int 1)) has type (int -> int) term.

(int -> int -> int is the same as (int -> (int -> int))

2 Likes
3

It makes me click. Thank you.

1 Like
4

Hi,
Emillon gave you an answer to your question, and I will not add to his answer. However there is another examples of GADT that you may want to check out :
https://www.zapashcanon.fr/ocaml
Just scroll down to the “GADT” section.

1 Like
5

App (Add, Int 1) is of type (int -> int) term for the same reason that (+) 1 is of type int -> int.
And yes the -> operator is right-associative (because application is left-associative).

1 Like
6

For completeness, here is the most practical and intuitive explanation of GADTs I saw so far: Writing a Game Boy Emulator in OCaml - The Linoscope Machine

2 Likes