Phantom booleans for encoding arbitrary finite relations

I'm not sure whether this technique has already been documented and/or
discovered earlier (wouldn't surprise me if it has), but at least I
haven't seen it, and the result seems theoretically interesting.
Basically, I will briefly present a technique that makes it relatively
straightforward to encode arbitrary finite relations at the type level
using just the very simple type system of Standard ML.

Tinkering the other day on some SML code, I wanted to encode a constraint
of the form

T(false) x T(false) -> T(false)
T(true) x T(false) -> T(true)
T(false) x  T(true) -> T(true)
T(true) x  T(true) -> type error

using phantom types.  (The type would be for a kind of join operation that
ensures that a particular property can only be specified once.)  I first
tried to design an ad hoc scheme for the constraint, but it proved
surprisingly elusive.  Then it occurred to me that basically the same
encoding technique as employed in the "static sum" technique

http://mlton.org/StaticSum

should also work purely at the type level.  The basic trick used in the
static sum technique is that the type of a static sum specifies the type
of deconstructing the sum.  Adapting the static sum technique to work
purely at the type level, one can drop the type variables that specify the
type of the value carried by a sum.

Below is a bit of SML code that implements the idea.  You should be able
to evaluate it using any SML implementation.

infix 6 andb
infix 5 xorb
infix 4 orb

structure PhantomBool :> sig

type ('false, 'true, 'result) t
(* Type level boolean.  To inspect a type-level boolean one specifies
* the 'false and 'true types and unifies with the boolean.  The
* 'result is then either the 'false or the 'true type. *)

(* Abbreviations for true and false. *)
type ('f, 't) T = ('f, 't, 't) t  (* {true} *)
type ('f, 't) F = ('f, 't, 'f) t  (* {false} *)

(* The following values are just for playing with type level
* booleans.  Ordinarily type level booleans would just appear as
* phantom type constraints.  Type expressions involving type level
* booleans can be quite complicated.  The following values allow one
* to use the type checker to infer desired type constraints from a
* program term. *)

val t : ('f, 't) T
val f : ('f, 't) F

val split : (('f1, 't1) F * ('f2, 't2) F,
('f3, 't3) T * ('f4, 't4) T,
('f5, 't5, 'r5) t * ('f6, 't6, 'r6) t) t ->
('f5, 't5, 'r5) t * ('f6, 't6, 'r6) t
(* In the absence of first-class polymorphism, split allows one to
* deconstruct a boolean multiple times with different types. *)

val iff : ('f, 't, 'r) t -> 't -> 'f -> 'r
(* Does not return normally. *)

val notb : (('f1, 't1) T, ('f2, 't2) F, ('f, 't, 'r) t) t ->
('f, 't, 'r) t
val andb : (('f1, 't1) F * ('f2, 't2) F, ('f3, 't3) F * ('f4, 't4) T,
'a * 'b) t * ('a, 'b, ('f, 't, 'r) t) t
-> ('f, 't, 'r) t
val orb : (('f1, 't1) F * ('f2, 't2) T, ('f3, 't3) T * ('f4, 't4) T,
'a * 'b) t * ('a, 'b, ('f, 't, 'r) t) t
-> ('f, 't, 'r) t
end = struct
type ('f, 't, 'r) t = unit
type ('f, 't) T = unit
type ('f, 't) F = unit
val t = ()
val f = ()
fun split () = ((), ())
fun iff _ = raise Fail "Phantom.Bool.iff"
val notb = ignore
val op andb = ignore
val op orb = ignore
end

open PhantomBool

Now, below are a few small examples.  To actually see the types, which is
the whole point, you need to evaluate them in a SML REPL.

First a simple equality test for type level booleans:

fun eq (a, b) = let
val (a, a') = split a
in
iff b a (notb a')
end

First evaluate it and then try each of the following:

fn () => eq (f, f)
fn () => eq (f, t)
fn () => eq (t, f)
fn () => eq (t, t)

Here is a definition of exclusive or:

fun a xorb b = let
val (a, a') = split a
in
iff b (iff a f t) (iff a' t f)
end

Evaluate it and then try each of the following:

fn () => f xorb f
fn () => f xorb t
fn () => t xorb f
fn () => t xorb t

Here is a definition of 2-bit modular arithmetic addition:

fun add2 ((l0, l1), (r0, r1)) = let
val (l0, l0') = split l0
val (r0, r0') = split r0
in
(l0 xorb r0, l0' andb r0' xorb l1 xorb r1)
end

If you evaluate it, you can see that it has a fairly complicated type
(which likely isn't the simplest type possible to express the relation).
Nevertheless, it works as it should:

fn () => add2 ((t, f), (t, f))  (* 1 + 1 = 2 = (f, t) *)
fn () => add2 ((t, t), (t, f))  (* 3 + 1 = 0 = (f, f) *)
(* ... *)

As an exercise, you might wish to try to come up with a type that
expresses 2-bit multiplication.  (Hint: Implement a multiplication
function using t, f, iff, ... and read the type of the function.)

Now, if you think about it for a moment, this technique, type level
booleans, allows one to encode arbitrary finite relations at the type
level using just the simple type system of Standard ML.  Furthermore, it
is relatively straightforward to come up with a particular relation.  The
obvious downside of the technique is that the types grow rather rapidly.

Finally, here is an encoding of the constraint I mentioned at the
beginning:

functor TryJoin
(type error
val join : (('f1, 't1) F * ('f2, 't2) T, ('f3, 't3) T * error,
'a * 'b) t * ('a, 'b, ('f, 't, 'r) t) t
-> ('f, 't, 'r) t) = struct
val a = fn () => join (f, f)
val b = fn () => join (f, t)
val c = fn () => join (t, f)
(* val d = fn () => join (t, t) (* uncomment for a type error *) *)
end

If you compare the type of join to the type of PhantomBool.orb, you can
see that it is the same except for the "error" at a position that
corresponds to the case where both arguments to join are true.

-Vesa Karvonen