Separation of concerns: the MonadAPI, Conway Games and the Reals over a Monad

Dear Steven,
Sweet! Can you extend your HOL representation to arbitrary monads? In particular, i've been looking for tools to prove things about the following variation of the construction

• CG = Set[CG] x Set[CG] // Conway's original type
• CG[A] = Set[CG[A] + A] x Set[CG[A] + A] // A parametrically polymorphic version of Conway's type

• CG[M,A] = M[CG[M,A] + A] x M[CG[M,A] + A] // A variation of Conway's type with other monads, M, to collect the left and right components

If you assume the existence of certain maps (and some obvious coherence conditions), then Conway's definitions extend smoothly to the type computed in the two variant equations. i wonder how this might look in Agda?

Converting tabs to whitespaces may help, but I'm not an expert either.

I struggled a while with inheritance and monads and it took me a long phase of trials and errors to conclude that the way you present it is the best way to implement monads in Scala. It is nicer for a beginner to have such self-contained overview before jumping straight ahead into something like scalaz. That is the first thing I spotted while scrolling quickly through your post and I mistaken it for an introduction to monads.

Although I barely know category theory, I wish Scala could infer automatically a monad from separate mu, eta and tau type classes. It looks like the ultimate modularity for me and I'm not even sure Haskell can infer that either. I think that is what scalaz folks try to achieve but it requires a lot of implicit magic in Scala and it look very contrived in the end. This might discourage newcomers from digging further into these wonderful abstractions. For example, the usage of a monad transformer still eludes me (don't worry, I'll look it up by myself) but I think I would be better off grokking the concept in Haskell than in Scalaz.

By the way, is there any reason why you decided to avoid scalaz besides gaining a better understanding on how to implement monads from scratch in Scala?

Sebastien

2011/6/23 Meredith Gregory <lgreg [dot] meredith [at] gmail [dot] com>

Dear Sebastien,
Thanks for the feedback! Indeed, there does seem to be some weird interaction between the blogspot template and the css stylesheets i use for source code. The html looks fine in standalone mode, but goes wonky in blogspot. i'm not expert enough in css to sort this out in a timely fashion. You can get a better view of code in github.
If it comes across as an introduction to monads, then i've failed as a writer! It actually assumes quite a bit of knowledge about monads and illustrates some key points

• typeclass style interfaces are better than inheritance, if reuse is your goal;
• more excitingly (for me, anyway), the Conway construction can be generalized to work over a very wide class of monads -- meaning we can have the structure of the Reals over a very wide class of data structure. That's fantastic news!

Best wishes,
--greg

On Thu, Jun 23, 2011 at 7:06 AM, Sébastien Bocq <sebastien [dot] bocq [at] gmail [dot] com> wrote:

Dear Meredith,

There is a problem with the indentation which makes the code samples difficult to read. I haven't read your post fully yet but at first glance it looks like a very understandable introduction to monads.

Kind regards,
Sebastien

2011/6/23 Meredith Gregory <lgreg [dot] meredith [at] gmail [dot] com>

Dear Scalarazzi,
i've a new blog post up. It's still a bit drafty (brrrrr!), but it's getting there. Comments welcome.
Best wishes,
--greg

--
L.G. Meredith
Managing Partner
Biosimilarity LLC
7329 39th Ave SWSeattle, WA 98136

+1 206.650.3740

http://biosimilarity.blogspot.com

--
Sébastien

--
L.G. Meredith
Managing Partner
Biosimilarity LLC
7329 39th Ave SWSeattle, WA 98136

+1 206.650.3740

http://biosimilarity.blogspot.com

--
Sébastien