Themes on Streams

May 9, 2011
> {-# LANGUAGE DeriveFunctor, FlexibleInstances #-}

Recall that a stream is a countably infinite sequence of values:

> data Stream a = a :> Stream a
>   deriving (Functor, Show)
> 
> sHead (a :> _) = a
> sTail (_ :> s) = s

Streams are lovely things (especially in a lazy language) with many nice properties.

> type Theme = String
> type Consciousness = Stream Theme

The remainder of this blog post (in two parts) will be of type Consciousness.

Theme 1: Stream is a monad

The other day I read Jeremy Gibbons’s blog post about the stream monad, proving the monad laws for the version of join that diagonalizes nested streams:

> instance Monad Stream where
>   return a       = a :> return a
>   s >>= f        = sJoin (fmap f s)
> 
> sJoin (s :> ss) = sHead s :> sJoin (fmap sTail ss)

sJoin takes a stream of streams, and outputs a stream with the first element of the first stream, the second element of the second stream, … the nth element of the nth stream.

I recommend reading his post, it’s a very cool example of using universal properties and equational reasoning.

Theme 2: Streams are (isomorphic to) functions

In a comment on Jeremy’s post, Patai Gergely noted that insight into this issue can be gained by observing that Stream a is isomorphic to Nat -> a: there is one item in a stream at every natural number index.

Of course, (->) Nat is a monad: in fact, (->) e is a monad (the "reader monad") for any type e. And what does join for the (->) e monad do? Why, it duplicates an argument:

> rJoin :: (e -> (e -> a)) -> (e -> a)
> rJoin s e = s e e

A little thought shows that this corresponds exactly to the diagonalizing join on Streams: rJoin s e = s e e can be read as "the eth element of rJoin s is the eth element of the eth stream in the stream of streams s." See?

So I told my officemate Daniel about this, and it occurred to us that there’s nothing special here about Nat at all! rJoin is polymorphic in e; R -> a is a monad for any type R.

Functors which are isomorphic to (->) R for some concrete type R are called representable; so what this means is that all representable functors are monads. (Not that we were the first to think of this.)

Theme 3: Streams are comonads

Hmm, but Stream is a comonad too, right?

> class Comonad w where
>   extract   :: w a -> a
>   duplicate :: w a -> w (w a)
> 
> instance Comonad Stream where
>   extract                = sHead
>   duplicate s@(hd :> tl) = s :> duplicate tl

And since Stream is isomorphic to (->) Nat, that type must be a comonad too. What is the corresponding comonad instance for (->) Nat?

> type Nat = Integer   -- just pretend, OK?
> 
> instance Comonad ((->) Nat) where

Extracting from a stream just returns its head element, that is, the element at index 0. So extracting from a Nat -> a applies it to 0.

>   extract = ($0)

Duplicating a stream gives us a stream of streams, where the nth output stream contains consecutive elements from the original stream beginning with the nth. Put another way, the jth element from the ith stream in the output is the (i+j)th element of the original stream:

>   duplicate s i j = s (i + j)

Neat. Unlike the implementation of join for the monad instance, however, this is definitely making use of the particular structure of Nat. So this throws some cold water on our hopes of similarly generalizing this to all representable functors.

…or does it?

Theme 4: Comonads for representable functors

In the previous paragraph I said "this is definitely making use of the particular structure of Nat", but I was being deliberately obtuse. Nat has lots and lots of structure, surely we weren’t using all of it! In fact, we only mentioned the particular natural number 0 and the addition operation. Hmm… zero and addition… what’s interesting about them? Well, zero is the identity for addition, of course, and addition is associative — that is, the natural numbers form a monoid under addition with zero as the identity. So just as a wild guess, perhaps it’s the monoid structure of Nat which makes the comonad instance possible?

In fact… yes! It turns out that comonad structures on R -> a are in one-to-one correspondence with monoid structures on R. To prove this, we can… oh, darn, looks like we’re out of time! (Read: this blog post is getting too long and if I don’t publish something soon I never will.) I’ll continue in another post, but in the meantime you might fancy trying to prove this yourself.


Monoids for Maybe

April 18, 2011

The other day I had two lists of monoidal values that I wanted to combine in a certain way, and I realized it was an instance of this more general pattern:

> {-# LANGUAGE GeneralizedNewtypeDeriving #-}
> import Data.Monoid
> import Control.Applicative
> 
> (<>) :: Monoid m => m -> m -> m
> (<>) = mappend   -- I can't stand writing `mappend`
> 
> newtype AM f m = AM { unAM :: f m }
>   deriving (Functor, Applicative, Show)
> 
> instance (Applicative f, Monoid m) => Monoid (AM f m) where
>   mempty        = pure mempty
>   mappend f1 f2 = mappend <$> f1 <*> f2

It’s not too hard (although a bit fiddly) to show that AM f m satisfies the monoid laws, given that f and m satisfy the applicative functor and monoid laws respectively.

The basic idea here is that the mappend operation for AM f m is just the mappend operation for m, but applied "idiomatically" in the f context. For example, when f = [], this combines two lists of monoidal values by combining all possible pairs:

*Main> map getProduct . unAM $ (AM (map Product [1,2,3]) 
                                <> AM (map Product [1,10,100]))
[1,10,100,2,20,200,3,30,300]

In the #haskell IRC channel someone pointed out to me that Data.Monoid has an instance Monoid m => Monoid (e -> m) which is just a special case of this pattern:

*Main> :m +Data.Ord
*Main Data.Ord> map ((unAM $ AM (comparing length) 
                             <> AM compare) "foo") 
                    ["ba", "bar", "barr"]
[GT,GT,LT]
*Main Data.Ord> map ((comparing length <> compare) "foo") 
                    ["ba", "bar", "barr"]
[GT,GT,LT]

It was also mentioned that the monoid instance for Maybe is also a special case of this pattern:

*Main> AM (Just (Sum 3)) <> AM Nothing
AM {unAM = Nothing}
*Main> Just (Sum 3) <> Nothing
Just (Sum {getSum = 3})

Wait, hold on, what?! It turns out that the default Monoid instance for Maybe is not an instance of this pattern after all! I previously thought there were three different ways of declaring a Monoid instance for Maybe; I now know that there are (at least) four.

  • The default instance defined in Data.Monoid uses Nothing as the identity element, so Nothing represents "no information". It requires a Monoid constraint on the type wrapped by Maybe, although Monoid is slightly too strong, since the type’s own identity element is effectively ignored. In fact, the Data.Monoid documentation states
    Lift a semigroup into Maybe forming a Monoid according to http://en.wikipedia.org/wiki/Monoid: "Any semigroup S may be turned into a monoid simply by adjoining an element e not in S and defining e*e = e and e*s = s = s*e for all s \in S." Since there is no Semigroup type class providing just mappend, we use Monoid instead.

    (Actually, there is (now) a Semigroup type class…)

    *Main> mconcat [Just (Sum 3), Nothing]
    Just (Sum {getSum = 3})
    *Main> mconcat [Just (Sum 3), Nothing, Just (Sum 4), Nothing]
    Just (Sum {getSum = 7})
    
  • The First newtype wrapper in Data.Monoid just takes the first non-Nothing occurrence:

    *Main> mconcat . map First $ [Nothing, Just 3, Nothing, Just 4]
    First {getFirst = Just 3}
    

    This is actually the same as the MonadPlus instance for Maybe, where mplus is used to choose the first non-failing computation:

    *Main Control.Monad> Nothing `mplus` 
                         Just 3 `mplus` 
                         Nothing `mplus` 
                         Just 4
    Just 3
    
  • The Last newtype wrapper is the dual of First, taking the last non-Nothing occurrence:

    *Main> mconcat . map Last $ [Nothing, Just 3, Nothing, Just 4]
    Last {getLast = Just 4}
    
  • The Monoid instance following the Applicative structure of Maybe, however, is distinct from all of these. It combines values wrapped by Just according to their own Monoid instance, but if any occurrences of Nothing are encountered, the result is also Nothing. That is, it corresponds to combining monoidal values in the presence of possible failure, that is, applying mappend idiomatically within the applicative context.

    *Main> mconcat [AM (Just (Sum 3)), AM (Just (Sum 4))]
    AM {unAM = Just (Sum {getSum = 7})}
    *Main> mconcat [AM (Just (Sum 3)), AM (Just (Sum 4)), AM Nothing]
    AM {unAM = Nothing}
    

    As far as I know, this instance is nowhere to be found in the standard libraries. Perhaps a wrapper like AM should be added to Control.Applicative?


Collecting attributes

October 28, 2009

I’m proceeding with the redesign of my diagrams library slowly but surely. I don’t have a lot of time to work on it, hence the “slowly”. But progress is being made. It’s still very much in the design phase, which makes it difficult for others to help, but Lennart has created a diagrams page on the Haskell wiki which I hope can be a good way to have an open design process and get input from the community. There’s a lot of stuff I have written down that I haven’t gotten around to putting on that page yet, but I hope to do that soon.

Occasionally I plan to write some blog posts about interesting issues that arise in the design; today is the first.

Here’s the background: a diagram is essentially a tree of sub-diagrams (although there will be a principled way to refer to subdiagrams in other parts of the tree; more on this in a future post), with leaves corresponding to atomic primitives. Every node in the tree can (optionally) have some associated style attributes, such as stroke width and color, fill color, font, and other such things. When we encounter a primitive at a leaf, how do we know what attributes to use when rendering it? It may have some associated attributes, but its parent node might also have some associated attributes, and other ancestor nodes higher up the tree might have attributes as well.

What we’d really like to do is have a Style data type which has a Monoid instance:

data Style = Style { strokeWidth :: Double
                   , strokeColour :: Colour
                   ... }

instance Monoid Style where
  ...

Then to determine the style to use for a leaf, we just combine the styles of all its ancestors using the monoid.

So, how to implement this Monoid instance? Well, first of all, what I wrote above is slightly bogus; at the very least each particular attribute ought to be optional, so it should look something more like this:

data Style = Style { strokeWidth :: Maybe Double
                   , strokeColour :: Maybe Colour
                   ... }

To combine two Style records, we match them up field-by-field, and Just trumps Nothing.

So far, so good. But how do we combine two fields containing Just? It seems we have two choices: we can be biased towards the top of the tree (i.e. parent attributes override child attributes) or towards the bottom (i.e. child attributes override parent attributes). Indeed, Data.Monoid contains two newtypes, First and Last, whose Monoid instances exhibit exactly this behavior.

But here’s the problem: in this application, one of these choices isn’t obviously better than the other. In fact, it’s easy to imagine situations where each would be the desired behavior. For example, imagine that we have created a subdiagram that we want to use many times throughout a larger diagram. Most of the time it will be blue, so it makes sense to specify that attribute as part of the subdiagram itself. However, in one place we want it to be red, so we’d like to be able to override its attributes with parent attributes. On the other hand, imagine a situation where a diagram is going to be composed of many different subdiagrams, which all share the property that they are blue. To avoid repeating ourselves, it makes sense to specify “blueness” as an attribute of the parent diagram and have all the subdiagrams inherit it. However, one subdiagram should be red, so we’d like to be able to override the parent attribute in this particular child.

What to do? A first cut might look something like this:

data Override a = Default | OverrideUp a | OverrideDown a

data Style = Style { strokeWidth :: Override Double
                   , strokeColour :: Override Colour
                   ... }

The intention is that OverrideUp a overrides any attributes above/before it, and OverrideDown a overrides any attributes below/after it. However, there’s a problem: what should

(OverrideDown a) `mappend` (OverrideUp b)

be? The OverrideDown a claims to override the OverrideUp b… and vice versa! So this doesn’t really work. We need a way to specify relative priorities. So, another solution would just be to assign each attribute with a priority:

data Prioritized a = Default | Priority Double a

data Style = Style { strokeWidth :: Prioritized Double
                   , strokeColour :: Prioritized Colour
                   ... }

For the Monoid instance, we just take the value with maximum priority. This allows us to do what we wanted—overriding parent or child attributes is done simply by assigning a higher priority. However, I really dislike this solution. Having to specify a priority is annoying—but not only that, figuring out what priority to use to achieve your desired effect requires global knowledge about the value of the priorities used elsewhere. One improvement we could make is to adopt the solution used by CSS: attributes are leaf-biased by default, but assigning a priority can override this. That is,

data Prioritized a = Default | Priority (Maybe Double) a

where the Monoid instance chooses the value with the highest priority, or the right/leaf-most value if no priorities are specified. This might be the best option—but it’s still somewhat unsatisfactory.

I wonder about a solution that allows you to say, “I want to override the attribute on THAT node”—where “THAT” represents some way to refer to a particular node by name (what these names look like will be the subject of another post). This might solve the problem of arbitrariness with the numerical priorities, but might also be veering into the realm of the overengineered…


Collecting unstructured information with the monoid of partial knowledge

April 17, 2008

In my last post, I described what I’m calling the “monoid of partial knowledge”, a way of creating a monoid over sets of elements from a preorder, which is a generalization of the familiar monoid (S,\max) over a set with a total order and a smallest element.

There’s actually one situation where a special case of this monoid is commonly used in Haskell. Suppose you have a record type which contains several fields, and you would like to parse some input to create a value of this type. The problem is that the input is not very nice: the bits of input which designate values for various fields are not in any particular order; some occur more than once; some might even be missing. How to deal with this?

One common solution is to wrap the type of each field in the record with Maybe, and create a Monoid instance which allows you to combine two partial records into one (hopefully less partial) record. Using this framework, you can just parse each bit of input into a mostly-blank record, with one (or more) fields filled in, then combine all the records (with mconcat) into one summary record. For example:

import Data.Monoid
import Control.Monad  -- for the MonadPlus instance of Maybe

data Record = R { name  :: Maybe String,
                  age   :: Maybe Int }
  deriving (Eq, Show)

instance Monoid Record where
  mempty = R Nothing Nothing
  mappend r1 r2 = R { name = name r1 `mplus` name r2
                    , age  = age r1  `mplus` age r2
                    }

The mplus function, from the MonadPlus instance for Maybe, simply takes the first Just value that it finds. This is nice and simple, and works just great:

> mempty :: Record
R {name = Nothing, age = Nothing}
> mconcat [mempty { name = Just "Brent" }]
R {name = Just "Brent", age = Nothing}
> mconcat [mempty { name = Just "Brent" }, mempty { age = Just 26 }]
R {name = Just "Brent", age = Just 26}
> mconcat [mempty { name = Just "Brent" }, mempty { age = Just 26 }, mempty { age = Just 23 }]
R {name = Just "Brent", age = Just 26}

Note how the appending is left-biased, because mplus is left-biased: after seeing the first age, all subsequent ages are ignored.

Now, really what we’re doing here is using the monoid (as in my previous post) induced by the preorder which says that any name is \lesssim any other name, and any age is \lesssim any other age, and names and ages can’t be compared!

Some code is in order. First, we create a class for preorders, and a newtype to contain sets of elements (there’s already a Monoid instance for Set, so we need a newtype to give a different semantics). Then we translate the specification from my previous post directly into a Monoid instance.

import qualified Data.Set as S

-- laws:
-- if x == y, then x <~ y
-- if x <~ y  and y <~ z, then x <~ z
class (Eq p) => Preorder p where
  (<~) :: p -> p -> Bool

newtype PStar p = PStar { unPStar :: (S.Set p) }
  deriving Show

instance (Preorder p, Ord p) => Monoid (PStar p) where
  mempty      = PStar S.empty
  mappend (PStar ss) (PStar ts) = PStar $
    S.filter (\s -> all (\t -> s == t || t <~ s || not (s <~ t)) $ S.toList ts) ss
    `S.union`
    S.filter (\t -> all (\s -> s == t || not (t <~ s)) $ S.toList ss) ts

Pretty straightforward! Of course, there are probably more efficient ways to do this, but I don’t care about that at the moment: let’s get some working proof-of-concept code, and worry about efficiency later. Now, one thing you may notice is that our Monoid instance requires an Ord instance for p! “But I thought we only needed a preorder?” I hear you cry. Well, the Ord is just there so that we can use an efficient implementation of Set. In particular, note that the Ord instance need have nothing at all to do with the Preorder instance, and won’t affect the semantics of this Monoid instance in any way. If we wanted, we could do away with the Ord entirely and use lists of unique elements (or something like that) instead of Sets.

So, how do we translate our record example from above into this new framework? Easy, we just create a data type to represent the different kinds of facts we want to represent, along with a convenience method or two, and make it an instance of Preorder:

data Fact = Name String | Age Int
  deriving (Eq,Show,Ord)

fact :: Fact -> PStar Fact
fact f = PStar (S.singleton f)

instance Preorder Fact where
  (Name _) <~ (Name _) = True
  (Age _)  <~ (Age _)  = True
  _        <~ _        = False

Let’s try it!

> mempty :: PStar Fact
PStar {unPStar = fromList []}
> mconcat . map fact $ [Name "Brent"]
PStar {unPStar = fromList [Name "Brent"]}
> mconcat . map fact $ [Name "Brent", Age 26]
PStar {unPStar = fromList [Name "Brent",Age 26]}
> mconcat . map fact $ [Name "Brent", Age 26, Age 23]
PStar {unPStar = fromList [Name "Brent",Age 26]}

Neato! But the really cool thing is all the extra power we get now: we can easily tweak the semantics of the Monoid instance by altering the Preorder instance. For example, suppose we want the first name that we see, but the oldest age. Easy peasy:

instance Preorder Fact where
  (Name _) <~ (Name _) = True
  (Age m)  <~ (Age n)  = m <= n
  _        <~ _        = False

> mconcat . map fact $ [Age 23, Name "Brent"]
PStar {unPStar = fromList [Name "Brent",Age 23]}
> mconcat . map fact $ [Age 23, Name "Brent", Age 24]
PStar {unPStar = fromList [Name "Brent",Age 24]}
> mconcat . map fact $ [Age 23, Name "Brent", Age 24, Name "Joe", Age 26]
PStar {unPStar = fromList [Name "Brent",Age 26]}

Of course, we could have done this with the Record model, but it wouldn’t be terribly elegant. But we’re not done: let’s say we want to remember the oldest age we find, and the first name, unless the age is over 50, in which case we don’t want to remember the name (I admit this is a bit contrived)? That’s not too hard either:

instance Preorder Fact where
  (Name _) <~ (Name _) = True
  (Age m)  <~ (Age n)  = m <= n
  (Name _) <~ (Age n)  = n > 50
  _        <~ _        = False

> mconcat . map fact $ [Name "Brent", Age 26]
PStar {unPStar = fromList [Name "Brent",Age 26]}
> mconcat . map fact $ [Name "Brent", Age 26, Age 45]
PStar {unPStar = fromList [Name "Brent",Age 45]}
> mconcat . map fact $ [Name "Brent", Age 26, Age 45, Age 53]
PStar {unPStar = fromList [Age 53]}

This would have been a huge pain to do with the Record model! Now, this isn’t an unqualified improvement; there are several things we can’t do here. One is if we want to be able to combine facts into larger compound facts: we can do that fairly straightforwardly with the Record-of-Maybes model, but not with the preorder-monoid model. We also can’t easily choose to have some fields be left-biased and some right-biased (the Monoid instance for PStar has left-bias built in!). But it’s certainly an interesting approach.

Now, one thing we do have to be careful of is that our Preorder instances really do define a preorder! For example, at first I tried using n < 18 in the above Preorder instance instead of n > 50, and was confused by the weird results I got. But such a Preorder instance violates transitivity, so no wonder I was getting weird semantics. =) It would be interesting to reformulate this in a dependently typed language like Agda, where creating a Preorder could actually require a proof that it satisfied the preorder axioms.

Thanks to Conal Elliott for some suggestions on making the formulation in the previous post more elegant — we’ll see what comes of it!


An interesting monoid

April 17, 2008

The other day I was just sort of letting my mind wander, and I came up with an interesting monoid, which I’m calling the “monoid of partial knowledge”. So I thought I’d write about it here, partly just because it’s interesting, and partly to see whether anyone has any pointers to any literature (I’m sure I’m not the first to come up with it).

Recall that a monoid is a set with an associative binary operation and a distinguished element which is the identity for the operation.

Now, given a total order on a set S with a smallest element e, we get a monoid (S, \max), where \max denotes the function which determines the larger of two elements, according to the total order on S. \max is clearly associative, and has identity e. Taking a list of elements of S and summarizing it via this monoid corresponds to finding the maximum element in the list. If you think of receiving the elements of the list one by one, and applying \max to each new incoming value and the value of an accumulator (storing the result back into the accumulator, which should obviously be initialized to e), at any given time the value of the accumulator represents the ‘current best’, i.e. the largest element among those received so far.

The idea I had was to generalize this from a total order to a preorder. Recall that a preorder is a set S equipped with a reflexive, transitive binary relation, often denoted \lesssim. That is, for any x,y,z \in S, we have x \lesssim x; and x \lesssim y \land y \lesssim z implies x \lesssim z. If \lesssim is also antisymmetric, that is, x \lesssim y \land y \lesssim x implies x = y, it is called a partial order, or poset. Then if x \lesssim y or y \lesssim x for any two elements x and y, we get a total order, but for a general preorder some pairs of elements may not be comparable — that is, there may be elements x and y for which neither x \lesssim y nor y \lesssim x holds.

Let’s think about this. Suppose we are given a preorder (P,\lesssim) with an initial object e (an initial object in this context is an element which is \lesssim all other elements). We’ll initialize an accumulator to e, and imagine receiving elements of P one at a time. For a concrete example, suppose we are dealing with the preorder (actually also a poset) of positive integers under the divisibility relation, so our accumulator is initialized to 1. Let’s say we receive the integer 4. Clearly, 1 divides 4, so we should replace the 1 in our accumulator with 4. But now suppose we next receive the integer 5. 4 does not divide 5 or vice versa, so what should we do? We would be justified in neither throwing the 5 away nor replacing the 4, since 4 and 5 are not related to each other under the divisibility relation. Somehow we need to keep the 4 and the 5 around.

The solution is that instead of creating a monoid over P itself, as we can for sets with a total order, we create a monoid over subsets of P. In particular, consider the set P_* of subsets of P which do not contain two distinct elements x,y for which x \lesssim y. Since we are dealing with subsets of P, we can actually drop the restriction that P contain an initial object; the empty set will serve as the identity for the monoid.

We then define the monoid operation \oplus on two such subsets as

S \oplus T = (S \triangleleft T) \cup (S \triangleright T)

where

S \triangleleft T = \{ s \in S \mid \forall t \in T, s = t \mbox{ or } t \lesssim s \mbox{ or } s \not \lesssim t \}

and

S \triangleright T = \{ t \in T \mid \forall s \in S, s = t \mbox{ or } t \not \lesssim s \}.

In words, we combine subsets S and T by forming the set of objects from S \cup T which are not \lesssim any others, with the exception of objects s \in S, t \in T where both s \lesssim t and t \lesssim s; in this case we keep s but not t. This introduces a “left bias” to \oplus; there is also an equally valid version with right bias (in particular, S \oplus' T = (T \triangleleft S) \cup (T \triangleright S)).

Now, let’s show that this really does define a valid monoid. First, we need to show that \oplus is closed over P_*. Suppose S, T \in P_*. Suppose also that x,y \in S \oplus T are distinct elements of P with x \lesssim y; we’ll derive a contradiction. First, we cannot have x,y \in S or x,y \in T by definition of P_*. Now suppose x \in T, y \in S. The fact that x \in S \oplus T together with the definition of S \triangleright T imply that we must have x \not \lesssim y, a contradiction. Finally, suppose x \in S, y \in T. Again, by the definition of S \triangleright T we must have y \not \lesssim x. But then the fact that x \in S \oplus T, together with the definition of S \triangleleft T and the facts that x \neq y and y \not \lesssim x imply that x \not \lesssim y, a contradiction again. Hence S \oplus T contains no such pair of elements.

The fact that the empty set \varnothing is the identity for \oplus is clear. (Incidentally, this is why we require that none of the sets in P_* contain two distinct elements with one \lesssim the other: if S were such a set, we would have \varnothing \oplus S \neq S.) I leave the associativity of \oplus as an exercise for the reader (translation: this post is already getting long, the associativity of \oplus seems intuitively obvious to me, and I don’t feel like formalizing it at the moment — perhaps I’ll try writing it up later). I also leave as an interesting exercise the following theorem: if S, T \in P_* are both finite and nonempty, then S \oplus T is also finite and nonempty.

In our example from before, we could now begin with \{1\} in our accumulator. After receiving the singleton set \{4\}, our accumulator would have that singleton set as its new value. Upon receiving \{5\}, our accumulator would become \{4,5\}. Receiving \{10\} would result in \{4,10\} (5 divides 10, so the 5 is discarded); if we later received \{20\}, we would simply have \{20\} in our accumulator (both 4 and 10 divide 20).

I like to think of this as the monoid of partial knowledge. If we consider P to be a set of facts or beliefs, some better (more reliable, useful, correct, complete, etc.) than others, then elements of P_* correspond to possible sets of beliefs. \oplus describes how a set of beliefs changes upon encountering a new set of facts; some of the new facts may supersede and replace old ones, some may not impart any new information, and some may be completely new facts that aren’t related to any currently known.

Now, why can this be thought of as a generalization of the monoid (P, \max) on a totally ordered set? Well, look what happens when we replace P in the definitions above with a totally ordered set with relation \leq: first of all, the restriction on P_* (no two elements of a set in P_* should be related by \leq) means that P_* contains only the empty set and singleton sets, so (ignoring the empty set) P_* is isomorphic to P. Now look at the definition of S \triangleleft T, with \lesssim replaced by \leq (and \not \lesssim replaced by >):

S \triangleleft T = \{ s \in S \mid \forall t \in T, s = t \mbox{ or } t \leq s \mbox{ or } s > t \}

But s = t and s > t are both subsumed by t \leq s, so we can rewrite this as

\{s\} \triangleleft \{t\} = \{s\} \mbox{ if } s \geq t, \mbox{ or } \varnothing \mbox{ otherwise }.

An analysis of \triangleright is similar, and it is clear that \{s\} \oplus \{t\} = \{\max(s,t)\}.

I note in passing that although it might appear shady that I swept that “ignoring the empty set” bit under the rug, everything really does check out: technically, to see a direct generalization of (P,\max) to (P_*, \oplus), we can require that P have an initial object and that P_* contains only finite, nonempty sets. Then it requires a bit more work to prove that \oplus is closed, but it still goes through. I used the formulation I did since it seems more general and requires less proving.

Anyway, this ended up being longer than I originally anticipated (why does that always happen!? =), so I’ll stop here for now, but next time I’ll give some actual Haskell code (which I think ends up being pretty neat!), and talk about one relatively common design pattern which is actually a special case of this monoid.


Follow

Get every new post delivered to your Inbox.