[MLton-user] Fixpoints

[Stephen Weeks]

I was reading through

  http://mlton.org/Fixpoints

and had an idea for simplifying things.  The idea is to hide the type
of the slot used to construct fixpoints underneath a closure, so that
it doesn't appear in the type of tiers.  As a minor change, I think it
is also cleaner to include the thunk used to work around the value
restriction directly in the type of tiers.  Those changes and some
other minor cleanup lead to the following signature.

signature FIX =
   sig
      type 'a u
      type 'a t = 'a u thunk

      exception Fix
      
      val ^ : 'a t * 'b t -> ('a, 'b) product t
      val fix: 'a t * ('a -> 'a) -> 'a
      val iso: 'a t * ('a, 'b) emb -> 'b t
      val tier: ('a * ('a -> 'a)) thunk -> 'a t
  end

Now, a tier is a thunk that creates the slot and returns an initial
value for the knot paired with a function that ties the knot and
returns it.  But, the actual slot type is completely hidden in the
closures.

Here's the complete code.

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

datatype ('a, 'b) product = & of 'a * 'b
infix &

type 'a thunk = unit -> 'a
type ('a, 'b) emb = ('a -> 'b) * ('b -> 'a)

signature FIX =
   sig
      type 'a u
      type 'a t = 'a u thunk

      exception Fix
      
      val ^ : 'a t * 'b t -> ('a, 'b) product t
      val fix: 'a t * ('a -> 'a) -> 'a
      val iso: 'a t * ('a, 'b) emb -> 'b t
      val tier: ('a * ('a -> 'a)) thunk -> 'a t
  end

structure Fix :> FIX =
  struct
    datatype 'a u = U of ('a * ('a -> 'a))
    type 'a t = 'a u thunk

    exception Fix

    fun tier t = U o t

    fun fix (t, f) =
       let
          val U (a, a') = t ()
       in
          a' (f a)
       end

    fun a ^ b = fn () =>
       let
          val U (a, a') = a ()
          val U (b, b') = b ()
       in
          U (a & b, fn a & b => a' a & b' b)
       end

    fun iso (a, (a2b, b2a)) () =
       let
          val U (a, a') = a ()
       in
          U (a2b a, a2b o a' o b2a)
       end
  end

structure Fn :>
   sig
      val T : ('a -> 'b) Fix.t
   end =
   struct
      fun T ? = Fix.tier (fn () =>
                          let
                             val r = ref (fn _ => raise Fix.Fix)
                             fun f a = !r a
                          in
                             (f, fn f' => (r := f'; f))
                          end) ?
   end

val isEven & isOdd =
   Fix.fix
   (let open Fix Fn in T^T end,
    fn isEven & isOdd =>
       (fn 0w0 => true
         | 0w1 => false
         | n => isOdd (n-0w1)) &
       (fn 0w0 => false
         | 0w1 => true
         | n => isEven (n-0w1)))

structure Promise :>
  sig
    type 'a t
    val lazy : 'a thunk -> 'a t
    val force : 'a t -> 'a
    val T : 'a t Fix.t
  end = struct
    datatype 'a t' = EXN of exn
                   | THUNK of 'a thunk
                   | VALUE of 'a
    withtype 'a t = 'a t' ref
    fun lazy f = ref (THUNK f)
    fun force t =
        case !t of
          EXN e => raise e
        | THUNK f =>
          (t := VALUE (f ())
           handle e => t := EXN e
         ; force t)
        | VALUE v => v
    fun T ? = Fix.tier (fn () =>
                        let
                           val p = lazy (fn () => raise Fix.Fix)
                        in
                           (p, fn x => (p := !x; p))
                        end) ?
  end

structure Stream :>
   sig
      type 'a t
       
      val cons: 'a * 'a t -> 'a t
      val get: 'a t -> ('a * 'a t) option
      val T: 'a t Fix.t
   end =
   struct
      datatype 'a t = IN of ('a * 'a t) option Promise.t
      fun cons (x, xs) = IN (Promise.lazy (fn () => SOME (x, xs)))
      fun get (IN p) = Promise.force p
      fun T ? = Fix.iso (Promise.T, (IN, fn IN p => p)) ?
   end

val ones =
    let open Fix Stream
    in fix (T, fn ones => cons (1, ones))
    end