[Caml-list] substituting recursive types inside a signature

[Caml-list] substituting recursive types inside a signature

[Ashish Agarwal]

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

$ cat foo.ml
module M = struct
  type t = A | B of u
  and u = C of t
end

module type N = sig
  include module type of M
    with type t = M.t
    and type u = M.u
end

$ ocamlc -c foo.ml
File "foo.ml", line 8, characters 9-21:
Error: This variant or record definition does not match that of type M.t
       The types for field B are not equal.

I guess the "and" in the constraint doesn't make the constraints mutually
recursive, so what does it do?

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

Re: [Caml-list] substituting recursive types inside a signature

[Jacques Garrigue]

On 2015/11/03 05:01, Ashish Agarwal wrote:
> 
> $ cat foo.ml
> module M = struct
>   type t = A | B of u
>   and u = C of t
> end
> 
> module type N = sig
>   include module type of M
>     with type t = M.t
>     and type u = M.u
> end
> 
> $ ocamlc -c foo.ml
> File "foo.ml", line 8, characters 9-21:
> Error: This variant or record definition does not match that of type M.t
>        The types for field B are not equal.
> 
> I guess the "and" in the constraint doesn't make the constraints mutually recursive, so what does it do?

with constraints are handled incrementally. I.e., the code you wrote is exactly equivalent to:

   include (((module type of M) with type t = M.t) with type u = M.u)

It has always been that way. An interesting question is whether we could actually delay the checking to
after applying all the constraints. This would be a non-trivial change.

Jacques Garrigue

Re: [Caml-list] substituting recursive types inside a signature

[Ashish Agarwal]

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

On Wed, Nov 4, 2015 at 9:10 PM, Jacques Garrigue <
garrigue@math.nagoya-u.ac.jp> wrote:

the code you wrote is exactly equivalent to:
>
>    include (((module type of M) with type t = M.t) with type u = M.u)
>

And the parentheses here don't matter right, so this is the same as:

include module type of M
    with type t = M.t
    with type u = M.u

So then why do we have the "and" syntax at all?

Well, I can use manifest types to work around this, at the expense of some
manual typing. Here's what works:

$ cat foo.ml
module M = struct
  type t = A | B of u
  and u = C of t
end

module N : sig
  type t = M.t = A | B of u
  and u = M.u = C of t
  val f : t -> t
end = struct
  type t = M.t = A | B of u
  and u = M.u = C of t
  let f x = x
end

let x : M.t = M.A
let _ = N.f x

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

Re: [Caml-list] substituting recursive types inside a signature

[Ashish Agarwal]

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

I pasted the wrong code. Slightly less typing is possible by doing "include
M" in N's implementation.

On Wed, Nov 4, 2015 at 10:22 PM, Ashish Agarwal <agarwal1975@gmail.com>
wrote:

> On Wed, Nov 4, 2015 at 9:10 PM, Jacques Garrigue <
> garrigue@math.nagoya-u.ac.jp> wrote:
>
> the code you wrote is exactly equivalent to:
>>
>>    include (((module type of M) with type t = M.t) with type u = M.u)
>>
>
> And the parentheses here don't matter right, so this is the same as:
>
> include module type of M
>     with type t = M.t
>     with type u = M.u
>
> So then why do we have the "and" syntax at all?
>
> Well, I can use manifest types to work around this, at the expense of some
> manual typing. Here's what works:
>
> $ cat foo.ml
> module M = struct
>   type t = A | B of u
>   and u = C of t
> end
>
> module N : sig
>   type t = M.t = A | B of u
>   and u = M.u = C of t
>   val f : t -> t
> end = struct
>   type t = M.t = A | B of u
>   and u = M.u = C of t
>   let f x = x
> end
>
> let x : M.t = M.A
> let _ = N.f x
>
>

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