Motivation
This work began with a desire to construct a simple and easily understandable example to illustrate separating out the monad API from the underlying structure that supports it. In Haskell this division of labor is well understood. The monad API is a type class that takes the constructor for the underlying data type as a parameter. In Scala this separation is less well exposed. The monadic API is organized as a trait (FilterMonadic) and folded into the data constructor type. Thus, Set, following a more OO-style, has these methods on the class. This organization actually gives less reuse, in particular as it comes to conversions between data structures, and the point is to have an example that illustrates this clearly -- while being pretty much immediately understandable and yet interesting and compelling.
The simplest example would be to have duplicate container-like structure, such as a pair of containers serving as components of some larger structure, either of which would serve to support the monadic API for the larger structure. Casting about for a symmetric structure having a container-like capability in each component i readily recognized Conway games as nearly tailor-made for this job. What is a Conway game, you ask, and why do we care about them?
Discussion of Conway games
John Horton Conway, in his inimitably playful style, found a simple data structure that supported or modeled the operations of the field of Real numbers. His data structure, however, not only captured the Reals but also many, many more of the notions of number, quantity and order that had been proposed, including Cantor’s infinities and Robinson’s infinitessimals. Moreover, Conway’s data structure is incredibly simple and easily understood and -- best of all -- has an interpretation as a representation of two-player games! So, just by playing along with Conway we get to organize and gain insight into how numbers work. It also turns out that the game interpretation really has a pay-off in it’s own right. For example, Elwyn Berlekamp, one of Conway’s collaborators, has done an analysis of the game of go, using Conway games, and found powerful new strategies, such as chilling. For a mathematician and computer scientist that’s motivation enough to spend a little time with them.
A Conway game can be thought of as a representation of a game at a given state of play. Specifically, it is really just a pair, the left part of which represents Player’s options, or moves in the game; and, the right part of which represents Opponent’s options, or moves in the game. The beauty of this way of thinking is that it may be used recursively. An option, or move, is just simply a game, i.e. a pair of options for Player and Opponent. By nesting in this way, we can represent all possibly plays of a given game. In Scala code, we might write this idea down as
1 | trait ConwayGame { |
Then we could provide some simple concrete implementations as
1 | case object EmptyGame extends ConwayGame { |
Now, we see that this definition is perfectly well founded. The EmptyGame, also known as 0, is a valid Scala object. It can be passed around as a value and inspected for its left and right components -- which just happen to be empty. Further, we can use our case class, Game, together with 0, to make the Conway game that represents unity, aka 1. We could write this at the Scala REPL prompt with
scala> val one = Game( Set( EmptyGame ), Set.empty )
one: Game = Game(Set(EmptyGame),Set())
Anyone familiar with the von Neumann encoding of the Naturals can see where this is going. (And anyone not will get the gist with the next bit... ) So, we’ll skip ahead, in a bit, and talk about how to model addition. First, though, we should take a look at Conway’s own notation. He writes games like this
G = { GL, … | GR, … }
The notation is much like set (comprehension) notation except that the bar in the middle of braces denotes the separation of the left and right components. The left (respectively, right) components of the game, G, are indexed by GL (respectively, GR). Thus, in Conway’s notation, the empty game, 0, is { | }, and 1 is { { | } | }. Whether you’re a math fanboy (resp, fangrrl) or not, you have to admit this is much more compact than the Scala code. So, we’ll at least write a toString that prints games out like this. (See the github project.)
On to addition! Since this structure -- like the game of go -- is simultaneously incredibly simple and incredibly rich let’s allow for the possibility that there might be multiple ways to define addition. So, rather than encode addition on Games, let’s create a Calculator that provides a notion of addition (and some of the other arithmetic operations). First, we’ll record the operations we expect to show up on the Calculator.
1 | trait ConwayOps { |
And, then we’ll provide a concrete implementation.
1 | class ConwayCalculator |
i feel compelled to offer just a quick observation regarding the fidelity of this code with respect to Conway’s code. While these definitions are nearly verbatim representations of Conway’s original definitions, Conway’s construction is a mathematical construction. So, he is very happy to have infinite left and right components. Because Scala is strict by default, these definitions would have to be modified to be lazy enough to model (some of) the infinite constructions Conway considers. These subtleties, however, are not of primary concern to us, here. Our focus here is to use the essence of the Conway data structure to illustrate a point about monads and design patterns. That said, let’s take a look at addition. Using our calculator, if we add 1 to 0 what do we get?
scala> val one = Game( Set( EmptyGame ), Set.empty )
val one = Game( Set( EmptyGame ), Set.empty )
one: com.biosimilarity.lift.lib.game.conway.Game = {{|}|}
scala> val zero = EmptyGame
val zero = EmptyGame
zero: com.biosimilarity.lift.lib.game.conway.EmptyGame.type = {|}
scala> val calc = new ConwayCalculator()
val calc = new ConwayCalculator()
calc: com.biosimilarity.lift.lib.game.conway.ConwayCalculator = com.biosimilarity.lift.lib.game.conway.ConwayCalculator@4662a3a1
scala> calc.add( one, zero )
calc.add( one, zero )
res0: com.biosimilarity.lift.lib.game.conway.ConwayGame = {{|}|}
scala> calc.add( zero, one )
calc.add( zero, one )
res1: com.biosimilarity.lift.lib.game.conway.ConwayGame = {{|}|}
scala>
This would hardly count as a mathematical proof of the correctness of our encoding. However, given that the encoding is a near verbatim representation of Conway’s original definitions, it gives us some confidence that we got it right enough for our main purpose.
Recap of the monad API
For this discussion we use the BMonad version of the monad API. So, if the trait Monad (see below) represents the (signatures) of the standard category theoretic presentation of monads
1 | // How the category boyz be looking at things monadically |
then the trait BMonad (below) represents an alternative presentation (in terms of a method called bind) that is common in the Haskel community.
1 | // How the Haskell boyz be looking at things monadically |
It turns out that we will also need some additional structure on our monad which we encapsulate in the trait MonadPlus. The additional structure allows us to interpret our monad more directly as if it were an additive structure with a +-like operation and an additive identity which we access via the zero method.
1 | // More monadically good richness |
Realizing the monad API
This API separates the monad type constructor from the monad methods. That is, they are not methods on M. They are methods on Monad (respectively, BMonad). This design choice is very much analogous to our choice to model the arithmetic operations on Conway games on a separate Calculator class. In the same way that we might invent different kinds of calculators for different ways to realize arithmetic operations on Conway games (and not perturb our Conway game code!), this affords us the opportunity to model different ways to interpret the monad API on the same underlying structure. To see the monad API at work let’s see how we might interpret the Option structure monadically.
One crucial point about the code below is that when we make this design choice we are swimming upstream relative to choices made in Scala’s basic design. In particular, Scala’s for-notation desugaring makes some strong assumptions about the factorization of the monad methods. To allow our design pattern to play well in the Scala ecosystem (be used in for-comprehensions) we have to provide an adapter (represented here in the inheritance of ForNotationAdapter)
1 | // Option interpreted as a monad |
Discussion of Conway game structure to interpret the monad API
Poking a hole in Conway
As it stands our presentation of the Conway game structure is not sufficient as a target for interpreting the monadic API. The monadic API is parametrically polymorphic in a type of element that can be encapsulated in our container structure. Conway games are purer than that! They are either empty or they contain other Conway games.
The resemblance of Conway games to Sets gives us a clue for how to rectify the situation. In point of fact, Scala Sets do not correspond to ordinary Set Theory! At least not ZF(C) Set Theory. This is because ZF Set Theory sets do not contain elements that aren’t sets! ZF Set Theory is built entirely from the empty set, {}, in the same way that Conway games are built entirely from the empty game, {|}. As programmers -- whether we know it or not! -- we are quite comfortable with the idea of “poking a hole” in ZF Set Theory; that is, making it parametrically polymorphic in an “atom” type, say A, where the type Set[A] can contain either A’s or Set[A]. So, let’s try the same idea here.
We make a new type, say GeneralizedConwayGame[A], that is parametric in a type of “atom”, A.
1 | trait GeneralizedConwayGame[+A] { |
We can go along and carry out the programme providing the obvious variants of our concrete implementations. For example,
1 | case object EmptyGenConGame |
(Here's what we are doing, mathematically. The type of ConwayGames can be seen as
CG = Pow( CG ) x Pow( CG )
The shape of this domain equation tells us that it is solvable. It's solution corresponds precisely to the concrete types we described above. Now, there's another way to arrive at the solution. We make CG parametric.
CG[A] = Pow( A ) x Pow( A )
then we see that µA.CG[A] gives us the original type of Conway Games. Now that we've made CG parametric, nothing stops us from using these type parameters in interesting ways. So, our recursive equation becomes
CG[A] = Pow( CG[A] + A ) x Pow( CG[A] + A )
And, as we mention below, this just begs the formulation
CG[M,A] = M[CG[M,A] + A] x M[CG[M,A] + A]
where we have replaced Pow (the Power set monad) with an arbitrary monad, M. If you look in the github project, you will see that the calculator definitions for this construction remain nearly unchanged. Thus, we have the field of Reals over an arbitrary monad, M.)
But, we hit a snag when it comes to supporting the operations of the Calculator! The definition of minus, for example, will require us to “negate” an inhabitant of the type, A. This is where reification -- which is the very heart of what monads do -- comes to the rescue! We simply invent some (largely syntactic) containers for each of the situations we are required to support and we defer any computational interpretation! It will be up to some richer Calculator together with some more detailed information about the type A to give a more detailed interpretation of these calculations.
You can see one relatively complete presentation of the required structure in the github project. Fortunately for us, because we have deferred any computational interpretation of these operations, and merely reified and recorded that the calculations need to be performed, that these operations type check constitutes the bulk of the proof that this is a reasonable model. This is the essential power of syntactic models. What remains of such a mathematical proof would be a (definition of and) demonstration of the coherence of the interaction of the various elements of the structure we’ve posited. The analogy to keep in mind here is to the monadic API, itself. What remains of correctness obligations, after type checking, are the monad laws. These a programmer must prove, by hand.
i would be remiss if i didn’t say that this approach to generalizing Conway is an entirely new idea! To the best of my knowledge no one was considered generalizing Conway’s construction in quite this way. Moreover, it leads to a second and even more beautiful generalization in which we replace Set as the left and right component containers with an arbitary monad! It turns out that the structure we derive above is sufficient to carry out this generalization as well. That in itself is justification for the introduction of extra structure because it allows us to define field operations that closely resemble the Reals over more or less arbitrary monads (such as the continuation monad). This opens up whole new possibilities! However, they are beyond the scope of the current discussion.
With this structure in hand, it should be clear that there are (at least!) two ways to interpret the monad API using Conway games. The two obvious ways correspond to two different interpretations of the unit method -- one which embeds the element in the left component, the other in the right. Interestingly, for the definition of bind to even type check we are more or less forced to treat the left and right sides symmetrically. So, the substantive difference between the two interpretations is whether unit encapsulates inhabitants of A in the left or right component of a game. In the code below we have recognized this fact by lifting the common code up into a separate trait.
1 | trait GenConPreM[A] { |
This allows us to write fairly simple, straightforward interpretations of the monad API.
1 | class GenConLeftM[A]( ) |
The point is that our Conway code doesn’t change. The underlying structure is rich enough to support two different interpretations of the monad API. So, we merely provide the two distinct witnesses (in Haskell these would be called instance declarations) of the interpretation of the monad API.
Coda
Ironically, as i was preparing the code samples for this post i was initially using List[A] as the container for the left and right options. Of course, it should be something closer to Set[A]. So, as i was cleaning up the code i went to change the container to Set[A]. Much to my surprise i discovered that in the Scala collections library Set[A] and List[A] do not share the same variance constraints. List[A] is covariant while Set[A] is invariant. The more i looked into the issue the more puzzled i became. The reason for this is that Set[A] inherits from A => Boolean. Now, this is only one view of the semantics of Set[A] and is also only one way to provide the capability. It would have been perfectly reasonable to provide a view of Set[A] that enabled this feature. Thus, inheritance, as i mentioned at the outset of this post, really, really did afford less reuse.
The list of places to go wrong with inheritance is pretty well explored from the fragile base class to the synchronization inheritance anomaly. At the core of this issue is that is-a relationships are almost always in context. Inheritance sublimates the context. This is exactly the opposite of what is needed for maximal reuse -- and actually at odds with O-O principles. Instead, reify the context, give it an explicit computational representation and you will get more reuse.
Thus, in the Set vs List case, it's only in some context that we agree that a Set[A] may be interpreted as a function A => Boolean. The context has very specific assumptions about what a function is and what a Set is. If we reify that context, we arrive at something like
trait SetsAreFunctions[A,B] { /* you could make this implicit */ def asFunction( s : Set[A] ) : A => B }
Notice that one "specialization" of this SetsAreFunctions[A,Float] is a candidate for representing fuzzy sets. Another "specialization" SetsAreFunctions[A,Option[Boolean]] is a candidate for various representations of partial functions. In this design our assumptions about the meaning of Set and function have been reified. Further, the act of specialization is much more clear, much more explicit and more highly governed by compiler constraints. If you compare it to what has been frozen into the Scala collections, it has a wider range, is mathematically and computationally more accurate and doesn't introduce an anomalous variance difference between collections that mathematical consistency demands be the same (List comes from the monad of the free monoid, Set is an algebra of this monad guaranteeing idempotency and commutativity of the operation -- variance should not differ!).
There's another reason to care about Conway Games that i'll speak about in a little more depth in a subsequent post. To date, there have been two proposals for a notion of location that generalizes to arbitrary data structures supports well known operations like arithmetic and differential calculus these are -- Conway games and Huet's zipper. At first glance these two ideas do not seem to have much in common. However, once we look at these two proposals through the monadic lens we see that they share a striking commonality.
Posts
No comments:
Post a Comment