Relation between functors and polymorphism

Relation between functors and polymorphism

[Christophe Raffalli]

Hi,

I have a question that arise in the following circonstances:
I modified the Hashtbl library to make it a function taking a "key structure"
containing a type "key" a function "hash : key -> int" and a function "eq :
key -> key -> bool". Then I wondered how I could use the polymorphic hash and
equality functions to recover the original polymorphic Hashtbl structure.

You can generalize the question to:

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 ?

---

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


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

----
Christophe Raffalli
Dept. of Computer Sciences
Chalmers University of Technology

URL: http://www.logique.jussieu.fr/www.raffalli

Re: Relation between functors and polymorphism

[Wolfgang Lux]

> 
> 
> 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