Hello everyone, I have been experimenting with OCaml GADTs and I have run into two brick walls, and I need help.
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
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)
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
type 'a t type _ gadt = T : 'a -> 'a t gadt
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