doc/guide/src/Fixpoints.adoc

   1 Fixpoints
   2 =========
   3
   4 This page discusses a framework that makes it possible to compute
   5 fixpoints over arbitrary products of abstract types.  The code is from
   6 an Extended Basis library
   7 (<!ViewGitFile(mltonlib,master,com/ssh/extended-basis/unstable/README)>).
   8
   9 First the signature of the framework
  10 (<!ViewGitFile(mltonlib,master,com/ssh/extended-basis/unstable/public/generic/tie.sig)>):
  11 [source,sml]
  12 ----
  13 sys::[./bin/InclGitFile.py mltonlib master com/ssh/extended-basis/unstable/public/generic/tie.sig 6:]
  14 ----
  15
  16 `fix` is a <:TypeIndexedValues:type-indexed> function.  The type-index
  17 parameter to `fix` is called a "witness".  To compute fixpoints over
  18 products, one uses the +*&grave;+ operator to combine witnesses.  To provide
  19 a fixpoint combinator for an abstract type, one implements a witness
  20 providing a thunk whose instantiation allocates a fresh, mutable proxy
  21 and a procedure for updating the proxy with the solution.  Naturally
  22 this means that not all possible ways of computing a fixpoint of a
  23 particular type are possible under the framework.  The `pure`
  24 combinator is a generalization of `tier`.  The `iso` combinator is
  25 provided for reusing existing witnesses.
  26
  27 Note that instead of using an infix operator, we could alternatively
  28 employ an interface using <:Fold:>.  Also, witnesses are eta-expanded
  29 to work around the <:ValueRestriction:value restriction>, while
  30 maintaining abstraction.
  31
  32 Here is the implementation
  33 (<!ViewGitFile(mltonlib,master,com/ssh/extended-basis/unstable/detail/generic/tie.sml)>):
  34 [source,sml]
  35 ----
  36 sys::[./bin/InclGitFile.py mltonlib master com/ssh/extended-basis/unstable/detail/generic/tie.sml 6:]
  37 ----
  38
  39 Let's then take a look at a couple of additional examples.
  40
  41 Here is a naive implementation of lazy promises:
  42 [source,sml]
  43 ----
  44 structure Promise :> sig
  45    type 'a t
  46    val lazy : 'a Thunk.t -> 'a t
  47    val force : 'a t -> 'a
  48    val Y : 'a t Tie.t
  49 end = struct
  50    datatype 'a t' =
  51       EXN of exn
  52     | THUNK of 'a Thunk.t
  53     | VALUE of 'a
  54    type 'a t = 'a t' Ref.t
  55    fun lazy f = ref (THUNK f)
  56    fun force t =
  57       case !t
  58        of EXN e   => raise e
  59         | THUNK f => (t := VALUE (f ()) handle e => t := EXN e ; force t)
  60         | VALUE v => v
  61    fun Y ? = Tie.tier (fn () => let
  62                              val r = lazy (raising Fix.Fix)
  63                           in
  64                              (r, r <\ op := o !)
  65                           end) ?
  66 end
  67 ----
  68
  69 An example use of our naive lazy promises is to implement equally naive
  70 lazy streams:
  71 [source,sml]
  72 ----
  73 structure Stream :> sig
  74    type 'a t
  75    val cons : 'a * 'a t -> 'a t
  76    val get : 'a t -> ('a * 'a t) Option.t
  77    val Y : 'a t Tie.t
  78 end = struct
  79    datatype 'a t = IN of ('a * 'a t) Option.t Promise.t
  80    fun cons (x, xs) = IN (Promise.lazy (fn () => SOME (x, xs)))
  81    fun get (IN p) = Promise.force p
  82    fun Y ? = Tie.iso Promise.Y (fn IN p => p, IN) ?
  83 end
  84 ----
  85
  86 Note that above we make use of the `iso` combinator.  Here is a finite
  87 representation of an infinite stream of ones:
  88
  89 [source,sml]
  90 ----
  91 val ones = let
  92    open Tie Stream
  93 in
  94    fix Y (fn ones => cons (1, ones))
  95 end
  96 ----