[MLton-user] Combining type-indexed values using functors or how to get two for the price of one

Vesa Karvonen vesa.karvonen at cs.helsinki.fi
Tue Aug 29 15:00:00 PDT 2006


In

  Encoding Types in ML-like Languages
  Zhe Yang
  ICFP 1998
  http://mlton.org/References#Yang98

the problem of combining type-indexed values that use the (ad hoc)
value-dependent encoding is explained.  ("Value-dependent" means that the
type-index depends on (and essentially is) the value that is being
indexed.)  The problem is nicely demonstrated in the paper using the
example

  fn T => flatten T o super_reverse T

where the type-indexed values flatten and super_reverse would ideally be
separately implemented functions that need not know anything about each
other.  Unfortunately, that would seem to be in conflict with the value
dependent encoding of type-indices.  It is also mentioned that the problem
can be evaded by tupling the type-indices.  In this reasonably brief note
I'll follow up on that idea.

Let me first note that the problem is quite real.  Combining *arbitrary*
type-indexed values using value-dependent encodings can not be done
conveniently (or so it seems to be).  However, it seems that many useful
type-indexed values can be specified using the same kind (as in having the
same signature) of type-indices and if we restrict the problem to
combining type-indexed values that share the same kind of type-indices,
then we can combine them fairly conveniently.  It should be possible for
the following signature for "structural" (meaning that no "nominal" data
is used to specify type-indices) type-indices to be shared by
implementations of such type-indexed values as (the example types are
somewhat naive, but should give the idea)
- arbitrary: 'a t -> rnd_gen -> 'a,
- compare: 'a t -> 'a * 'a -> order,
- dummy: 'a t -> 'a,
- embedding: 'a t -> ('a, Foreign.value) emb,
- hash: 'a t -> 'a -> word, and
- serialization: 'a t -> ('a, Word8Vector.vector) emb.
It would be unfortunate if we would have to implement the type-indices
for each user-defined type and each type-indexed value separately.  On the
other hand, consider the possibility that the following code

  fun option a = iso (fn NONE => INL () | SOME a => INR a,
                      fn INL () => NONE | INR a => SOME a)
                     (unit + a)

would be sufficient to implement a hash function, a compare function, a
dummy function, a function for generating arbitrary values, serialization
functions, and even embedding functions (for an embedded interpreter) (and
more) for the option datatype.

(Full code is included in this message.  See the end of the message for
utilities.)

Let's then take a look at the STRUCTURAL_TYPE signature:

signature STRUCTURAL_TYPE =
   sig
      type 'a t

      val iso : ('a, 'b) iso -> '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

I won't go into the design of the above signature.  It is a straighforward
simplification of the signature of show as described on the page

  http://mlton.org/TypeIndexedValues

and shares essentially the same design patterns.  It is also
straightforward to implement a functor for lifting modules that implement
the above signature to modules that implement a minor generalization of
the signature used by show, but I'll skip that.

As a reminder, here is how one could implement a type-indexed dummy value:

signature DUMMY =
   sig
      include STRUCTURAL_TYPE
      val dummy : 'a t -> 'a
   end

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

      val dummy = valOf

      fun prj b2a = Option.map b2a

      fun iso (_, p) = prj p

      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)) ?

      fun _ --> _ = SOME (fail (Fail "Dummy.-->"))

      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

And here is how one could implement a type-indexed compare function:

signature COMPARE =
   sig
      include STRUCTURAL_TYPE
      val compare : 'a t -> 'a compare
   end

structure Compare :> COMPARE =
   struct
      type 'a t = 'a compare

      val compare = id

      fun inj a2b b =
          b o cross (a2b, a2b)

      fun iso (i, _) = inj i

      fun a * b =
          fn (al & bl, ar & br) =>
             case a (al, ar) of
                EQUAL => b (bl, br)
              | result => result

      fun a + b =
          fn (INL l, INL r) => a (l, r)
           | (INL _, INR _) => LESS
           | (INR _, INL _) => GREATER
           | (INR l, INR r) => b (l, r)

      val Y = Fn.Y

      fun _ --> _ = undefined

      val exn = undefined
      val regExn = ignore

      val array = Array.collate
      val list = List.collate
      fun refc ? = inj ! ?
      val vector = Vector.collate

      val unit = fn ((), ()) => EQUAL
      val bool = inj (fn false => INL () | true => INR ()) (unit + unit)
      val char = Char.compare
      val int = Int.compare
      val word = Word.compare
      val real = Real.compare
      val string = String.compare
   end

As you can see, the signature of COMPARE promises more than what the
implementation of Compare delivers.  Namely, functions and exceptions are
not really supported and an attempt to use a compare function whose type
contains arrows or exn may result in a run-time exception.  This is a
price one has to pay if one wants to be able to use the same signature for
a number of different type-indexed values.  (Well, it is probably possible
to reintroduce the necessary constraints (namely that compare requires a
type-index that contains neither arrows nor exn) using phantom types, but
I haven't yet investigated the possibility.  It would certainly complicate
the STRUCTURAL_TYPE signature.)

