Require a type in a module type is a polymorphic variant

Learning
1

I have a function that looks like this:

type err = [ .... ]
val tx : t -> f:(unit -> ('a, ([> err ] as 'e)) result) -> ('a, 'e) result

And I would like to make a module type that can be used as a functor that could reasonably wrap different instantiations of this function, all with different err types. But I’m running into trouble expressing it because I can’t seem to define a module type where err is guaranteed to be a polymorphic variant.

Somethign liek this:

module type S = sig
  module Db : sig
    type err
    type t

    val tx :
      t -> f:(unit -> ('a, ([> err ] as 'e)) result) -> ('a, 'e) result
  end

Is this solvable?

1 Like
2

You may type:

module type S = sig
  module Db : sig
    type t

    val tx :
      t -> f:(unit -> ('a, ([>  ] as 'e)) result) -> ('a, 'e) result
  end
end
3

I would advise you to simply remove the constraint that err is of a kind polymorphic variant since it doesn’t provide any benefits:

module type S = sig
  module Db : sig
    type t
    val tx : t -> f:(unit -> ('a, 'e)) result) -> ('a, 'e) result
end
4

I’m a big user of polymorphic variants for in result monads. I know it has some limitations, and maybe this is one of them, but to me they have have a lot of benefits in terms of code readability.

5

My point is that such constraints do not belong to the module type (aka the specification). Polymorphic variants are certainly useful in implementations.

1 Like
6

Thank you @octachron . Another question I have: is there anyway to “disaggregate” a polymorphic variant? For example something like:

match foo with
| #bar as v -> ...
| rest -> ...

As a human I know that the type of rest is whatever foo is minus #bar.

1 Like
7

As far as I know that’s the best you can do unfortunately. Consequently, this makes it difficult to provide convenience functions and monads around the error handling machinery.

It’s probably the main thing I don’t like about using them for errors but I still do in practice because I like the explicitness of my type signatures.