Concatenating signatures: maybe I'm missing something?

Ecosystem
1

[I’m hacking with the modular implicits variant, though this question is more generic.]

I’m trying to figure out the idiom for a particular kind of concatenation of signatures, and having no luck. Does anybody know if there’s a trick for this? [other than, y’know, manually copying the relevant bits?]

Suppose I have a signature:

module type ZERO = sig
  type t
  val zero : unit -> t
end

and another one

module type SUBSCRIPTABLE = sig
  type item_t
  type t
  val sub : t -> int -> item_t
  val make : item_t -> item_t list -> t
end

I’d like to make one that is the “sum” of these two signatures, where Z:ZERO, S:SUBSCRIPTABLE, and Z.t = S.item_t. So I’d like the signature

module type ZERO_SUBSCRIPTABLE = sig
  type item_t
  type t
  val zero : unit -> item_t
  val sub : t -> int -> item_t
  val make : item_t -> item_t list -> t
end

Now why would I like this? Well, there are types that enjoy a zero value. And types that don’t. For types that enjoy a zero value, I might want to have the make that builds a vector automatically use that zero value to initialize the vector, where for types that don’t have a zero value, the caller would have to provide the initializer value.

More generally, in Rust, often in places where you can provide a type, you can provide a type that enjoys some collection of traits, and these are implicitly somewhat like what I describe above: the concatenation of signatures, with some renaming of types. And in some cases, the collection of traits that a type enjoys can be … significant, e.g.

    pub fn spmat_dot_densevec<T>(sp_mat : &CsMatI<T, u64>, v: &ArrayView<T, Dim<[usize; 1]>>) -> Array<T, Dim<[usize; 1]>>
    where
	T : Zero + Sum + Copy + MulAdd + MulAdd<Output = T> + Send + Sync,
    for<'r> &'r T: Mul<&'r T, Output = T>,

which says that the item-type T:

  1. has a zero value
  2. has an addition operation
  3. can be copied
  4. has a multiply-add operation
  5. that multiply-add operation produces the same type T
  6. and has some good multi-threading properties

Maybe this is just something that isn’t doable in OCaml, simply due to cumbersome syntax. That’d be OK – I just want to figure out the answer.

2

With destructive substitutions:

# module type ZERO_SUBSCRIPTABLE = sig
    include SUBSCRIPTABLE
    include ZERO with type t := item_t
  end ;;
module type ZERO_SUBSCRIPTABLE =
  sig
    type item_t
    type t
    val sub : t -> int -> item_t
    val make : item_t -> item_t list -> t
    val zero : unit -> item_t
  end
4 Likes
3

By the way, this phrasing might throw off the type theorists in here since what you’re asking for is a “product” in that parlance, i.e. the exact dual of a “sum”.

4

For sure, he was asking for a product type (it’s a bit strange that Rust chose a sum to express a conjunction of constraints: A and (B or C) = (A and B) or (A and C), i.e a conjunction works like a product and a disjunction like a sum).

By the way, another solution to this problem (similar to the way inheritance is done in the examples section of the modular implicit paper) is to not flatten the product of these multiple interfaces:

module type Zero_subscriptable = sig
  type t
  type item
  module Zero : Zero with type t = item
  module Sub : Subscriptable with type t = t and type item = item
end
1 Like
5

Thank you for the advice, it worked and I’m moving along. And you’re right, that what I wanted was a product-type. Been a long time since I thought in type theory terms, and most of that knowledge has been pushed out to tape archive, so the space can be taken up by other knowledge.