[MLton] broken attempt at encoding existentials

[Stephen Weeks]

For the archives.  Here's a broken attempt at encoding an existential
type (a counter object) in SML.  It all works, except I can't figure
out how to make unpack generate a different type for each occurrence.
Hence, uses of unpack that should be rejected are accepted.

------------------------------------------------------------

signature COUNTER =
   sig
      type 'a obj = {create: 'a, get: 'a -> int, inc: 'a -> 'a}
      type t  (* exists 'a. 'a obj *)
      type 'a z
      val pack: 'a obj -> t
      val unpack: t * ('a z obj -> 'b) -> 'b
   end

functor TestCounter (Counter: COUNTER) =
   struct
      open Counter
	 
      val intC = pack {create = 1, get = fn i => i, inc = fn i => i + 1}
      val realC = pack {create = 1.0, get = Real.round, inc = fn r => r + 1.0}

      fun doit c = unpack (c, fn {create, get, inc} =>
			   print (concat [Int.toString (get (inc (inc create))),
					  "\n"]))
      val _ = doit intC
      val _ = doit realC

      (* This should be a type error! *)
      val _ = unpack (intC, fn {create, ...} =>
		      unpack (realC, fn {get, ...} => get create))
   end

structure Counter: COUNTER =
   struct
      type 'a obj = {create: 'a, get: 'a -> int, inc: 'a -> 'a}

      datatype t = T of exn obj

      type 'a z = exn

      fun 'a pack ({create, get, inc}: 'a obj) =
	 let
	    exception E of 'a
	    val create = E create
	    val get = fn E a => get a | _ => raise Fail "impossible"
	    val inc = fn E a => E (inc a) | _ => raise Fail "impossible"
	 in
	    T {create = create,
	       get = get,
	       inc = inc}
	 end
	 
      fun unpack (T r, f) = f r
   end

structure Test = TestCounter (Counter)