[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