Fixpoints

This page discusses a framework that makes it possible to compute fixpoints over arbitrary products of abstract types. The code is from an Extended Basis library (README).

First the signature of the framework (tie.sig):

<!IncludeSVN(mltonlib/trunk/com/ssh/extended-basis/unstable/public/generic/tie.sig,sml,6:)>

fix is a type-indexed function. The type-index parameter to fix is called a "witness". To compute fixpoints over products, one uses the *` operator to combine witnesses. To provide a fixpoint combinator for an abstract type, one implements a witness providing a thunk whose instantiation allocates a fresh, mutable proxy and a procedure for updating the proxy with the solution. Naturally this means that not all possible ways of computing a fixpoint of a particular type are possible under the framework. The pure combinator is a generalization of tier. The iso combinator is provided for reusing existing witnesses.

Note that instead of using an infix operator, we could alternatively employ an interface using Fold. Also, witnesses are eta-expanded to work around the value restriction, while maintaining abstraction.

Here is the implementation (tie.sml):

<!IncludeSVN(mltonlib/trunk/com/ssh/extended-basis/unstable/detail/generic/tie.sml,sml,6:)>

Let’s then take a look at a couple of additional examples.

Here is a naive implementation of lazy promises:

structure Promise :> sig
   type 'a t
   val lazy : 'a Thunk.t -> 'a t
   val force : 'a t -> 'a
   val Y : 'a t Tie.t
end = struct
   datatype 'a t' =
      EXN of exn
    | THUNK of 'a Thunk.t
    | VALUE of 'a
   type 'a t = 'a t' Ref.t
   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 Y ? = Tie.tier (fn () => let
                             val r = lazy (raising Fix.Fix)
                          in
                             (r, r <\ op := o !)
                          end) ?
end

An example use of our naive lazy promises is to implement equally naive lazy streams:

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

Note that above we make use of the iso combinator. Here is a finite representation of an infinite stream of ones:

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