Message-Id: <9604040809.AA38159@idse.heidelbg.ibm.com>
To: Christophe Raffalli <raffalli@cs.chalmers.se>
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>
>
>
> 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