# Typing puzzle: type constructor arity abstraction (for Seqes)
**URL:** https://discuss.ocaml.org/t/typing-puzzle-type-constructor-arity-abstraction-for-seqes/10948
**Category:** Learning
**Tags:** types
**Created:** [December 12, 2022, 2:54pm UTC](https://discuss.ocaml.org/t/typing-puzzle-type-constructor-arity-abstraction-for-seqes/10948 "2022-12-12T14:54:26Z")
**Posts on this page:** 4
**Page:** 1
### Author:  [@raphael-proust](https://discuss.ocaml.org/u/raphael-proust)
#### Post date: [December 12, 2022, 2:54pm UTC](https://discuss.ocaml.org/t/typing-puzzle-type-constructor-arity-abstraction-for-seqes/10948/1 "2022-12-12T14:54:26Z")
The [recently released `Seqes` library](https://discuss.ocaml.org/t/ann-release-of-seqes-version-0-1/10947) 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:
```ocaml
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:
```ocaml
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:
```ocaml
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?
---
### Author:  [@art-w](https://discuss.ocaml.org/u/art-w)
#### Post date: [December 12, 2022, 7:01pm UTC](https://discuss.ocaml.org/t/typing-puzzle-type-constructor-arity-abstraction-for-seqes/10948/2 "2022-12-12T19:01:00Z")
> [@raphael-proust](#):
>
> Of course once can pass a two-parameter monad as a one-parameter monad. The two-parameter functor will accept the following monad:
>
> ```auto
> type ('a, 'e) t = 'a Lwt.t
> let return = Lwt.return
> let bind = Lwt.bind
>
> ```
>
> But this returns a two-parameter Seq-like type.
The following trick can work to erase a type parameter:
```auto
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:
```ocaml
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:
```ocaml
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
```
---
### Author:  [@raphael-proust](https://discuss.ocaml.org/u/raphael-proust)
#### Post date: [December 13, 2022, 12:25pm UTC](https://discuss.ocaml.org/t/typing-puzzle-type-constructor-arity-abstraction-for-seqes/10948/3 "2022-12-13T12:25:18Z")
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
> [@art-w](#):
>
> ```auto
> 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
>
> ```
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:
```ocaml
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
```ocaml
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.
---
### Author:  [@art-w](https://discuss.ocaml.org/u/art-w)
#### Post date: [December 14, 2022, 11:17am UTC](https://discuss.ocaml.org/t/typing-puzzle-type-constructor-arity-abstraction-for-seqes/10948/4 "2022-12-14T11:17:04Z")
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:
```ocaml
and 'a node = [`Nil | `Cons of 'a * 'a t]
```
(We sadly can’t do:
```ocaml
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)