Eliminating existentials, finally
 oleg@p...
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20071114 (08:39) 
From:  oleg@p... 
Subject:  Eliminating existentials, finally 
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 nontrivial 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 firstclass 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 poorman objects http://www.cs.cmu.edu/afs/cs/project/airepository/ai/lang/scheme/oop/yasos/swob.txt The title betrays my hunch that coalgebraic implementations (using functions) typically require simpler types than the corresponding algebraic, datatype based implementations.