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?

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?

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

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

It was indeed (I had renamed `a`

to `t`

to avoid some potential confusion and missed this instance).

Thank you for awesome explanation!