typing of recursive modules in 3.10.2

typing of recursive modules in 3.10.2

[Charles Hymans]

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

Hi,

I have encountered a behavior of the type checking of recursive modules
which is hard for me to understand.
Especially so, since the code used to compile with Ocaml 3.10.0 but does not
with 3.10.2. And, an almost similar piece of code compiles correctly.

I tried to extract the smallest piece of code that exhibits the problem, but
it's still quite long. Sorry.

Here is the code that does not type with 3.10.2:
=======================================

module type BSig =
sig
  type t
  val f: t -> unit
end

module type ASig = functor(B: BSig) ->
sig
  type t
  val g: B.t -> unit
end

module Make(C: BSig) =
struct
  type t = int
  let g _ = ()
end

module MakeA = (Make: ASig)

module rec A:
sig
  type t
  val g: B.t -> unit
end
= MakeA(B)

and B:
sig
  type t = int * A.t
  val f: t -> unit
end
=
struct
  type t = int * A.t

  let f x = A.g x   (* does not type *)
(*
  let f (a, b) = A.g (a, b)   (* types correctly *)
*)
end

=========================

Note that if function f is replaced by the commented version, then the type
checker succeeds. Even though, this code modification is only giving the
additional information that the argument of f is a pair.

It would be nice for both versions of the code to compile, because the
current behavior of the type checker seems to me not easily predictable.

Thank you in advance for your help,

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

RE: [Caml-list] typing of recursive modules in 3.10.2

[Josh Berdine]

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

Hi Charles,

I don't know if it helps, and this doesn't address your concern over predictability, but your example will also typecheck if you annotate the argument of f with t:

let f (x : t) = A.g x

I can't claim to be able to explain just why that helps, but without the annotation it seems that when typechecking structure B, the typechecker needs to know the type equality t = B.t directly, while either adding the annotation or destructing the pair causes the type definitions to be unfolded once.

The following threads seem to be related:
http://caml.inria.fr/pub/ml-archives/caml-list/2007/05/d9414d45a9a6f30f2609e08c43f011a0.en.html
http://caml.inria.fr/pub/ml-archives/caml-list/2007/06/0d23465b5b04f72fedecdd3bbf2c9d72.en.html

There is also a related bug (4266) in the database.

Cheers,  Josh


From: caml-list-bounces@yquem.inria.fr [mailto:caml-list-bounces@yquem.inria.fr] On Behalf Of Charles Hymans
Sent: Tuesday, June 10, 2008 8:27 PM
To: caml-list@yquem.inria.fr
Subject: [Caml-list] typing of recursive modules in 3.10.2

Hi,

I have encountered a behavior of the type checking of recursive modules which is hard for me to understand.
Especially so, since the code used to compile with Ocaml 3.10.0 but does not with 3.10.2.<http://3.10.2.> And, an almost similar piece of code compiles correctly.

I tried to extract the smallest piece of code that exhibits the problem, but it's still quite long. Sorry.

Here is the code that does not type with 3.10.2:
=======================================

module type BSig =
sig
  type t
  val f: t -> unit
end

module type ASig = functor(B: BSig) ->
sig
  type t
  val g: B.t -> unit
end

module Make(C: BSig) =
struct
  type t = int
  let g _ = ()
end

module MakeA = (Make: ASig)

module rec A:
sig
  type t
  val g: B.t -> unit
end
= MakeA(B)

and B:
sig
  type t = int * A.t
  val f: t -> unit
end
=
struct
  type t = int * A.t

  let f x = A.g x   (* does not type *)
(*
  let f (a, b) = A.g (a, b)   (* types correctly *)
*)
end

=========================

Note that if function f is replaced by the commented version, then the type checker succeeds. Even though, this code modification is only giving the additional information that the argument of f is a pair.

It would be nice for both versions of the code to compile, because the current behavior of the type checker seems to me not easily predictable.

Thank you in advance for your help,


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

Re: [Caml-list] typing of recursive modules in 3.10.2

[Charles Hymans]

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

Thanks for the answer and links, Josh.
I had also noticed that annotating the argument with type t solved the
problem.

However the current behavior of the type-checker is really awkward to me. I
hope it is improved in the future to make the use of recursive modules more
intuitive and less of a black art.

Best regards,


On Wed, Jun 11, 2008 at 11:25 AM, Josh Berdine <jjb@microsoft.com> wrote:

>  Hi Charles,
>
>
>
> I don't know if it helps, and this doesn't address your concern over
> predictability, but your example will also typecheck if you annotate the
> argument of f with t:
>
>
>
> let f (x : t) = A.g x
>
>
>
> I can't claim to be able to explain just why that helps, but without the
> annotation it seems that when typechecking structure B, the typechecker
> needs to know the type equality t = B.t directly, while either adding the
> annotation or destructing the pair causes the type definitions to be
> unfolded once.
>
>
>
> The following threads seem to be related:
>
>
> http://caml.inria.fr/pub/ml-archives/caml-list/2007/05/d9414d45a9a6f30f2609e08c43f011a0.en.html
>
>
> http://caml.inria.fr/pub/ml-archives/caml-list/2007/06/0d23465b5b04f72fedecdd3bbf2c9d72.en.html
>
>
>
> There is also a related bug (4266) in the database.
>
>
>
> Cheers,  Josh
>
>
>
>
>
> *From:* caml-list-bounces@yquem.inria.fr [mailto:
> caml-list-bounces@yquem.inria.fr] *On Behalf Of *Charles Hymans
> *Sent:* Tuesday, June 10, 2008 8:27 PM
> *To:* caml-list@yquem.inria.fr
> *Subject:* [Caml-list] typing of recursive modules in 3.10.2
>
>
>
> Hi,
>
>
>
> I have encountered a behavior of the type checking of recursive modules
> which is hard for me to understand.
>
> Especially so, since the code used to compile with Ocaml 3.10.0 but does
> not with 3.10.2. And, an almost similar piece of code compiles correctly.
>
>
>
> I tried to extract the smallest piece of code that exhibits the problem,
> but it's still quite long. Sorry.
>
>
>
> Here is the code that does not type with 3.10.2:
>
> =======================================
>
>
>
> module type BSig =
> sig
>   type t
>   val f: t -> unit
> end
>
> module type ASig = functor(B: BSig) ->
> sig
>   type t
>   val g: B.t -> unit
> end
>
> module Make(C: BSig) =
> struct
>   type t = int
>   let g _ = ()
> end
>
> module MakeA = (Make: ASig)
>
> module rec A:
> sig
>   type t
>   val g: B.t -> unit
> end
> = MakeA(B)
>
> and B:
> sig
>   type t = int * A.t
>   val f: t -> unit
> end
> =
> struct
>   type t = int * A.t
>
>   let f x = A.g x   (* does not type *)
> (*
>   let f (a, b) = A.g (a, b)   (* types correctly *)
> *)
> end
>
>
> =========================
>
>
>
> Note that if function f is replaced by the commented version, then the type
> checker succeeds. Even though, this code modification is only giving the
> additional information that the argument of f is a pair.
>
>
>
> It would be nice for both versions of the code to compile, because the
> current behavior of the type checker seems to me not easily predictable.
>
>
>
> Thank you in advance for your help,
>
>
>

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