How to read/understand function signature with GADT?

Learning
1

For example, given the code:

let rec eval : type a . a term -> a = ...

How to read/understand this part: type a . a term -> a? What does the dot here mean? Why should we define type a in the function’s signature?

2

This came up on IRC a day or two ago. a . apparently means ∀a

There’s documentation in the manual on this, but it’s quite hard to find.

1 Like
3

There is two things going on simultaneously here. The first is that GADTs can only add equation to abstract types in a pattern matching. For instance, let’s consider the toy example

type a = Tag_a
type b = Tag_b
type _ t =
  | A: a t
  | B: b t

then

let to_string = function
  | A -> "a"
  | B -> "b"

yields a type error

Error: This pattern matches values of type b t
but a pattern was expected which matches values of type a t
Type b is not compatible with type a

because the type of the argument was inferred to a t in the first branch of the pattern matching.

The solution is to make the type phantom parameter of t a locally abstract type in to_string.

let to_string (type any) (x: any t) = match x with
  | A -> "a"
  | B -> "b"

The notation (type any) introduces a local abstract type named any, since the type is abstract, it can be refined to different types in the branches of the pattern matching.

The second point is that recursive function involving GADTs often needs to be recursive polymorphic.
For instance, with a toy langage,

type _ term  =
  | Bool : bool -> bool term
  | Int : int -> int term
  | If : bool term * 'a term * 'a term -> 'a term

an eval function would look like

let rec eval (type t) (x:t term): t = match x with
| Bool b -> b
| Int x -> x
| If (cond,then',else') -> if eval cond then eval then' else eval else'

but in the If branch eval is called with an argument of a different types, which result in a type error

Error: This expression has type t term but an expression was expected of type
bool term

on the first call with a different value for the term type parameter.
The long-winded solution here is to add an explicit polymorphic annotation and then introduce
locally abstract types

let rec eval: 't. 't term -> 't = 
fun (type t) (x: t term): t -> match x with
| Bool b -> b
| Int x -> x
| If (cond,then',else') -> if eval cond then eval then' else eval else'

Since this is a bit of a mouthful, there is shorter variant that directly combines explicit polymorphic annotation with locally abstract types:

let rec eval: type t. t term -> t = function
| Bool b -> b
| Int x -> x
| If (cond,then',else') -> if eval cond then eval then' else eval else'

Here type t. … declares t as both a locally abstract types and makes it explicitly polymorphic.

14 Likes
4

Is that a typo, @octachron?

5

It was indeed (I had renamed a to t to avoid some potential confusion and missed this instance).

6

Thank you for awesome explanation!