From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <AndreasRossberg@web.de>
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=none autolearn=disabled 
	version=3.1.3
Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38])
	by yquem.inria.fr (Postfix) with ESMTP id 19557BC0A
	for <caml-list@yquem.inria.fr>; Tue, 15 May 2007 19:40:18 +0200 (CEST)
Received: from fmmailgate02.web.de (fmmailgate02.web.de [217.72.192.227])
	by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l4FHeHUH012569
	for <caml-list@inria.fr>; Tue, 15 May 2007 19:40:17 +0200
Received: from smtp06.web.de (fmsmtp06.dlan.cinetic.de [172.20.5.172])
	by fmmailgate02.web.de (Postfix) with ESMTP id E03DA7DC8B1F;
	Tue, 15 May 2007 19:40:16 +0200 (CEST)
Received: from [84.165.180.53] (helo=wiko)
	by smtp06.web.de with smtp (WEB.DE 4.108 #197)
	id 1Ho10S-0000nU-00; Tue, 15 May 2007 19:40:16 +0200
Message-ID: <01c201c79718$310774d0$16b2a8c0@wiko>
From: "Andreas Rossberg" <AndreasRossberg@web.de>
To: "Josh Berdine" <berdine@dcs.qmul.ac.uk>,
	"'ocaml ml'" <caml-list@inria.fr>
References: <02bd01c79707$7b9d4c60$72d7e520$@qmul.ac.uk><4649DFDD.6040409@philippewang.info> <02d701c79712$0fbb09f0$2f311dd0$@qmul.ac.uk>
Subject: Re: [Caml-list] type aliases and recursive modules
Date: Tue, 15 May 2007 19:40:55 +0200
MIME-Version: 1.0
Content-Type: text/plain;
	format=flowed;
	charset="iso-8859-1";
	reply-type=original
Content-Transfer-Encoding: 7bit
X-Priority: 3
X-MSMail-Priority: Normal
X-Mailer: Microsoft Outlook Express 6.00.2900.3028
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.3028
Sender: AndreasRossberg@web.de
X-Sender: AndreasRossberg@web.de
X-Provags-ID: V01U2FsdGVkX1+9xpOD5Myzq3TbxU1SZ+BB0j6FuwLRl18QgISm
	igHda8esY5PkmQXWj7b8qJJjYUWReBaropSJegbH94LW7nwOJA
	uo+J2ddLlexKYejS1kaA==
X-Miltered: at discorde with ID 4649F081.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)!
X-Spam: no; 0.00; rossberg:01 recursive:01 sig:01 val:01 val:01 struct:01 sig:01 struct:01 arises:01 recursive:01 abstraction:01 ocaml:01 abstract:01 abstract:01 rec:01 

"Josh Berdine" <berdine@dcs.qmul.ac.uk>:
> #
> module rec A : sig
>  type t = It of ASet.t
>  val compare : t -> t -> int
>  val get : t -> ASet.t
> end = struct
>  type t = It of ASet.t
>  let compare = compare
>  let get = function It(x) -> x
> end
>
> and ASet : sig
>  type t
>  val get_its_elements : t -> A.t list
> end = struct
>  module C = Set.Make(A)
>  type t = C.t
>  let get_its_elements x = C.elements (A.get (C.choose x))
> end
>
>                                      Characters 350-370:
>    let get_its_elements x = C.elements (A.get (C.choose x))
>                                        ^^^^^^^^^^^^^^^^^^^^
> This expression has type ASet.t but is here used with type
>  C.t = Set.Make(A).t

You are suffering from the "double vision" problem. This arises when you 
have a recursive module with an abstract type and attempt to cross the 
abstraction boundary recursively. The type system does not make the abstract 
type recursively transparent. Here is a simpler example:

# module rec A : sig type t val f : t -> t end =
  struct type t = int let f (x : t) = A.f x end;;
This expression has type t = int but is here used with type A.t

You cannot do that in current Ocaml. The only way to avoid this problem is 
by making the type t transparent in the ascribed signature.

This problem actually is not straightforward to address on the 
type-theoretic level, and one of the reasons why recursive modules are 
pretty much an open research topic.

Hope this helps,
- Andreas