Constraining type parameter to be polymorphic variant

Learning
1

I am writing a function that stores a key value pair asynchronously. The key is a string but the value is supplied as an async stream so that it can be streamed to the key-value store without loading the whole value into memory. I am making use of lwt for async and the result type to represent success/failure.

What I am struggling with is how to combine the error type of the input value stream with the error type that represents an error writing to the key-value store. I think this problem can be represented without the async twist, but I wanted to leave it in to show that the value cannot be resolved before calling this function.

Currently, what I have looks something like this:

val store:
  t -> (* client *)
  string -> (* key *)
  Bigstringaf.t Lwt_stream.t -> (* value to store. contents are streamed in asynchronously *)
  (unit, 'error) Lwt_result.t -> (* promise that indicates whether contents stream succeeded or failed *)
  (unit, [ `Contents_error of 'error | ClientError.t ]) Lwt_result.t (* ClientError.t is a polymorphic variant type *)

I was hoping to able to constrain the 'error type parameter to be a polymorphic variant so that I could do this:

val store:
  t -> (* client *)
  string -> (* key *)
  Bigstringaf.t Lwt_stream.t -> (* value to store. contents are streamed in asynchronously *)
  (unit, 'error) Lwt_result.t -> (* promise that indicates whether contents stream succeeded or failed *)
  (unit, [> 'error | ClientError.t ]) Lwt_result.t (* NOTE the `Contents_error variant is no longer needed *)

Is there a way to add the polymorphic variant constraint? If not, is there a better approach to combining variants?

If possible, I would like to avoid the “big ball of mud” error approach (often found in Rust) where every error that can occur in the program/library is added to one giant error variant. I don’t like this approach because it makes it hard to know which errors actually need to be handled after calling a function, which is, IMHO, the biggest advantage of the result type to begin with! But I am open to being convinced otherwise.

3 Likes
2

You mean like this: prometo/Yawaramin__Prometo.rei at ef7229d3cbfe9980e32feef8e882785b49a96434 · yawaramin/prometo · GitHub (ReasonML syntax but you should be able to convert it to OCaml)

2 Likes
3

The notation

val f: [< t ] -> unit

only works with type declaration, not type expressions. Constraining the type variable 'error to the polymorphic variant kind is thus not going to work. (In general, polymorphic variants do not implement set operations at the type-level).

However, in your case, you can rewrite your type as

val store : t -> string ->  Bigstringaf.t Lwt_stream.t -> 
  (unit,  'error ) Lwt_result.t -> 
  (unit,  [> ClientError.t ] as 'error ) Lwt_result.t

The interesting part is that the 'error type variable is shared between the input and the output, thus all errors in the input can appears in the output. Moreover, the output is constrained to positively contain a ClientError.t .

Note however that in order to use this function, you might need to use explicit coercion.
For instance, in this simplified example:

let with_random_error x =
  if Random.float 1. > 0. then `Random_failure else x
let ok = with_random_error `Ok
let known_error () : [ `Known_failure ] = `Known_failure
let error = with_random (known_error ())

fails with

Error: This expression has type [ Known_failure ] but an expression was expected of type [> Random_failure ]
The first variant type does not allow tag(s) `Random_failure

because the typechecker cannot add `Random_failure to the closed set of failures of known_failure. The solution here is an explicit cast:

let ok_too =
  with_random_error (known_error () :> [ `Random_failure | `Known_failure ])
4 Likes
4

Very cool! That did the trick. The fact that variant types don’t implement set operations is good to know and means I need to think about them differently.

I don’t mind adding a type coercion internal to the library, especially if it is the tradeoff necessary for error clarity. I’ll have to think about how to structure things so the coercion is not necessary at the API boundary, though.