Support parameter constraints in module signature type equalities

[gasche]

Sometimes it is natural to consider two different interfaces for a data structure, one where the container type is parametrized, and one where it is monomorphic. I propose to let us instantiate the polymorphic signature into the monomorphic signature by using a type constraint to transform occurrences of the type parameter.

For example, if we have

module type Poly = sig
  type 'a t
  val return : 'a -> 'a t
  val map : ('a -> 'b) -> 'a t -> 'b t
end

then I propose to write

module type Mono = sig
  type elt
  type t
  include Poly with type 'a t := t constraint 'a = elt
end

and to have the type-checker understand this as the following signature:

module type Mono = sig
  type elt
  type t
  val return : elt -> t
  val map : (elt -> elt) -> t -> t
end

To apply the equation type 'a t = u constraint 'a = foo, for each occurrence of bar t in the signature, we unify foo with bar and apply the resulting substitution. We fail with an error if foo and bar are not unifiable, for example if we used int t in another item of the Poly signature above.

[gasche]

cc @garrigue : if this is unsound for a well-known reason, @garrigue would be aware of it.

[gasche]

Note: it is currently possible to derive both interfaces by introducing a signature that encapsulates the use of the type parameters.

module type Generic = sig
  type 'a t
  type 'a param
  val return : 'a param -> 'a t
  val map : ('a param -> 'b param) -> 'a t -> 'b t
end

module type Poly = Generic with type 'a param := 'a
module type Mono = sig
  type t
  type elt
  include Generic with type 'a t = t and type 'a param = elt
end

[garrigue]

That is an interesting proposal.
However, it requires an important amount of work to be implemented: basically, you need to both substitute the occurrences of t and unify its arguments. There is no code doing that in the type checker yet.
Since doing that also means that you have to re-check the coherence of all the types, I suppose that there is no soundness problem; it would have to be detected anyway.

If we want to do things like that, it probably means that we want a way to reason about types at a higher level, rather than just substitution and unification, that would be more amenable to this kinds of extra checks.

[goldfirere]

I think the original goal can be achieved today:

module type Poly = sig
  type 'a elt
  type 'a container constraint 'a = 'b elt
  val return : 'a -> 'a container
  val map : ('a -> 'b) -> 'a container -> 'b container
end

module type Mono = sig
  type elt
  type t
  include Poly with type 'a elt := elt and type 'a container = t
end

This gives the desired signature, but with container unfortunately still around, because we can't use destructive substitution with constrained types. But given this decent approximation of the original goal, I think it's probably not worth adding a new feature requiring re-type-checking a signature upon a substitution.

[gasche]

Wow, nice! For the record, here is an alternative way to do this which is less nice -- which I wanted to avoid.

module type Gen = sig
  type 'a elt
  type 'a t
  val return : 'a elt -> 'a t
  val map : ('a elt -> 'b elt) -> 'a t -> 'b t
end

module type Poly = Gen with type 'a elt := 'a

module type Mono = sig
  type elt
  type t
  include Gen with type 'a elt := elt and type 'a t := t
end

Between this and the approach proposed by @goldfirere above, I agree that people who really wants this have workarounds, and that the proposed new feature is not really worth the effort. Closing.