[Caml-list] Encoding existential types without modules

["Daniel Bünzli" <daniel.buenzli@epfl.ch>]

Hello,

I think this may be usefull to others (e.g. to port some clever haskell 
code). Below, I give two examples that show how to encode existential 
types in ocaml without using modules. This is done by adapting to ocaml 
the encoding given by Pierce in [1]. It uses polymorphic record fields.

The examples are a little bit silly but their aim is to show the 
concept of the encoding.
The first example is a counter abstract datatype. The second one is a 
datatype that can hold a list of composable function, that is a type 
that expresses something like

  type ('a, 'b) funlist = Nil of ('a ->'b) | Cons of exists 'c. ('a -> 
'c) * ('c,'b) funlist

I usually need three types to encode an existential type. Does anybody 
see a simpler way of doing that ?

Daniel

[1] Benjamin C. Pierce, Types and Programming Languages, section 24.3


--- Abstract counter datatype

(* The type expressed by the three types below is :
    type packed_counter =
       exists 'x. { create : 'x; get : ('x -> int); inc : ('x -> 'x)}
*)
type 'x counter = { create : 'x;  get : ('x -> int); inc : ('x -> 'x) }
type 't counter_scope = { bind_counter : 'x. 'x counter -> 't }
type packed_counter = { open_counter : 't. 't counter_scope -> 't }

(* Creating a package from a counter implementation *)
let pack_counter impl = { open_counter = fun scope -> 
scope.bind_counter impl }

(* Using a package with a scoped expression *)
let with_packed_counter p e = p.open_counter e

(* Two different implementations of the counter *)
let int_impl = { create = 1 ; get = (function i -> i) ; inc = (fun i -> 
i+1) }
let float_impl = { create = 1.0; get = (function i -> (int_of_float i)) 
;
		   inc = (fun i -> i +. 1.0) }

let counter = pack_counter int_impl
let counter' = pack_counter float_impl

(* An expression using an abstract counter *)
let expr =
   { bind_counter = fun counter -> (* counter is bound to the << 
interface >> *)
     (counter.get (counter.inc counter.create)) }

let result = with_packed_counter counter expr
let result' = with_packed_counter counter' expr

(*
    This doesn't type, the counter type is abstract !
    let expr =
    { bind_counter = fun counter ->
      (counter.get (counter.inc (counter.get counter.create))) }
*)

(*
    This doesn't type, the abstract type tries to escape its scope !
    let expr = { bind_counter = fun counter -> (counter.create) }
*)


--- Lists of composable functions.

module Funlist : sig

(* The funlist datatype *)
type ('a, 'b) t

(* Constructors *)
val nil : ('a, 'a) t
val cons : ('a -> 'b) -> ('b, 'c) t -> ('a, 'c) t

(* Applying a value to a composition *)
val apply : ('a, 'b) t -> 'a -> 'b

end = struct

(* The type expressed by the four types below is :
    type ('a, 'b) t = Nil of ('a -> 'b)
                    | Cons of exists 'c. ('a -> 'c) * ('c, 'b) t  *)

type ('a, 'b) t = Nil of ('a -> 'b) | Cons of ('a, 'b) packed_list
and ('a, 'b, 'c) list_data = ('a -> 'c) * ('c, 'b) t
and ('a, 'b, 'z) list_scope = { bind_list : 'c. ('a, 'b, 'c) list_data 
-> 'z}
and ('a, 'b) packed_list = { open_list : 'z. ('a, 'b, 'z) list_scope -> 
'z }

(* Packing and unpacking lists *)
let pack_list h t = { open_list = fun scope -> scope.bind_list (h,t) }
let with_packed_list p e = p.open_list e

(* Constructors *)
let nil = Nil(fun x -> x)
let cons h t = Cons(pack_list h t)


(* The following type is introduced to avoid the problem of polymorphic
recursion that comes while attempting a naive implementation of the 
apply
funtion. The idea was taken from Laufer, Odersky, Polymorphic Type 
Inference
and Abstract Data Types, 1994. *)

(* The type expressed by the three types below is :
     type 'b packed_apply = exists 'a. ('a, 'b) t * 'a
*)
type ('a, 'b) apply_data = ('a, 'b) t * 'a
type ('b, 'z) apply_scope = { bind_apply : 'a. ('a, 'b) apply_data -> 
'z}
type 'b packed_apply = { open_apply : 'z. ('b, 'z) apply_scope -> 'z}

(* Packing and unpacking applications *)
let pack_apply l x = { open_apply = fun scope -> scope.bind_apply (l,x) 
}
let with_packed_apply p e = p.open_apply e

let rec apply' a =
   with_packed_apply
     a { bind_apply = function
       | Nil id, x -> id x
       | Cons l, x ->
	  with_packed_list
	    l { bind_list = function h,t -> apply' (pack_apply t (h x))}}
	
let apply l x = apply' (pack_apply l x)

end

(* Example of use *)
let twice x = 2*x
let double x = (x, x)
let list = Funlist.cons twice (Funlist.cons (( = ) 4) (Funlist.cons 
double Funlist.nil))
let a, b = Funlist.apply list 2


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners