Constraining a type in a module-type?

Learning
1

I’m trying to figure out how to constrain a type in a module-type, and having … some trouble figuring it out. I’m sure I’m just missing something …

  1. I’m starting with Map.S
  2. and then I want to constrain the type 'a t to be int t (more generally, to some type t2, but this is sufficient for the example)

And I cannot figure out how to express it to OCaml. The obvious thing

module type MT = (Map.S with type !+ 'a t = 'a t constraint 'a = int) ;;

doesn’t work:

Line 1, characters 47-48:
1 | module type MT = (Map.S with type !+ 'a t = 'a t constraint 'a = int) ;;
                                                   ^
Error: Unbound type constructor t

From what I understand, that’s not surprising: the r.h.s. of the mod-constraint isn’t supposed to mention members of the module-type (again, IIUC). I thought maybe I needed to declare a type with the right shape, and then constrain the module-type with that, viz.

module type MT = sig 
  type !+ 'a t
  include (Map.S with type !+ 'a t = 'a t constraint 'a  = int)
end ;;

but that didn’t work either:

Line 3, characters 11-62:
3 |   include (Map.S with type !+ 'a t = 'a t constraint 'a  = int)
               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: In this `with' constraint, the new definition of t
       does not match its original definition in the constrained signature:
       Type declarations do not match:
         type +'a t = 'a t constraint 'a = int
       is not included in
         type +!'a t
       Their parameters differ
       The type int is not equal to the type 'a
       File "map.mli", line 70, characters 4-15: Expected declaration

I know I can just copy the module-type (and that’s what I’ll do to make progress, but I figured I’d ask, in case there’s some clever nicety I’m missing.

Any advice would be appreciated.

1 Like
2

This works with old-enough versions of OCaml:

module type MT = Map.S with type 'a t = bool list

If you want MT to come with its own type 'a t, and use int t in the signature, you could do this as follows:

module type MT = sig
  type 'a t
  include (Map.S with type 'a t := int t)
end

However, neither of those are valid anymore since the Map.S signature contains the new ! thing that means that !+'a t must be injective in 'a. This gives strictly more information than back in the days when 'a t was just covariant, it allows the user to deduce 'a = 'b from 'a t = 'b t, and so refining 'a t to be int or some other constant independent of 'a is not valid anymore.

Injectivity annotations on Map were added in #9781 by @yallop. I don’t know if we realized at the time that it breaks the not-unheard-of pattern of specializing the signature of a polymorphic container into a monomorphic container.

(Note: if you see your process in terms of adding a constraint, rather than instantiating a type with a new definition, then intuitively this preserves injectivity, we are just taking a subset of valid instances. But the type-checker does not let you add constraints on types in signatures.)

3 Likes
3

Thank you for the explanation! I’m proceeding with just cloning the signature. As it turns out, for my purpose, I need to remove some of the members anyway, so it’s not exactly a loss. But good to understand these details. Again, thank you!

4

I stumbled upon this issue (specializing the signature of a polymorphic container into a monomorphic container) a few days ago, and got blocked by the injectivity annotation, as you mentioned.
Hence the question: do we really want destructive substitution (i.e., :=, as opposed to =) in signatures to check annotations on type parameter at all?

5

I must say I don’t fully understand what the design constraints are for with equalities. It looks like we currently try to ensure a sub-signature relation (S with ...) <: S, in the sense that if M : S with ... then M : S should hold. (This is typically the case when adding an equality on an abstract type: the converse direction corresponds to hiding more, which is always valid). But do we actually rely on this for soundness?

In the case of Map.S, however, I don’t know if it really makes sense to try to specialize it into a heterogeneous container. For example specializing 'a t into t0 in get : key -> 'a t -> 'a becomes get : key -> t0 -> 'a, which does not make much sense to me. (Some other signatures are such that this operation does make sense, they typically also have type-indexed keys.) Maybe when Chet mentioned constraint 'a = int he had in mind to get get : key -> t0 -> int in this case, which does make more sense and is what you would get if you could add constraints, instead of using a destructive substitution.

1 Like
6

It seems to me that destructive substitution does not satisfy the sub-signature constraint that you mention, since it removes a type component (if I understand correctly, the signature S has one more type component than the signature S with type t := ..., and thus S with type t := ... cannot be a sub-signature of S).
I agree with your argument, however, when a (non-destructive) type equality constraint is added (... with type t = ...).

And yes, in the case of containers, some value signatures (such as the one for get) need to be redefined. I am neither surprised nor bothered with that. In practice, only a few function signatures must be redefined.

I also agree that in the case of monomorphic instantiation of polymorphic containers, Chet’s approach using type 'a t = 'a t constraint 'a = int (should this work) would make more sense than the destructive substitution approach I proposed.

7

(I guess @garrigue could comment on the intended static discipline for destructive substitution.)