From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from weis@localhost) by pauillac.inria.fr (8.6.10/8.6.6) id KAA21213 for caml-redistribution; Fri, 5 Apr 1996 10:37:28 +0200
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.6.10/8.6.6) with ESMTP id KAA29322 for <caml-list@pauillac.inria.fr>; Thu, 4 Apr 1996 10:10:18 +0200
Received: from cherub.hd.ibm.de ([192.101.197.10]) by concorde.inria.fr (8.7.1/8.7.1) with SMTP id KAA17847 for <caml-list@pauillac.inria.fr>; Thu, 4 Apr 1996 10:09:29 +0200 (MET DST)
Received: from kaa.heidelbg.ibm.com by cherub.hd.ibm.de (AIX 3.2/UCB 5.64/4.03/chkV1.0)
          id AA55577; Thu, 4 Apr 1996 10:09:42 +0200
Received: from idse.heidelbg.ibm.com by kaa.heidelbg.ibm.com (AIX 3.2/UCB 5.64/4.03)
          id AA49021; Thu, 4 Apr 1996 10:09:16 +0200
Received: by idse.heidelbg.ibm.com (AIX 3.2/UCB 5.64/4.03)
          id AA38159; Thu, 4 Apr 1996 10:09:15 +0200
Message-Id: <9604040809.AA38159@idse.heidelbg.ibm.com>
To: Christophe Raffalli <raffalli@cs.chalmers.se>
Cc: caml-list@pauillac.inria.fr
Subject: Re: Relation between functors and polymorphism 
In-Reply-To: (Your message of Wed, 03 Apr 96 11:59:24 O.)
             <199604030959.LAA25846@lips.cs.chalmers.se> 
Date: Thu, 04 Apr 96 10:09:15 +0100
From: Wolfgang Lux <lux@heidelbg.ibm.com>
Sender: weis


> 
> 
> Hi,
> 
> [...]
> 
> What is the relation between a functor that only depends on one type (or more)
> like
> 
> module A (B : sig type t end) = struct
>   type u = Some of B.t | None
> 
>   let read = function
>     Some x -> x
>   | None -> raise Not_found
> end
> 
> and a polymorphic structure like
> 
> module A' = struct
>   type 'a u = Some of 'a | None
> 
>   let read = function
>     Some x -> x
>   | None -> raise Not_found
> end
> 
> They look isomorphic ?

No they are not isomorphic. The type A(B).u (for whatever module B the
matches the signature sig type t end), is monomorphic, while the type
'a A'.u is polymorphic.

> 
> ---
> 
> You can easely go from A' to A (This is quite verbose but you don't have to
> rewrite the types or functions definitions):
> 
> module A (B : sig type t end) = struct
>   type u = B.t A'.u
> 
>   let read = (A'.read : u -> B.t)
> end
> 

This is obviously possible, as you now consider the polymorphic type
'a A'.u for one concrete type B.t.

> 
> But how can you reconstruct A' from A without rewriting the type or function
> definitions. Is this impossible ?
> 

Yes. Once you have lost polymorphism by applying the type schme of
A'.u to a type B.t, the resulting type no longer has a free type
variable you cou generalize over.


Regards
Wolfgang

----
Wolfgang Lux
WZH Heidelberg, IBM Germany             Internet: lux@heidelbg.ibm.com
+49-6221-59-4546                        VNET:     LUX at HEIDELBG
+49-6221-59-3500 (fax)	                EARN:     LUX at DHDIBMIP