[MLton-user] Fixpoints

[Stephen Weeks]

> I'm not sure I like the uncurrying of fix or the new specification
> of iso, but those are largely stylistic issues.

Yep.  Those changes both follow two long-standing MLton conventions
that have proved extremely useful:

  1. Only use currying if there is actual staging of computation going
     on.
  2. Always take the object of the type being described by the
     signature as the first argument to a function.

> >     datatype 'a u = U of ('a * ('a -> 'a))
> >     type 'a t = 'a u thunk
> 
> The above definition of u has a problem.  Namely, a user can now
> instantiate the tier thunk.

Good point, but the problem is not so much the definition of u, the
problem is that I exposed too much in the interface.  One can tweak my
interface so that it only exposes that "t" is an arrow type, and hence
can be eta-expanded to circumvent the value restriction.

> It seems that the type of the tiers should be changed to
> 
> >       val tier: ('a * 'a effect) thunk -> 'a t
> 
> where
> 
>   type 'a effect = 'a -> unit
> 
> In other words, the tying of the knot using this fixpoint framework is
> inherently imperative and it leads to slightly simpler code when this is
> reflected in the types.

I considered that, and thought that I would stick with the more
general type that I proposed, because it allows the post-fixpoint
tying of the knot to do some interesting computation.  However, I
admit it's not clear if that's useful, and drop it until someone shows
that it is.  If one ever needs to go back, it should be easy enough to
add a more general tier function to the interface and re-implement Fix
without changing any old clients.

> Also, I'm not sure whether to prefer ordinary eta-expansion
> 
> >       fun T ? = Fix.iso (Promise.T, (IN, fn IN p => p)) ?
> 
> or just plain thunking
> 
> >       fun T () = Fix.iso (Promise.T, (IN, fn IN p => p))
> 
> leading to slightly different types.

I think eta-expansion is both preferable and leads to simpler types
and implementation (once I got the interface right).

Here is my proposal incorporating the above changes.  Note that the
"t" type is all that is used in the specifications -- I think that is
simpler that having a client need to understand both "t" and "t'".

signature FIX =
   sig
      type 'a t1
      type 'a t2
      type 'a t = 'a t1 -> 'a t2

      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 -> unit)) thunk -> 'a t
  end

The complete code is below -- it is a minor modification of the
earlier code that I sent.

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

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 t1
      type 'a t2
      type 'a t = 'a t1 -> 'a t2

      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 -> unit)) thunk -> 'a t
  end

structure Fix :> FIX =
   struct
      type 'a t1 = unit
      type 'a t2 = 'a * ('a -> unit)
      type 'a t = 'a t1 -> 'a t2

      exception Fix
      
      val tier = id
         
      fun fix (t, f) =
         let
            val (a, a') = t ()
            val () = a' (f a)
         in
            a
         end
      
      fun (a ^ b) () =
         let
            val (a, a') = a ()
            val (b, b') = b ()
         in
            (a & b, fn a & b => (a' a; b' b))
         end
      
      fun iso (a, (a2b, b2a)) () =
         let
            val (a, a') = a ()
         in
            (a2b a, 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)
                          in
                             (fn a => !r a, fn f' => r := 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)
                        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