[Caml-list] Deleting a type alias while including a module

[Caml-list] Deleting a type alias while including a module

[Michael Grünewald]

Dear list,

I am trying to use destructive substitution to remove a type alias in an 
inclusion. Some module XArray has the following signature:

XArray: sig
  type 'a xarray
  type 'a t
end

and I would like to remove the 'a t in the resulting signature. I thought

include (XArray : module type of XArray
   with 'a t := 'a XArray.xarray
)

would do, but it would not:

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 XArray.xarray
        is not included in
          type 'a t = 'a xarray

Honestly, I do not really understand why the substitution can not 
happen, despite my careful reading of the documentation.  Any 
suggestions are welcome!
-- 
Michael

Re: [Caml-list] Deleting a type alias while including a module

[Michael Grünewald]

As a complement to my previous message, here is a minimal (well, short!) 
example displaying the behavior I cannot go around:

----8<--- example starts here ----
module type XARRAY =
sig
   type 'a xarray
   type 'a t = 'a xarray
end

module XArray : XARRAY =
struct
   type 'a xarray = 'a
   type 'a t = 'a xarray
end

module UseXArray =
struct
   include (XArray : XARRAY with type 'a t := 'a XArray.xarray )
end
----8<---- example ends here ----
Trying to compile this file yields the following error:

File "include_substitute.ml", line 15, characters 20-61:
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 XArray.xarray
        is not included in
          type 'a t = 'a xarray

(OCaml 3.12.1 on FreeBSD/amd64)

Re: [Caml-list] Deleting a type alias while including a module

[Gabriel Scherer]

Here is how I understand the situation:

> module type XARRAY =
> sig
>  type 'a xarray
>  type 'a t = 'a xarray
> end

> (XArray : XARRAY with type 'a t := 'a XArray.xarray )

>       Type declarations do not match:
>         type 'a t = 'a XArray.xarray
>       is not included in
>         type 'a t = 'a xarray

When you seal a module with a signature that has an abstract type (the
type ('a xarray) in the XARRAY signature), you get a "fresh" abstract
type is a result. The typer is here giving the following complain:
- you told me in the XARRAY signature that ('a t) would always be
equal to ('a xarray)
- in this example you also ask for ('a t) to be equal with 'a
XArray.xarray, the type of the previously defined module
- but by definition the ('a xarray) type of the current sealing is a
fresh abstract type, thus different of all previous types

If you want to equate ('a t = something) while still respecting the
(type 'a t = 'a xarray) signature contract, you have to first make ('a
xarray) a defined type rather than abstract type:

  # module Test = (XArray : XARRAY with type 'a xarray = 'a XArray.xarray);;
  module Test : sig type 'a xarray = 'a XArray.xarray type 'a t = 'a xarray end

Then you can substitute 'a t without breaking the weakened interface contract:

  # module Test = (XArray : XARRAY with type 'a xarray = 'a
XArray.xarray and type 'a t := 'a XArray.xarray);;
  module Test : sig type 'a xarray = 'a XArray.xarray end

If you wish to get an abstract type again, you can seal it after the
fact, but this requires to know the whole result type signature (here
it's only (sig type 'a xarray end)):

# module Test : sig type 'a xarray end = (XArray : XARRAY with type 'a
xarray = 'a XArray.xarray and type 'a t := 'a XArray.xarray);;
module Test : sig type 'a xarray en


2011/11/24 Michael Grünewald <michaelgrunewald@yahoo.fr>:
> As a complement to my previous message, here is a minimal (well, short!)
> example displaying the behavior I cannot go around:
>
> ----8<--- example starts here ----
> module type XARRAY =
> sig
>  type 'a xarray
>  type 'a t = 'a xarray
> end
>
> module XArray : XARRAY =
> struct
>  type 'a xarray = 'a
>  type 'a t = 'a xarray
> end
>
> module UseXArray =
> struct
>  include (XArray : XARRAY with type 'a t := 'a XArray.xarray )
> end
> ----8<---- example ends here ----
> Trying to compile this file yields the following error:
>
> File "include_substitute.ml", line 15, characters 20-61:
> 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 XArray.xarray
>       is not included in
>         type 'a t = 'a xarray
>
> (OCaml 3.12.1 on FreeBSD/amd64)
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

Re: [Caml-list] Deleting a type alias while including a module

[Michael Grünewald]

Hello Gabriel,

thank you for your much useful answer!

Gabriel Scherer wrote:
> When you seal a module with a signature that has an abstract type (the
> type ('a xarray) in the XARRAY signature), you get a "fresh" abstract
> type is a result.
I think I did not analyse adequately the situation because I overlooked 
the fact you pinpoint here.  I thought I knew this, but I probably 
implicitly assumed that the result of `module type of XArray` (my 
original code used this)  was annotated with concrete type definitions.  
But it does not work like this, and it is not expected to do so!

As you might guess I am now trying out the new features of OCaml 3.11, 
and the `include module type of` mantra together with destructive 
substitution in signatures is makes the implementation of inheritance 
mechanisms for modules much easier.  Something else I am very excited 
about is first class modules!

Best Regards,
Michael