Typing puzzle: type constructor arity abstraction (for Seqes)

The recently released Seqes library offers functors to mix the Stdlib.Seq abstraction with monads. The original impetus for development was the use of Lwt, result and Lwt+result monads in the octez code-base. The use of these monads in combination with Seq introduced a lot of boilerplate code, which Seqes aims to alleviate.

Code duplication in Seqes

The Lwt “monad” (something something exceptions can break one of the monadic law) has one parameter. Thus the functor allowing to define a Seq+Lwt module is:

module Make1
  (Mon: sig
    type 'a t
    val return : 'a -> 'a t
    val bind : 'a t -> ('a -> 'b t) -> 'b t
  end)
: S1
   with type 'a mon := 'a Mon.t
= struct

  (* code here *)

end

The Result monad has two parameters. Thus the functor for defining a Seq+Result module is:

module Make2
  (Mon: sig
    type ('a, 'e) t
    val return : 'a -> ('a, 'e) t
    val bind : ('a. 'e) t -> ('a -> ('b, 'e) t) -> ('b, 'e) t
  end)
: S2
   with type ('a, 'e) mon := ('a, 'e) Mon.t
= struct

  (* code here *)

end

Interestingly, there is no difference in the code of the two functor apart from type definition.

Technically, it’s worse than just that:

  • There is a (duplicated) functor for making traversors over the Stdlib.Seq.t.
  • There is a (duplicated) functor as presented above.
  • There is a (duplicated) functor inside the functor presented above formaking additional traversors.

But the observation is still valid: only the types differ, the control structures are 1-to-1 identical. The library is essentially fully duplicated: there’s a one-parameter version and two-parameter version.

Can I encode the arity of a type constructor in the type system and use that to deduplicate the code?

Of course once can pass a two-parameter monad as a one-parameter monad. The two-parameter functor will accept the following monad:

      type ('a, 'e) t = 'a Lwt.t
      let return = Lwt.return
      let bind = Lwt.bind

But this returns a two-parameter Seq-like type.

I notice that the kinded and higher_kinded libraries have a similar approach of duplicating the code for each arity of the type constructor. And I think that if there was a known trick it would be used in those libraries.

Anyone has examples? Ideas?
Alternatively, explanations as to why it’s not possible?

The following trick can work to erase a type parameter:

module type MONAD2 = sig
  type ('a, 'e) t
  val return : 'a -> ('a, 'e) t
  val bind : ('a, 'e) t -> ('a -> ('b, 'e) t) -> ('b, 'e) t
end

module type MONAD1 = sig
  type 'a t
  include MONAD2 with type ('a, _) t := 'a t
end

In other words, you might be able to define Make1 in terms of Make2 by only repeating the type definition:

module Make2 (M : MONAD2) (* : S2 *) = struct
  type ('a, 'e) t = unit -> (('a, 'e) node, 'e) M.t
  and ('a, 'e) node = Nil | Cons of 'a * ('a, 'e) t
  (* ... your code here ... *)
end

module type S1 = sig
  type 'a t
  include S2 with type ('a, _) t := 'a t
end

module Make1 (M : MONAD1) : S1 = struct
  type 'a t = unit -> 'a node M.t
  and 'a node = Nil | Cons of 'a * 'a t

  module Mon2 = struct type ('a, 'e) t = 'a M.t let return = M.return let bind = M.bind end
  include (Make2 (Mon2) : S2 with type ('a, _) t := 'a t)
end

(You’ll need to add similar constraints for 'a mon, 'a callermon etc on that last line, it may not be easy to convince the typechecker that the 'e parameter is erasable)


edit: You can even skip the repetition of the type 'a t if it’s not public:

module Make1_ (M : MONAD1) : S1
= struct
  module Mon2 = struct type ('a, 'e) t = 'a M.t let return = M.return let bind x f = M.bind x f end
  type 'a t = ('a, unit) Make2(Mon2).t
  include (Make2 (Mon2) : S2 with type ('a, _) t := 'a t)
end
1 Like

Thanks for the answer. I was able to apply it to part of the source. I have trouble pushing it through everywhere.

The main issue I’m struggling against is with this snippet

The type 'a t and the type generated by the Make2 module are distinct. That’s because the functor generates a new type altogether. I can circumvent this:

module type T2 = sig
  type ('a, 'e) mon
  type ('a, 'e) t = unit -> (('a, 'e) node, 'e) mon
  and ('a, 'e) node =
    | Nil
    | Cons of 'a * ('a, 'e) t
end
module Make2WithT2
  (Mon: Sigs2.MONAD2)
  (T: T2 with type ('a, 'e) mon := ('a, 'e) Mon.t)
: S2
   with type ('a, 'e) mon := ('a, 'e) Mon.t
   with module T = T (* carries type equalities for both t and node *)
= struct
  module T = T
  include T
  (* … the code here … *)
end
module Make2(Mon: Sigs2.MONAD2) = Make2WithT2(Mon)(struct (* … types here … *) end)

And then I try to use it to define Make1 based on Make2WithT2. But I can’t manage to make a one-parameter version of seq and pass it to Make2WithT2. Essentially I can’t make the one-parameter node into a two-parameter version. I’m trying to do something along the lines of

  module T1 = struct
    type 'a t = unit -> 'a node Mon.t
    and 'a node =
      | Nil
      | Cons of 'a * 'a t
  end
  module T2 = struct
    type ('a, 'e) t = ??
    and ('a, 'e) node = ??
  end

and I can’t find a way to express that in a way that the type checker accepts. I don’t know if there is an issue with the specific invocations I’ve tried (maybe there’s a cleverer way to twist the module system and type system arms), if there is a limitation in the expressivity of OCaml, or if there is a more fundamental limit that I’m hitting.


Still, I’ve used your recommendations to reduce the duplication and also to increase expressivity. I’ll release a 0.2 version in the not too distant future.

Oh right, yes the constructors are different and I don’t know how to force the typechecker here… It works better with polymorphic variants since unification is possible there:

  and 'a node = [ `Nil | `Cons of 'a * 'a t ]

(We sadly can’t do:

and 'a node = ('a, void) M2.node = Nil | Cons of ...
 (* ^^   and  ^^^^^^^^^^ must be strictly equal *)

And I can’t think of a way that doesn’t lead to a worse documentation/API)