Polymorphic function and GADT : can the output stem from another constructor than the input?

Learning
1

Hi everyone,

I’ve started making use of GADT in my code and I’ve been loving the elegance of it so far. I understand that a typical use case of GADTs is when you’ve got a parameterized type 'a t and want the output type of a function to depend on parameter 'a, while providing different implementations for different values of 'a using polymorphism.
I had no problem building functions whose signatures looked like type a. a t -> a, but now I’d like to do something a little different. My GADT _ t has several constructors :

type x
type y
type z

type _ t =
    | X : x -> x t
    | Y : y -> y t
    | Z : z -> z t

For some reasons, the function I’d like to write would return a y t when passed a x t as an argument, and would return a z t when passed a y t.

let f : type a. a t -> (* what should I write here ? *) = function
| X _ as x -> y_of_x x (* output of type y t *)
| Y _ as y -> z_of_y y (* output of type z t *)
| Z _      -> raise InvalidArgument

Having such a function seems doable in theory (static typability could be achieved just by examining the constructors), but I can’t get to express its type right. OCaml seems to only allow the output type to depend on the local type that is provided by the input GADT parameter.
Does OCaml provide a proper way to achieve this or is it not currently possible ?

I’ve found a clumsy workaround using polymorphic variants, but I dislike the facts that they require the variables to be matched upon to know of which type they actually are, which is not necessary in my case : if var is of type x t, the compiler can be sure that f var is of type y t.

Thanks in advance for your answers or advices

2

I don’t think that can be directly expressed as foo t -> bar t. You can get close by defining an auxiliary type

type (_,_) rel = 
| Xr : (x,y) rel
| Zr : (y,z) rel

then define f : type a b. a t -> (a,b) rel -> b t (assuming the compiler is capable of telling x and y apart, ie it won’t work when they’re abstract types as ocaml will think X and Zr can be passed together to your function).

2 Likes
3

You can encode any finite automaton at the type level with GADT, you just need to add the explicit transition in the type:

type x = X_flag
type y = Y_flag

type _ t =
  | X : x -> x_state t
  | Y : y -> y_state t
and x_state = <state:x; next:y_state>
and y_state = <state:y; next:x_state>

let next (type a b) (x: <state: a; next:b> t) : b t = match x with
| X X_flag -> Y Y_flag
| Y Y_flag -> X X_flag

(Note that here object types are only used as a kind of record at the type level, there are no concrete objects involved)

2 Likes
4

@octachron’s solution is very nice, but there is an alternative (I would say dual) solution:

The only problem, that I see with the @octachon’s solution is that it gives to much power to the interface user, if x and y constructors are exposed. It could be addressed by abstracting them, as well as the representation of the state transition witness, and posting in the interface the set of valid state transitions.

5

Thanks a lot @octachron for your very elegant solution ! It did the trick