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 …
- I’m starting with
- 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) ;;
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)
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.
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)
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.)
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!
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?
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
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.
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
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.
(I guess @garrigue could comment on the intended static discipline for destructive substitution.)