From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=HTML_MESSAGE autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 7E9F1BBAF for ; Wed, 11 Jun 2008 12:51:23 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ap0CAPNKT0hC+Vq1aWdsb2JhbACCQDOOW0MNBAMECQ8Fl3+GPQ X-IronPort-AV: E=Sophos;i="4.27,623,1204498800"; d="scan'208";a="13819323" Received: from ik-out-1112.google.com ([66.249.90.181]) by mail3-smtp-sop.national.inria.fr with ESMTP; 11 Jun 2008 12:51:22 +0200 Received: by ik-out-1112.google.com with SMTP id c30so2408472ika.3 for ; Wed, 11 Jun 2008 03:51:22 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:message-id:date:from:to :subject:cc:in-reply-to:mime-version:content-type:references; bh=nh86SPldhaspJxmv+ymV1m9SOy9Bxe0rJKTatjtBEXk=; b=Jfldoquz74n1i2trcxvgWxH+/wlIH3i5dxv4OHmPc9gzvMTb0D4O6rD8zQTEK5L4s3 oK0GgDMiOEdPV0ZLhLJmvK4ahC7dH3enibp6Ky1S0net30HJYv5QuTlj/9FHFLT4Yqi7 xBKmI1ekhk4W40HRtRvuPQmAtsJmDpkKuHf3Y= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:cc:in-reply-to:mime-version :content-type:references; b=OuNrx63R3pspofVZ3dogbBjvFTPfg5X1rm9ftv/C4clJiUo3yrPg1AweQ0SmTVGU/1 6PDOou51RymUp6MF/7kFhu1kWYiuSuTNiuWvYRWtllqpjiLavsYWeYIO7TopylDFFcy7 IB27cKG2dDL9u5k+NM3W8UPe61ezUJzy543x8= Received: by 10.210.10.1 with SMTP id 1mr5035638ebj.158.1213181482008; Wed, 11 Jun 2008 03:51:22 -0700 (PDT) Received: by 10.210.39.11 with HTTP; Wed, 11 Jun 2008 03:51:21 -0700 (PDT) Message-ID: <676aba050806110351q7bedc2ccs31ca5867c39cfd41@mail.gmail.com> Date: Wed, 11 Jun 2008 12:51:21 +0200 From: "Charles Hymans" To: "Josh Berdine" Subject: Re: [Caml-list] typing of recursive modules in 3.10.2 Cc: "caml-list@yquem.inria.fr" In-Reply-To: <857DD0FDAC042B4485F9F5F4EA675104166C8EB605@EA-EXMSG-C332.europe.corp.microsoft.com> MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="----=_Part_220_32038405.1213181482003" References: <676aba050806101227m1696d555n6f23f55f57af0db2@mail.gmail.com> <857DD0FDAC042B4485F9F5F4EA675104166C8EB605@EA-EXMSG-C332.europe.corp.microsoft.com> X-Spam: no; 0.00; recursive:01 type-checker:01 recursive:01 typecheck:01 typechecker:01 bug:01 cheers:01 ocaml:01 sig:01 val:01 functor:01 sig:01 val:01 struct:01 struct:01 ------=_Part_220_32038405.1213181482003 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline 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 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, > > > ------=_Part_220_32038405.1213181482003 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline

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,

 


------=_Part_220_32038405.1213181482003--