Adding a constraint in an existing type

Learning
1

Hello,

I’m trying to add a constraint in a functor in order to bind two modules together.

Let say I have a module signature like this:

module type EXPR = sig
  type 'a t
end

What I whould like is to declare a signature where two modules Expr1 and Expr2 would be linked together like this:

module Assoc
    (Expr1 : EXPR)
    (Expr2 : sig
      (* This is the type I want to declare *)
      type 'a constrained_t constraint 'a = 'b Expr1.t -> 'c

      include EXPR with type 'a t = 'a constrained_t
    end) =
struct end

But this cause an error in the compilation:

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 constrained_t constraint 'a = 'b Expr1.t -> 'c
       is not included in
         type 'a t
       Their parameters differ
       The type 'b Expr1.t -> 'c is not equal to the type 'a

I’m not sure to understand the message error because this sounds like to be exactly what the constraint keyword is suposed to solve! Is this something OCaml cannot handle or is this may to express it which does not works ?

Thanks !

2

One problem with adding constraints to types in signatures is that the new constraints might make the existing instantiations of the types invalid. For example, consider the following (invalid) code that adds a constraint to the type t:

module type s =
sig
  type 'a t
  val x : int t
end with type 'a t = 'a list constraint 'a = float

If adding the constraint were allowed then this’d be equivalent to the following (also invalid) code

module type s =
sig
  type 'a t = 'a list constraint 'a = float
  val x : int t
end

in which the instantiation of t in the type of x does not match the constraint on 'a.

2 Likes
3

Thanks ! This make sense.

This may be off-topic, but how do you keep a track of all thoses cases when you see an evolution request or a question like I did ? There is no such documentation in the language specification telling why a syntax can be rejected. Do you keep in mind all the possible situations or is this just so obvious that you do not think about it ?

4

It wasn’t obvious to me in this case (but I don’t use constraints very often). I constructed the justification using reasoning like the following:

Why would adding a constraint to a signature not be allowed?

Modifying a signature is only allowed if it is guaranteed that the resulting signature will be consistent. So perhaps adding a constraint could make the signature inconsistent.

How could adding a constraint make a signature inconsistent?

Constraints restrict the instantiation of type parameters. So perhaps the signature already uses the type parameter in a way that is not consistent with the constraint.

How might the signature use the type parameter in a way that is not consistent with the constraint?

[etc.]

It’s possible to reason about the OCaml language in this way because the design isn’t completely arbitrary: there are a few overarching principles (e.g. principality, abstraction/modularity, a uniform value representation) with which all language features have to be consistent.