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 [0] Max    (* OK *)
let _ = A.reduce_list [0] 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) [0] Max    (* OK *)
let _ = A.reduce (List Int) [0] 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.