 # Filtering constructors by type variable (GADTs + polymorphic variants)

The following problems arise in the context of a patch for adding support for bigarrays to the ocamlmpi library. I don’t know how to solve the third problem. I have a vague intuition that it is not possible, but I would love to be proved wrong or to really understand why it cannot be done.

You are given a list of operations (e.g., Maximum and Logical-And). All of them apply to integer values but only some of them (e.g., Maximum) apply to floating-point values.

Constraint 1: The operations must be modeled by a single variant type.

Problem 1 (easy): give the signature of a function from an int and any operation to an int.

Problem 2 (harder): give the signature of a function from a float and a floating-point-only operation to a float.

Problem 3 (unknown): give the signature of a function from a list of int, char, or float and an operation to unit. When the list contains floats, only floating-point operations are allowed.

Here is my attempt. It solves problems 1 and 2 but fails to solve problem 3.

``````type _ op =
| Max  : [< `Int of int | `Char of char | `Float of float ] op
| Land : [< `Int of int | `Char of char ] op

module type S = sig
val reduce_int: int -> [`Int of int ] op -> int
val reduce_float: float -> [`Float of float] op -> float
val reduce_list: 'a list -> [< `Int of 'a | `Char of 'a | `Float of 'a ] op -> unit
end

module A : S = struct
let reduce_int x op = x
let reduce_float x op = x
let reduce_list s op = ()
end

let _ = A.reduce_int 0 Max       (* OK *)
let _ = A.reduce_int 0 Land      (* OK *)
let _ = A.reduce_float 0. Max    (* OK *)
let _ = A.reduce_float 0. Land   (* OK: REJECTED *)

let _ = A.reduce_list  Max    (* OK *)
let _ = A.reduce_list  Land   (* OK *)
let _ = A.reduce_list [0.] Max   (* OK *)
let _ = A.reduce_list [0.] Land  (* KO: NOT REJECTED! *)
``````

The problem can be solved using module types if constraint 1 is dropped, but this solution seems more bureaucratic than elegant.

Anyone have a better idea?

Tim.

1 Like

A function of the type of `reduce_list` cannot be meaningfully implemented since the behavior of its implementation is depending on the type of the type variable `'a`.

Your interface feels quite complex, but it may be implementable by adding a GADT witness for the type of the argument:

``````type int_like = Int_like
type float_like = Float_like

type ('inp,'out,'req) ty =
| Char: (char, char, int_like) ty
| Int: (int, int, int_like) ty
| Float: (float, float, float_like) ty
| List: ('a,'out,'b)  ty -> ('a list, unit,'b) ty

type _ op =
| Max  : 'any op
| Land : int_like op

module type S = sig
val reduce: ('i,'o,'op) ty -> 'i -> 'op op -> 'o
end

module A : S = struct
let reduce (type i o r) (w: (i,o,r) ty) (x:i) (op:r op): o = match w with
| Int -> x
| Float -> x
| Char -> x
| List _ -> ()
end

let _ = A.reduce Int 0 Max       (* OK *)
let _ = A.reduce Int 0 Land      (* OK *)
let _ = A.reduce Float 0. Max    (* OK *)
let _ = A.reduce Float 0. Land   (* OK: REJECTED *)

let _ = A.reduce (List Int)  Max    (* OK *)
let _ = A.reduce (List Int)  Land   (* OK *)
let _ = A.reduce (List Float) [0.] Max   (* OK *)
let _ = A.reduce (List Float) [0.] Land (* Rejected *)
``````

The reduce function can be specialized by hand for the non-list case if required.

3 Likes

Passing a GADT witness like that is a clever idea that I hadn’t thought of. Thank you. Here is an adaptation to the bigarrays of the original problem.

``````type int_like = Int_like
type float_like = Float_like

type ('a, 'req) ty =
| Char: (char, int_like) ty
| Int: (int, int_like) ty
| Float: (float, float_like) ty

type _ op =
| Max  : 'any op
| Land : int_like op

module type S = sig
val reduce_bigarray:
('a, 'req) ty
-> ('a, 'b, 'c) Bigarray.Genarray.t
-> 'req op
-> unit
end

module A : S = struct
let reduce_bigarray ty a op = ()
end

let ba1 = Bigarray.(Genarray.create Char C_layout [| 1 |])
let ba2 = Bigarray.(Genarray.create Float64 C_layout [| 1 |])

let _ = A.reduce_bigarray Char ba1 Max   (* OK *)
let _ = A.reduce_bigarray Char ba1 Land  (* OK *)
let _ = A.reduce_bigarray Float ba2 Max  (* OK *)
let _ = A.reduce_bigarray Float ba2 Land (* Rejected *)
``````

(Unlike for lists, a meaningful implementation with bigarrays is possible essentially because the underlying type can be recovered with `Bigarray.Genarray.kind`.)

If I understand things correctly, rather than filtering the allowed operations based on the instantiation of a type variable (`'a`), the relevant types of the function are fixed by the witness argument.

Is there a way to do the filtering directly, i.e., without having to pass an extra argument?

In your bigarray case, the GADT argument provides the `int_like` classification for types. This classification needs to be written down at some point and the `reduce` function needs to have access to this classification.

This is quite similar to the kind of bigarray which maps C types to OCaml types. In fact, if changing the interface of Bigarrays was an option, this information could be integrated directly into the kind.

Yes, I see. The GADT provides a table mapping base types to the classification used for operations, but the typing algorithm cannot infer which row is required for a given base type, so it must be specified explicitly.

Besides the compatibility issues, it seems to me that the bigarray interface is already complicated enough without adding a fourth type argument.

Never mind. We can make do with a dynamic check in this case.

Thank you for helping. Your example is a really nice way to better understand GADTs.

An alternative solution could be to make `Land` carry the witness that the type variable is `int_like`.

``````type _ int_like =
| Char: char int_like
| Int: int int_like

type _ op =
| Max: _ op
| Land: 'a int_like -> 'a op

val reduce_bigarray: ('a, _, _) Bigarray.Genarray.t -> 'a op -> unit
``````

This solution allows `reduce_bigarray` to be called with `Max`, `Land Char` and `Land Int` (it is worth noticing that this solution is quite close to the “heavy-handed” solution that @tbrk suggested initially, with constructors such as `Char_land` and `Char_int`, but instead of having `n`×`m` constructors for `n` types and `m` operations, this solution needs only `n` constructors for `int_like` and `m` constructors for `op`).

I like this much better than the `Char/Int/Float_*` solution (not least because `int_like` becomes a simple predicate on the base type) even if it does still require the caller to make the type explicit. I also think its better than the “bureaucratic” solution based on modules.