[Caml-list] Signature substitution deleting an exposed type alias

[Caml-list] Signature substitution deleting an exposed type alias

[Mathieu Barbin]

[-- Attachment #1: Type: text/plain, Size: 1947 bytes --]

Dear list,

I apologize in advance as I believe this has been discussed already in some
very close forms, such as in the thread "Narrowing a signature with a
constrained type" or a few other threads too.  The other examples I've
found in the archives I thought were maybe slightly more involving
(containing either some type variable, type paramters, an object type, or
type variable constraints, etc.).  So in the hope that what I am trying to
do might be simpler, here goes:

$ cat > /tmp/a.ml
module type A = sig
  type t = int
  val of_int : int -> t
end

module type B = sig
  type t
  include A with type t := t
end

$ ocamlopt /tmp/a.ml
File "/tmp/a.ml", line 8, characters 10-28:
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 t = t
       is not included in
         type t = int
       File "/tmp/a.ml", line 2, characters 7-14: Expected declaration
       File "/tmp/a.ml", line 8, characters 17-28: Actual declaration
EXIT STATUS 2

$ ocamlopt -version
4.00.1

In a previous answer from Jacques Garrigue I read that

> to ensure the coherence of the with constraints, we require that
> the new signature be a subtype of the original one (as a module, not as
an object).
> This is where your code gets rejected.

In the example, I am not sure what exactly are the signatures involved in
the comparison, since the included signature does not contain the
definition of the type t ( removed by the use of := ), and without the type
[t] the signature are virtually identical.

I've used the following workaround [1], however I was just wondering what
was the reason behind the rejection.

Thanks,
Mathieu.

[1]
module type S = sig
  type t
  val of_int : int -> t
end

module type A = sig
  type t = int
  include S with type t := t
end

module type B = sig
  type t
  include S with type t := t
end

[-- Attachment #2: Type: text/html, Size: 2873 bytes --]

Re: [Caml-list] Signature substitution deleting an exposed type alias

[Leo White]

[-- Attachment #1: Type: text/plain, Size: 1048 bytes --]


> module type A = sig type t = int val of_int : int -> t end
>
> module type B = sig type t include A with type t := t end
>
> [...]
>
> In the example, I am not sure what exactly are the signatures involved
> in the comparison, since the included signature does not contain the
> definition of the type t ( removed by the use of := ), and without the
> type [t] the signature are virtually identical.

The two signatures being compared are the signatures before the
definition of t is removed, so essentially:

sig type t = int val of_int : int -> t end

is being compared with:

sig type t = t' val of_int : int -> t end

where t' refers to the type defined by the `type t` definition in the B
signature.

This prevents inconsistent signatures being created. For example,

type t = T of int

module type C = sig type s = int type r = t = T of s end

module type D = C with type s := float

would result in:

module type D = sig type r = t = T of float end

which is inconsistent, since the definition does not match the equation.

Regards,

Leo

[-- Attachment #2: Type: text/html, Size: 2305 bytes --]

Re: [Caml-list] Signature substitution deleting an exposed type alias

[Mathieu Barbin]

[-- Attachment #1: Type: text/plain, Size: 1376 bytes --]

Dear Leo, Thank you for the explanation and the illustrating example.


On Mon, Mar 9, 2015 at 4:50 AM, Leo White <leo@lpw25.net> wrote:

>  > module type A = sig
> >   type t = int
> >   val of_int : int -> t
> > end
> >
> > module type B = sig
> >   type t
> >   include A with type t := t
> > end
> >
> > [...]
> >
> > In the example, I am not sure what exactly are the signatures involved
> in the comparison, since the included signature
> > does not contain the definition of the type t ( removed by the use of :=
> ), and without the type [t] the signature are
> > virtually identical.
>
> The two signatures being compared are the signatures before the
> definition of t is removed, so essentially:
>
>     sig
>       type t = int
>       val of_int : int -> t
>     end
>
> is being compared with:
>
>     sig
>       type t = t'
>       val of_int : int -> t
>     end
>
> where t' refers to the type defined by the `type t` definition in the B
> signature.
>
> This prevents inconsistent signatures being created. For example,
>
>     type t = T of int
>
>     module type C = sig
>       type s = int
>       type r = t = T of s
>     end
>
>     module type D = C with type s := float
>
> would result in:
>
>     module type D = sig type r = t = T of float end
>
> which is inconsistent, since the definition does not match the equation.
>
> Regards,
>
> Leo
>

[-- Attachment #2: Type: text/html, Size: 2697 bytes --]