# Two questions about GADTs

**URL:** <https://discuss.ocaml.org/t/two-questions-about-gadts/3342>\
**Category:** Learning\
**Tags:** gadt\
**Created:** [February 13, 2019, 12:11am UTC](https://discuss.ocaml.org/t/two-questions-about-gadts/3342 "2019-02-13T00:11:20Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![rdavison](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/rdavison/32/4321_2.png) [@rdavison](https://discuss.ocaml.org/u/rdavison)\
**Post date:** [February 13, 2019, 12:11am UTC](https://discuss.ocaml.org/t/two-questions-about-gadts/3342/1 "2019-02-13T00:11:20Z")

</div>

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:

```ocaml
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:

```ocaml
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`.

```ocaml
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:

```ocaml
type 'a t
type _ gadt = T : unit -> 'a t gadt

```

✅ this type-checks

```ocaml
type 'a t
type _ gadt = T : 'a -> 'a t gadt

```

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

```ocaml
type 'a t = 'a
type _ gadt = T : 'a -> 'a t gadt

```

✅ this type-checks

What gives?

---

<div class="post-metadata">

**Author:** ![bnguyenvanyen](https://avatars.discourse-cdn.com/v4/letter/b/7ea924/32.png) [@bnguyenvanyen](https://discuss.ocaml.org/u/bnguyenvanyen)\
**Post date:** [February 13, 2019, 9:30am UTC](https://discuss.ocaml.org/t/two-questions-about-gadts/3342/2 "2019-02-13T09:30:12Z")

</div>

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](https://sympa.inria.fr/sympa/arc/caml-list/2013-10/msg00189.html)

(also this [https://caml.inria.fr/mantis/view.php?id=5985&nbn=49](https://caml.inria.fr/mantis/view.php?id=5985&nbn=49))

---

<div class="post-metadata">

**Author:** ![Drup](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/drup/32/35_2.png) [@Drup](https://discuss.ocaml.org/u/Drup)\
**Post date:** [February 13, 2019, 10:05am UTC](https://discuss.ocaml.org/t/two-questions-about-gadts/3342/3 "2019-02-13T10:05:39Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![Freyr666](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/freyr666/32/591_2.png) [@Freyr666](https://discuss.ocaml.org/u/Freyr666)\
**Post date:** [February 13, 2019, 10:15am UTC](https://discuss.ocaml.org/t/two-questions-about-gadts/3342/4 "2019-02-13T10:15:12Z")

</div>

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)*)
```

---

<div class="post-metadata">

**Author:** ![gersonmoraes](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/gersonmoraes/32/485_2.png) [@gersonmoraes](https://discuss.ocaml.org/u/gersonmoraes)\
**Post date:** [February 13, 2019, 11:23am UTC](https://discuss.ocaml.org/t/two-questions-about-gadts/3342/5 "2019-02-13T11:23:40Z")

</div>

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:

```auto
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.