[MLton-user] Fixpoints

[Vesa Karvonen]

Quoting Stephen Weeks <sweeks@sweeks.com>:
> I was reading through
> 
>   http://mlton.org/Fixpoints
> 
> and had an idea for simplifying things.

I was going to ask for feedback on the page once I got another page (on
type-indexed functions) ready and before linking them to the StandardML
page, but now I don't have to.

> 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.

Excellent idea!  This is actually the second time (that I recall) that
I've missed a similar simplification opportunity.  I'll have to make a
mental note to consider using closures whenever a signature contains extra
type variables that reveal implementation details.

> 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

The simplified tier types look good.  I'm not sure I like the uncurrying
of fix or the new specification of iso, but those are largely stylistic
issues.  One thing I've been wondering about is whether other tier
building combinators (in addition to iso and ^) would make sense.  A
couple of less cosmetic issues below.

>     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.  Consider the following kind of code:

  let
    val T = MyType.T ()  (* Instantiates the tier thunk *)
    val T = fn () => T
  in
    (fix T (* ... *), fix T (* ... *))
  end

The same slot/knot would tied twice, which (I think) shouldn't be allowed.
To fix this problem, the u type also needs to be thunked, so that only a
call to the fix function instantiates a tier.

Look at the tier closure specifications:

[...]
>                              (f, fn f' => (r := f'; f))
                                ^                     ^
[...]
>                            (p, fn x => (p := !x; p))
                              ^                    ^
[...]

As you can see, both of the closures return the same value that is already
returned as the "knot".  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.

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.

Below is a modified implementation with the simplified tier type, thunked
abstract tiers (to eliminate the retying problem), curried fix, and plain
thunking of tier implementations.

-Vesa Karvonen

fun cross (f, g) (x, y) = (f x, g y)
fun id x = x
fun dup x = (x, x)

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

type 'a uop = 'a -> 'a
type 'a fix = 'a uop -> 'a
type 'a thunk = unit -> 'a
type 'a effect = 'a -> unit
type ('a, 'b) ep = ('a -> 'b) * ('b -> 'a)   (* embedding/projection pair *)

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

    exception Fix

    val fix : 'a t -> 'a fix
    val ^ : 'a t * 'b t -> ('a, 'b) product t
    val tier : ('a * 'a effect) thunk -> 'a t'
    val iso : ('a, 'b) ep -> 'b t -> 'a t'
  end

structure Fix :> FIX =
  struct
    type 'a t' = ('a * 'a effect) thunk
    type 'a t = 'a t' thunk

    exception Fix

    val tier = id

    fun fix a f =
        let val (a, ta) = a () ()
        in ta (f a) : unit ; a
        end

    fun (a ^ b) () () =
        let val (a, ta) = a () ()
            val (b, tb) = b () ()
        in (a & b, fn a & b => (ta a : unit ; tb b : unit))
        end

    fun iso (a2b, b2a) b () =
        let val (b, tb) = b () ()
        in (b2a b, tb o a2b)
        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 x = !r x
                     in (f, fn f' => r := f')
                     end)
  end

val isEven & isOdd =
    let open Fix Fn in fix (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 r = lazy (fn () => raise Fix.Fix)
              in (r, fn r' => r := !r')
              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 (fn IN p => p, fn p => IN p) Promise.T
  end

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