 Hello everyone, I have been experimenting with OCaml GADTs and I have run into two brick walls, and I need help.

## First question

I have a GADT that looks like this:

``````type _ gadt =
| O : 'a -> 'a option gadt
| A : 'a -> 'a gadt
``````

I would like to write a function that essentially would do the following, however, I’m currently convinced it is impossible to write the type for such a function:

``````let map t ~f =
match t with
| O x -> O (f x)
| A x -> A (f x)
``````

I have tried using locally abstract types, but they are clearly insufficient, since the function that is passed in has no idea whether it’s going to be used within an `'a option` or just an `'a`.

``````let map (type a) (type b) (t : a gadt) ~f : b gadt =
match t with
| O x -> O (f x)
| A x -> A (f x)
``````

## Second question

I feel this question is a little more nuanced.

Let’s look at three minimal examples:

``````type 'a t
`````` this type-checks

``````type 'a t
`````` Error: In this definition, a type variable cannot be deduced from the type parameters.

``````type 'a t = 'a
`````` this type-checks

What gives?

Hello, I’m not that knowledgeable about GADTs myself but for the second point,
this might help :

https://sympa.inria.fr/sympa/arc/caml-list/2013-10/msg00189.html

For your first function, Let’s assume the input `t` is of type `a gadt`. and consider the possible type of `f`.

• If `t = A x`, then `f : a -> b`.
• If `t = O x`, then `a = x option` and `f : x -> y` for some `y`.

There is no general type that can encompass these two cases. Since there is no type that can type this function, you can’t write it.

Yes, you can only write

``````let map : type a b. a gadt -> (a -> b) -> b gadt = fun m f ->
match m with
| O v -> let x = f (Some v) in A x
| A v -> A (f v)
``````

or

``````let map : type a b. a gadt -> (a -> b) -> b option gadt = fun m f ->
match m with
| O v -> let x = f (Some v) in O x
| A v -> A (Some (f v)) (* or O (f v)*)``````

Hello Richard,

Considering the behavior you described, it sounds like there’s a problem with the GADT definition. It looks like this is what you want:

``````type _ gadt =
| A: 'a -> 'a gadt
| O: 'a option -> 'a gadt

let map: type a. f:(a -> 'b) -> a gadt -> 'b gadt = (
fun ~f ->
function
| A x -> A (f x)
| O (Some x) -> O (Some (f x))
| O None -> O None
)
``````

As others have pointed out, the syntax for functions expecting a GADT is a bit different. To be honest, you don’t need GADTs to write this code. But if the point is learning syntax, then that’s it.

A final point: you want to define a non labeled argument as your last in function declarations. In the end, the caller will pick the order.