Re: existentials [was: Formal specifications of programming languages]

[oleg@okmij.org]

Jacques Garrigue wrote:
> There are no existentials in ocaml, only first-class universal types
> (in polymorphic methods and polymorphic record fields.)

Surely object types are existentials with respect to the types of their
fields?!

Wasn't it the very motivation of objects -- encapsulation -- to
abstract over the types of the fields and so prevent the outsiders
from finding out not only the values of the fields but also their types.
Outsiders should only use the methods of the object and should know
nothing about object's fields, if any.

As the illustration, here is the standard counter example, defining
one existential type and two its values. The values use two
different representations of the internal state of the counter: a pair
of integers and a float. This state is not observable: and so we can
place the two counter objects in the same list without any need for
coercions. OCaml knows that the state is not observable and so the two
objects have the same type, difference in the type of their state
notwithstanding. 

One must say that exactly the same example has been implemented
without any existentials whatsoever:

 Eliminating existentials, finally
 Caml-list, Nov 14, 2007
 http://caml.inria.fr/pub/ml-archives/caml-list/2007/11/dcd3aab066b5f28852db8ccaf35d35d7.en.html

which poses the question if existentials are really needed.


On with the example: the declaration of the existential type
 
class type counter = object ('self)
  method observe : int
  method step : unit -> 'self
end;;

Here are two different counters, with two different
representations of the internal state (a pair of int, or a float).

let counter1 = 
  object
   val seed = 0
   val upper = 5
   method observe = seed
   method step () = 
     let new_seed = if seed >= upper then 0 else succ seed in
     {< seed = new_seed >}
end;;

(* use FP seed *)
let counter2 = 
  object
   val seed = 0.0
   method observe = int_of_float (10.0 *. seed)
   method step () = {< seed = cos seed >}
end;;

We can place them into a list

let lst = [counter1; counter2];;

and iterate over:

let advance_all = List.map (fun c -> c#step ());;
let show_all = List.iter (fun c -> Printf.printf "%d\n" c#observe);;

let test = let () = show_all lst in
           let () = show_all (advance_all (advance_all lst))
           in ();;

result:
0
0
2
5
val test : unit = ()