The Commutativity monad

I have released Commutative, a monadic combinator library for writing commutative functions. This post explains the theory behind how it works.

Combinator-based, not Proof-based

Haskell's type system is quite precise and sophisticated, yet dependently-typed languages such as Agda and Idris manage to go even further. For example, using Agda, it is trivial to define the type of commutative functions: they are simply binary functions together with a proof that the function is commutative.

    record Commutative (a b : Set) : Set where
      field
        f : a → a → b
        prf : ∀ x y → f x y ≡ f y x

Haskell's type system is not powerful enough to represent proof objects, but even if it did, would you want to use them? Instead of writing proofs and programs in two separate steps, I much prefer Haskell's approach of using combinator libraries.

A simple example of a combinator library which avoids the need for proofs is bijections. The main idea is that since composing two bijections yields another bijection, programmers should be allowed to compose existing bijections without proof.

    data Bijection a b = MkBij (a -> b) (b -> a)
    
    instance Category Bijection where
      id = Bijection id id
      (MkBij g g') . (MkBij f f') = MkBij (g . f) (f' . g')

If the module exports a few bijective primitives but keeps the MkBij constructor private, users of the library will only be able to create Bijection instances through composition. Assuming the primitives were indeed proper bijections, this ensures that values of type Bijection are always guaranteed to be bijective. Without having to write any proof objects, even in the library!

Aspect-oriented Interlude

My passion for commutative (and associative) functions began while I was working on my master's thesis. I was working on aspect-oriented conflicts, and I soon discovered that the issue might not lie in the conflicting aspects themselves, but in the way in which those aspects were combined. The aspect-weaving process was not commutative!

Instead of keeping all the aspects in one global namespace and weaving them all together into one big program, I think aspects should be separated into independent "aquariums". One key aspect of my proposal is that there would be different types of aquariums, and only aspects of the same type should be combined with each other. Programmers may define custom aquariums, with one caveat: the aquarium must combine its aspects in a commutative and associative manner.

I knew that I couldn't just ask programmers to prove that all of their combination functions were commutative. Instead, I dedicated chapter 5 to a simple system which let programmers write "intrinsically" commutative functions, for which no further proof of commutativity would need to be written. That system eventually grew into today's combinator library.

Unordered pairs

My goal was to restrict the language in a way which ensured that only commutative functions could be written. The idea I came up with was to prevent functions from observing the order in which their arguments were given, by rewriting those two arguments into a unordered form. For example, if the arguments are both booleans, there are four possible (ordered) pairs of booleans, but only three unordered pairs.

    data Unordered_Bool = TT | TF | FF
    
    unorder_bool :: (Bool, Bool) -> Unordered_Bool
    unorder_bool (True,  True ) = TT
    unorder_bool (True,  False) = TF
    unorder_bool (False, True ) = TF
    unorder_bool (False, False) = FF

If a function is written in terms of Unordered_Bool instead of in terms of (Bool, Bool), then this function is commutative by construction, because the function has no way to distinguish the two orderings.

    xor :: Unordered_Bool -> Bool
    xor TF = True
    xor _  = False

The main limitation of this strategy is that not all types can be unordered in this fashion. Algebraic types are okay, but what about function types? If you need to write a higher-order commutative function, that is, a function which takes a pair of functions as arguments, then you would need a way to represent an unordered pair of functions. How do we represent that?

At the time when I wrote my thesis, I could not answer this question. But now I can!

Unordered observations

A function is defined by its observations, so it would make sense for an unordered pair of functions to also be defined by its available observations.

With an ordinary (ordered) pair of functions, that is, an observation-based value approximating the type (a -> b, a -> b), it would make sense of have an observation of type a -> (b, b). That is, in order to observe a pair of functions, you need to provide an argument at which each of the two functions will be observed, and you receive the output of each function on that argument.

The way to represent an unordered pair of functions is now blindingly obvious: instead of returning an ordered pair revealing which output came from which function, we should return an unordered pair. That is, our unordered pair of functions should have an observation of type a -> Unordered b.

