[Caml-list] Encoding existential types without modules

[Caml-list] Encoding existential types without modules

[Daniel Bünzli]

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

Re: [Caml-list] Encoding existential types without modules

[Jean-Christophe Filliatre]

Daniel Bünzli writes:
 > 
 > 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.

How tricky! Thanks for this post.

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

I guess  you really need  these three types  (at least before  we have
rank-2 polymorphism  in ocaml). As a  attempt to justify  this, let us
try to make a more generic, functorized, code from your first example.
It takes  the first of your  three types as argument  ('a counter) and
returns the third one (packed_counter) as a result (so obviously these
two types you need).

The functor looks like

	module Make(X : sig type 'a t end) : sig
	  type t (* the existential type exists 'a. 'a t *)
	  val pack : 'a X.t -> t
	  ...
        end = struct
	  ...
        end

To be  able to use  the abstract  type t, we  would like to  provide a
function similar to your with_packed_counter, of type

	val use : ('a. 'a X.t -> 'b) -> t -> 'b

Since we do not have  rank-2 polymorphism, your solution introduces an
intermediate record type, as the type of the first argument.

Finally we get this:

	module Make(X : sig type 'a t end) : sig 
	  type t
	  val pack : 'a X.t -> t
	  type 'a user = { f : 'b. 'b X.t -> 'a }
	  val use : 'a user -> t -> 'a
	end = struct
	  type 'a user = { f : 'b. 'b X.t -> 'a }
	  type t = { pack : 'a. 'a user -> 'a }
	  let pack impl = { pack = fun user -> user.f impl }
	  let use f p = p.pack f
	end

and it seems  that we can't avoid the three  types solution. Note that
for other examples requiring the returned type to be polymorphic (e.g.
the compositional list example) you need to write another functor.

-- 
Jean-Christophe


Daniel Bünzli writes:
 > 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


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

Re: [Caml-list] Encoding existential types without modules

[Daniel Bünzli]

Thanks for your feedback.

Besides, I would just like to point out that the way I solved the 
problem of polymorphic recursion for the apply function in the example 
of the list of composable function cannot be applied in general.

A general way to solve the problem of polymorphic recursion was given 
by Brian Rogoff in a previous post [1]. Applying this solution gives 
the following (much simpler and maybe more efficient) code.

Daniel

[1] http://caml.inria.fr/archives/200208/msg00334.html

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
(* List of composable functions.

    The intended 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, 'z) list_scope = { bind_list : 'c. ('a -> 'c) * ('c, 'b) t 
-> '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)

(* Type to handle the polymorphic recursion of the apply function *)
type poly_rec = { apply : 'a 'b. poly_rec -> ('a, 'b) t -> 'a -> 'b }
let apply' r l x = match l with
| Nil id -> id x
| Cons l ->
     with_packed_list l { bind_list = function h,t -> r.apply r t (h x) }

let poly_rec = { apply = apply' }
let apply l x = apply' poly_rec 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

Re: [Caml-list] Encoding existential types without modules

[brogoff]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: TEXT/PLAIN; charset=X-UNKNOWN, Size: 2527 bytes --]

On Fri, 9 Jan 2004, [ISO-8859-1] Daniel Bünzli wrote:
> Thanks for your feedback.
>
> Besides, I would just like to point out that the way I solved the
> problem of polymorphic recursion for the apply function in the example
> of the list of composable function cannot be applied in general.
>
> A general way to solve the problem of polymorphic recursion was given
> by Brian Rogoff in a previous post [1]. Applying this solution gives
> the following (much simpler and maybe more efficient) code.

I blame Jacques Garrigue for that trick! He is entitled to transfer the blame
to whomever he chooses. ;-)

You may also want to consider using the recursive module feature introduced in
OCaml 3.07 for this too. Unfortunately, you can't (yet, Xavier says he's
working on it)  apply it directly to Funlist on account of your nil. That would
be best, but by wrapping apply I think you can do it like so:

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
(* List of composable functions.

     The intended 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, 'z) list_scope = { bind_list : 'c. ('a -> 'c) * ('c, 'b) t
                                   -> '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)

   module rec PolyRec : sig val apply : ('a, 'b) t -> 'a -> 'b end =
     struct
       let apply l x =
         match l with
         | Nil id -> id x
         | Cons l ->
             with_packed_list
           l { bind_list = function h,t -> PolyRec.apply t (h x) }
     end
   let apply = PolyRec.apply

 end

-- Brian

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