Refnum

[Stephen Weeks]

> re  Norman's  thing,  isn't  it  relatively clear that his original signature
> isn't achievable without cheats like cast?  It would  require  some  kind  of
> type  dispatch since given a 'a ref you can only compare it to other 'a refs.

It's pretty clear, but I'm not totally sure.  For example, here is an
implementation of Norman's original signature with a slightly different
underlying implementation of refs.

structure Refnum:
   sig
      structure Ref:
	 sig
	    type 'a t
	       
	    val reff: 'a -> 'a t
	    val ! : 'a t -> 'a
	    val := : 'a t * 'a -> unit
	 end
      
      val refnum: 'a Ref.t -> int
   end =
   struct
      structure Ref =
	 struct
	    datatype 'a t = T of 'a option ref

	    fun reset (T r) () =
	       case !r of
		  NONE => raise Fail "Ref.reset bug"
		| SOME v => (r := NONE; fn () => r := SOME v)

	    val isSome = fn (T r) => isSome (! r)

	    fun reff x = T (ref (SOME x))
	    val ! = fn (T r) => valOf (! r)
	    val op := = fn (T r, v) => r := SOME v
	 end
      
      val count: int ref = ref 0
      val refs: (unit -> unit -> unit) list ref = ref []

      fun 'a refnum (r: 'a Ref.t) =
	 let
	    fun loop (l, n) : int =
	       case l of
		  [] =>
		     let
			val n = !count + 1
		     in
			count := n
			; refs := Ref.reset r :: !refs
			; n
		     end
		| f :: l =>
		  let
		     val f = f ()
		     val is = Ref.isSome r
		     val _ = f ()
		  in
		     if is
			then loop (l, n - 1)
		     else n
		  end
	 in
	    loop (!refs, !count)
	 end
   end