Now, to recap the problem, the code

  local
     open Compare
  in
     fun option a = iso (fn NONE => INL () | SOME a => INR a,
                         fn INL () => NONE | INR a => SOME a)
                        (unit + a)
  end

would implement a type-index (or, more precisely, a type-index
constructor) for compare functions and essentially the same code

  local
     open Dummy
  in
     fun option a = iso (fn NONE => INL () | SOME a => INR a,
                         fn INL () => NONE | INR a => SOME a)
                        (unit + a)
  end

would implement a type-index for dummy values.  Alas, the type-indices are
not the same:

  val option : 'a Compare.t -> 'a option Compare.t
  val option : 'a Dummy.t -> 'a option Dummy.t

So, we need a way to combine type-indexed values.  This can be done using
a straightforward pairing functor:

functor StructuralTypePair (structure A : STRUCTURAL_TYPE
                            structure B : STRUCTURAL_TYPE) :>
   STRUCTURAL_TYPE
      where type 'a t = 'a A.t * 'a B.t =
   struct
      type 'a t = 'a A.t * 'a B.t

      fun iso ? = cross (A.iso ?, B.iso ?)

      local
         fun mk t ((a1, a2), (b1, b2)) =
             cross t ((a1, b1), (a2, b2))
      in
         fun op * ? = mk ( A.*, B.* ) ?
         fun op + ? = mk ( A.+, B.+ ) ?
         fun op --> ? = mk ( A.-->, B.--> ) ?
      end

      fun Y ? =
          let
             open Fix
          in
             iso (fn (a, b) => a & b,
                  fn a & b => (a, b))
                 (A.Y ^ B.Y)
          end ?

      val exn = (A.exn, B.exn)
      fun regExn ? =
          (A.regExn (Option.map (cross (id, fst)) o ?)
         ; B.regExn (Option.map (cross (id, snd)) o ?))

      fun array ? = cross (A.array, B.array) ?
      fun list ? = cross (A.list, B.list) ?
      fun refc ? = cross (A.refc, B.refc) ?
      fun vector ? = cross (A.vector, B.vector) ?

      val bool = (A.bool, B.bool)
      val char = (A.char, B.char)
      val int = (A.int, B.int)
      val real = (A.real, B.real)
      val string = (A.string, B.string)
      val unit = (A.unit, B.unit)
      val word = (A.word, B.word)
   end

To combine the type-indices of the Compare and Dummy modules one could
write:

structure StructuralType =
  StructuralTypePair (structure A = Compare
                      structure B = Dummy)

A single type-index implementation

local
   open StructuralType
in
   fun option a = iso (fn NONE => INL () | SOME a => INR a,
                       fn INL () => NONE | INR a => SOME a)
                      (unit + a)
end

can now be used by both Compare and Dummy - well, almost.  We still need
to lift the compare and dummy function to the combined type-indices.  This
can also done relatively conveniently by defining a lifting functor for
each type-indexed value.  Here are suitable functors for Compare and
Dummy:

functor LiftCompare
      (structure StructuralType : STRUCTURAL_TYPE
       structure Compare : COMPARE
       val prj : 'a StructuralType.t -> 'a Compare.t) =
   struct
      fun compare ? = (Compare.compare o prj) ?
   end

functor LiftDummy
      (structure StructuralType : STRUCTURAL_TYPE
       structure Dummy : DUMMY
       val prj : 'a StructuralType.t -> 'a Dummy.t) =
   struct
      fun dummy ? = (Dummy.dummy o prj) ?
   end

(In this simple example, the benefit of using functors for lifting may not
be obvious.  Consider that some type-indexed values may need (many) extra
"specifiers" that refine some aspects of the type-index.  For example, a
specifier of the type

  val acyclic : 'a Serialize.t uop

could be used to specify (modify a type-index) that no cyclicity detection
is necessary for serialization.)

Then, using the lifting functors, we would create lifted versions of the
compare and dummy functions:

local
   fun prjA (a, _) = a
   fun prjB (_, b) = b

   structure Compare = LiftCompare
      (structure StructuralType = StructuralType
       structure Compare = Compare
       val prj = prjA)

   structure Dummy = LiftDummy
      (structure StructuralType = StructuralType
       structure Dummy = Dummy
       val prj = prjB)
in
   open Compare Dummy
end

We can finally use the same type-index for both compare and dummy

local
   open StructuralType
in
   val option_int = option int
end

val GREATER = compare option_int (SOME 2, SOME 1)
val NONE = dummy option_int

It is worth noting that the modules Compare and Dummy do not depend on
each other.  They only depend on the STRUCTURAL_TYPE signature.

Obviously, if we had implementations of other type-indexed values (hash,
serialize, ...) that implement the same STRUCTURAL_TYPE signature we
could also pair them together and lift the type-indexed values to use the
combined type-indices.

-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) iso = ('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 *)
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) iso -> '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

structure Fn :>
   sig
      val Y : ('a -> 'b) Fix.t
   end = struct
      fun Y ? = Fix.tier (fn () =>
                             let
                                val r = ref (fail Fix.Fix)
                                fun f x = !r x
                             in
                                (f, r <\ op :=)
                             end) ?
   end



More information about the MLton-user mailing list