Two questions about GADTs

Learning
1

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
type _ gadt = T : unit -> 'a t gadt

:white_check_mark: this type-checks

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

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

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

:white_check_mark: this type-checks

What gives?

2

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

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

3

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.

4

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

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.