Eliminating existentials, finally

[oleg@pobox.com]

Peng Zang wrote:
> Is there a way to create lists in which the elements may be of
> differing types but which all have some set of operations defined
> (eg. tostr) in common?  One can then imagine mapping over such lists
> with "generic" versions of those common operations.

First of all, if simple type classes, mentioned during the discussion,
are desired, they can be easily obtained
	http://okmij.org/ftp/ML/ML.html#typeclass

(alas, modulo the convenient inference and automatic dictionary
construction). That is not the topic of this message however. We would
like to show that in some (many?) circumstances, existentials can be
just eliminated.

Peng Zang continued:
> Essentially we have ints, floats and bools.  All these types can be
> shown.  It would be nice to be able to create a list of them [1; 2.0;
> false] that you can then map a generalized show over.

So, we want abstract values with the only non-trivial operation of
converting them to strings. One may immediately ask: 
why not to convert them to strings to start with? So, instead of writing
	 [`Int 1; `Float 2.0; `Bool false]
we can just
	[string_of_int 1; string_of_float 2.0; string_of_bool false]
That idea looks better in Haskell: first of all, since polymorphic
equality is absent in Haskell, nothing breaks parametricity in
safe Haskell and we lose nothing in expressiveness if we treat
	forall a. Show a => a
as Strings. Also, because of the default laziness of Haskell, the
conversions to string are not performed unless needed. OTH, ML
programmers have never been scared of thunks. Thus the idea is to
represent an existential by a tuple of its observations, using thunks
to delay computations. 

Here is a more complex example, of a counter, whose interface could be
described as follows.

module type COUNTER = sig
  type t
  val init : unit -> t
  val observe : t -> int
  val step : t -> t
end;;

We see the producer, consumer/observer, and the transformer. Of course
we cannot use modules of the above signature for our purposes
since we cannot put modules into a list (cf: MoscowML and AliceML have
first-class modules). We do note however that the above is equivalent
to the following

type counter = C of (unit -> int) * (unit -> counter);;

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

let counter1 = 
  (* internal function, unavailable outside *)
  let rec make seed upper = 
    C ((fun () -> seed),(fun () -> 
      let seed = if seed >= upper then 0 else succ seed in make seed upper))
  in make 0 5;;

(* use FP seed *)
let counter2 = 
  (* internal function, unavailable outside *)
  let observe seed = int_of_float (10.0 *. seed) in
  let step seed = cos seed in
  let rec make seed = C ((fun () -> observe seed),
			 (fun () -> make (step seed)))
  in make 0.0;;


We can place them into a list

let lst = [counter1; counter2];;


and iterate over:

let advance_all = List.map (function C (_,adv) -> adv ());;
let show_all = List.iter (function C (s,_) -> Printf.printf "%d\n" (s()));;

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


We thus demonstrated a very old idea (whose realization in 1976 was
the birth of Scheme) that closures are poor-man objects

http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/lang/scheme/oop/yasos/swob.txt

The title betrays my hunch that co-algebraic implementations (using
functions) typically require simpler types than the corresponding
algebraic, data-type based implementations.