If a function is written in terms of (a -> Unordered b) instead of (a -> b, a -> b), then this function is commutative by construction, because the function has no way to distinguish the two orderings. For example, if we want to implement a commutative higher-order function which returns true if at least one of its two function arguments returns true on either 0 or 1, we can implement it as follows.

    or01 :: (Int -> Unordered_Bool) -> Bool
    or01 fg = fg 0 /= FF || fg 1 /= FF

I really like this solution. It is clean, simple, elegant... and wrong.

Distinguishable observations

Okay, maybe not wrong, but at least incomplete. The strategy fails if we try to implement, for example, a commutative higher-order function which returns true if at least one of its two function arguments returns true on both 0 and 1.

    and01 :: (Int -> Unordered_Bool) -> Bool
    and01 fg | fg 0 == FF ||
               fg 1 == FF = False
    and01 fg | fg 0 == TT ||
               fg 1 == TT = True  -- Since the other is not FF.
    and01 fg | fg 0 == TF ||      -- Are the two T from the
               fg 1 == TF = ?     --  same function or not?

The problem with (a -> Unordered b) is that this representation is not just hiding the order of the original two arguments; it's hiding the order of every single observation. As the above example demonstrates, this is too strong.

The result TF indicates that a boolean observation has returned a different value for each argument. Once we have found such an observation, we ought to be able to use T and F as labels for the two arguments. We still won't know which was the first or second argument, but for each subsequent observation, we will know whether that observation came from the argument which resulted in T or from the one which resulted in F.

My commutativity monad is based on a single primitive, "distinguishBy", which does precisely what the previous paragraph describes. You ask it to perform a boolean observation (r -> Bool), which it performs on both arguments. If the answers are identical, you have failed to distinguish the arguments, but you still get to observe the Bool result. If the answers are different, hurray! You have successfully distinguished the two arguments, so you get the pair (r, r) corresponding to the original arguments.

The first r is always the argument for which the observation was False, while the second r is the one for which the observation was True. This way, you never learn the order in which the two r arguments were originally given, so the result is a Commutative operation from a pair of r to a value of type (Either Bool (r, r)).

    distinguishBy :: (r -> Bool)
                  -> Commutative r (Either Bool (r, r))

There is also "distinguish", a slightly more general version which uses Either instead of Bool. From those two operations, plus trivial implementations for bind and return, all unordered pairs and all commutative operations can be reimplemented in a way which guarantees commutativity.

Completeness

Since the problem with (a -> Unordered b) was that the representation could not be used to implement all commutative functions, it would be wise to verify that Commutative doesn't suffer from the same flaw. Here is an informal argument proving completeness. I don't think it's completely airtight, but it's good enough for me.

proof:

Suppose f is a pure, computable, and commutative function of type r -> r -> a. We want to show that there exists a corresponding implementation of type Commutative r a. We modify the existing implementation as follows.

First, inline all the helper functions used by f, including builtins, and reimplement everything in monadic style. Then, rewrite everything again in CPS style so that we can abort the computation at any time. Also rewrite all pattern-matching to nested if statements, so that all decisions are performed on booleans, and use thunks to delay any observation of the two arguments until one of those boolean decisions. This ensures that all argument observations are boolean observations.

Since f is computable, f obtains its result after observing each of its arguments a finite number of times. Uniformly replace all those observations, regardless of the argument observed, by a call to distinguishBy. If the observations agree, continue with the observed value; it doesn't matter which argument was observed by f, since both arguments have the same observation. If the observations disagree, stop; we have managed to distinguish the two arguments x and y, so we can simply abort the computation and return f x y instead.

If it is the observation on x which returned True, the call to distinguishBy will give us (y, x) instead of (x, y), but by hypothesis, f y x returns the same result as f x y. If we never abort, we also return the same result as f, since all observations were the same as what f would have observed. ∎

Associativity

I am quite proud of my commutativity monad. I wish I could work on an associativity monad next, but none of the insights listed in this post seem to carry over. I am thus in need of new insights. Dear readers, any suggestions?