[MLton-user] Generating dummy values for tying cycles, serialization

[Vesa Karvonen]

In

  Type-Specialized Serialization with Sharing,
  Martin Elsman,
  University of Copenhagen,
  IT University Technical Report TR-2004-43, 2004.
  http://mlton.org/References#Elsman04

a type-indexed serialization library is described that has a combinator
refCyc for serializing (possibly cyclic) references.  refCyc has the
specification

  val refCyc : 'a -> 'a pu -> 'a ref pu

which means that the user is responsible for passing a dummy value (the
first parameter) to refCyc for tying cycles.  (Read the report for further
details.)  In this very brief note (few words, more code) I'll show how to
generate dummy type-indexed values.

(The end of this message contains some utilities.  Full code is included
in this message.)

First a generic signature for "structural" type-indexed values:

signature STRUCTURAL_TYPE =
   sig
      type 'a t

      val iso : ('a, 'b) emb -> 'b t -> 'a t

      val * : 'a t * 'b t -> ('a, 'b) product t
      val + : 'a t * 'b t -> ('a, 'b) sum t

      val Y : 'a t Fix.t

      val --> : 'a t * 'b t -> ('a -> 'b) t

      val exn : exn t
      val regExn : (exn -> ('a * 'a t) option) effect

      val array : 'a t -> 'a array t
      val list : 'a t -> 'a list t
      val refc : 'a t -> 'a ref t
      val vector : 'a t -> 'a vector t

      val bool : bool t
      val char : char t
      val int : int t
      val real : real t
      val string : string t
      val unit : unit t
      val word : word t
   end

Then the signature for the type-indexed dummy values:

signature DUMMY =
   sig
      include STRUCTURAL_TYPE

      val dummy : 'a t -> 'a

      val prj : ('b -> 'a) -> 'b t -> 'a t
   end

The implementation is mostly straightforward (see the comments for some
fine points):

structure Dummy :> DUMMY =
   struct
      type 'a t = 'a option

      val dummy = valOf

      fun prj b2a = Option.map b2a

      fun iso (_, p) = prj p

      (* When computing dummy products and sums we propagate definedness: *)
      fun a * b = case a & b of
                     SOME a & SOME b => SOME (a & b)
                   | _ => NONE

      fun a + b = case a of
                     SOME a => SOME (INL a)
                   | NONE => Option.map INR b

      fun Y ? = Fix.pure (const (NONE, id)) ?
      (* We use the more general Fixpoint framework (by Stephen Weeks)
       * that allows functional fixpoints.  Note that the initial value is
       * undefined.
       *)

      fun _ --> _ = SOME (fail (Fail "Dummy.-->"))
      (* To define a function (for example), no other dummy values are
       * needed.
       *)

      val exn = SOME Empty
      val regExn = ignore

      fun array _ = SOME (Array.tabulate (0, undefined))
      fun list _ = SOME []
      fun refc a = Option.map ref a
      fun vector _ = SOME (Vector.tabulate (0, undefined))

      val bool = SOME false
      val char = SOME #"\000"
      val int = SOME 1
      val real = SOME 0.0
      val string = SOME ""
      val unit = SOME ()
      val word = SOME 0w0
   end

Here is an example:

datatype 'a tree = B of 'a tree * 'a * 'a tree | N

fun tree a =
    let
       open Fix Dummy
    in
       fix Y (fn tree_a =>
                 iso (fn B (l, x, r) => INL (l & x & r) | N => INR (),
                      fn INL (l & x & r) => B (l, x, r) | INR () => N)
                     (tree_a * a * tree_a + unit))
    end

val N =
    let
       open Dummy
    in
       dummy (tree int)
    end

Using this technique, it should be possible to build a serialization
library that doesn't require the user to specify a dummy value for
serializing references.

The necessary utilities and the Fixpoint framework are below.

-Vesa Karvonen

(* Operator precedence table *)
infix   8  * / div mod        (* +1 from Basis Library *)
infix   7  + - ^              (* +1 from Basis Library *)
infixr  6  :: @               (* +1 from Basis Library *)
infix   5  = <> > >= < <=     (* +1 from Basis Library *)
infix   4  <\ \>
infixr  4  </ />
infix   3  o
infix   2  >|
infixr  2  |<
infix   1  :=                 (* -2 from Basis Library *)
infix   0  before &
infixr  0  -->

(* Some basic combinators *)
fun const x _ = x
fun cross (f, g) (x, y) = (f x, g y)
fun curry f x y = f (x, y)
fun fail e _ = raise e
fun id x = x
fun undefined _ = raise Fail "undefined"
fun fst (a, _) = a
fun snd (_, b) = b

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

(* Sum type *)
datatype ('a, 'b) sum = INL of 'a | INR of 'b

(* Some type shorthands *)
type 'a sq = 'a * 'a
type 'a uop = 'a -> 'a
type 'a fix = 'a uop -> 'a
type 'a thunk = unit -> 'a
type 'a effect = 'a -> unit
type 'a compare = 'a sq -> order
type ('a, 'b) emb = ('a -> 'b) * ('b -> 'a)

(* Infixing, sectioning, and application operators *)
fun x <\ f = fn y => f (x, y)
fun f \> y = f y
fun f /> y = fn x => f (x, y)
fun x </ f = f x

(* Piping operators *)
val op>| = op</
val op|< = op\>

(* Fixpoint framework with the "pure" combinator *)
signature FIX =
   sig
      type 'a t1
      type 'a t2
      type 'a t = 'a t1 -> 'a t2

      exception Fix

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

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

      exception Fix

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

      val pure = id

      fun tier th () =
          let
             val (a, ta) = th ()
          in
             (a, const a o ta)
          end

      fun iso (a2b, b2a) b () =
         let
            val (b, tb) = b ()
         in
            (b2a b, b2a o tb o a2b)
         end

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