- About Scala
- Documentation
- Code Examples
- Software
- Scala Developers

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

Thu, 2011-06-23, 14:32

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

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

Thu, 2011-06-23, 19:27

#2
Re: Separation of concerns: the MonadAPI, Conway Games and the

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>

--

Sébastien

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>

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

Thu, 2011-06-23, 19:37

#3
Re: Separation of concerns: the MonadAPI, Conway Games and the

If you are interested in Conway games and data types, maybe you are also interested in how to formalize them in Higher-Order Logic and the issues that come up with that. My paper about that can be found at http://www.springerlink.com/content/37u2588512145n23/ . Also includes a "bug" in a proof in Conways book "On Numbers and Games". I think a version of the paper can be found online for free by googling ;-)

- Steven

On 23.06.2011, at 15:32, Meredith Gregory wrote:

- Steven

On 23.06.2011, at 15:32, Meredith Gregory wrote:

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

Thu, 2011-06-23, 19:57

#4
Re: Separation of concerns: the MonadAPI, Conway Games and the

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

Best wishes,

--greg

On Thu, Jun 23, 2011 at 11:34 AM, Steven Obua <steven [dot] obua [at] googlemail [dot] com> wrote:

--

L.G. Meredith

Managing Partner

Biosimilarity LLC

7329 39th Ave SWSeattle, WA 98136

+1 206.650.3740

http://biosimilarity.blogspot.com

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

Best wishes,

--greg

On Thu, Jun 23, 2011 at 11:34 AM, Steven Obua <steven [dot] obua [at] googlemail [dot] com> wrote:

If you are interested in Conway games and data types, maybe you are also interested in how to formalize them in Higher-Order Logic and the issues that come up with that. My paper about that can be found at http://www.springerlink.com/content/37u2588512145n23/ . Also includes a "bug" in a proof in Conways book "On Numbers and Games". I think a version of the paper can be found online for free by googling ;-)

- Steven

On 23.06.2011, at 15:32, Meredith Gregory wrote:

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

--

L.G. Meredith

Managing Partner

Biosimilarity LLC

7329 39th Ave SWSeattle, WA 98136

+1 206.650.3740

http://biosimilarity.blogspot.com

Thu, 2011-06-23, 19:57

#5
Re: Separation of concerns: the MonadAPI, Conway Games and the

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

Best wishes,

--greg

On Thu, Jun 23, 2011 at 11:34 AM, Steven Obua <steven [dot] obua [at] googlemail [dot] com> wrote:

--

L.G. Meredith

Managing Partner

Biosimilarity LLC

7329 39th Ave SWSeattle, WA 98136

+1 206.650.3740

http://biosimilarity.blogspot.com

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

Best wishes,

--greg

On Thu, Jun 23, 2011 at 11:34 AM, Steven Obua <steven [dot] obua [at] googlemail [dot] com> wrote:

If you are interested in Conway games and data types, maybe you are also interested in how to formalize them in Higher-Order Logic and the issues that come up with that. My paper about that can be found at http://www.springerlink.com/content/37u2588512145n23/ . Also includes a "bug" in a proof in Conways book "On Numbers and Games". I think a version of the paper can be found online for free by googling ;-)

- Steven

On 23.06.2011, at 15:32, Meredith Gregory wrote:

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

--

L.G. Meredith

Managing Partner

Biosimilarity LLC

7329 39th Ave SWSeattle, WA 98136

+1 206.650.3740

http://biosimilarity.blogspot.com

Thu, 2011-06-23, 20:07

#6
Re: Separation of concerns: the MonadAPI, Conway Games and the

Dear Sebastien,

i really, really should make more of an effort to include scalaz samples. Thanks for the suggestion!

Best wishes,

--greg

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

--

L.G. Meredith

Managing Partner

Biosimilarity LLC

7329 39th Ave SWSeattle, WA 98136

+1 206.650.3740

http://biosimilarity.blogspot.com

i really, really should make more of an effort to include scalaz samples. Thanks for the suggestion!

Best wishes,

--greg

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

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>

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

--

L.G. Meredith

Managing Partner

Biosimilarity LLC

7329 39th Ave SWSeattle, WA 98136

+1 206.650.3740

http://biosimilarity.blogspot.com

Thu, 2011-06-23, 21:07

#7
Re: Separation of concerns: the MonadAPI, Conway Games and the

On 23.06.2011, at 20:49, Meredith Gregory wrote:

Dear Steven,I think this could be done by a) extending HOLZF to HOLZF[A] by treating A as urelements in set theoryb) proceeding as in the paper (first define fixgames, and so on)

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

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?

- 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

I have no idea :-) Did you manage to construct the above monadic type in Agda?

- Steven

Thu, 2011-06-23, 21:17

#8
Re: Separation of concerns: the MonadAPI, Conway Games and the

Dear Steven,

Interesting! Your first comment corresponds exactly with my intuitions. Regarding Agda, i've not engaged it in earnest, yet. It just seemed like it might be the right sort of tool.

Best wishes,

--greg

On Thu, Jun 23, 2011 at 12:57 PM, Steven Obua <steven [dot] obua [at] googlemail [dot] com> wrote:

--

L.G. Meredith

Managing Partner

Biosimilarity LLC

7329 39th Ave SWSeattle, WA 98136

+1 206.650.3740

http://biosimilarity.blogspot.com

Interesting! Your first comment corresponds exactly with my intuitions. Regarding Agda, i've not engaged it in earnest, yet. It just seemed like it might be the right sort of tool.

Best wishes,

--greg

On Thu, Jun 23, 2011 at 12:57 PM, Steven Obua <steven [dot] obua [at] googlemail [dot] com> wrote:

On 23.06.2011, at 20:49, Meredith Gregory wrote:Dear Steven,I think this could be done by a) extending HOLZF to HOLZF[A] by treating A as urelements in set theoryb) proceeding as in the paper (first define fixgames, and so on)

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
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?

I have no idea :-) Did you manage to construct the above monadic type in Agda?

- Steven

--

L.G. Meredith

Managing Partner

Biosimilarity LLC

7329 39th Ave SWSeattle, WA 98136

+1 206.650.3740

http://biosimilarity.blogspot.com

Thu, 2011-06-23, 21:27

#9
Re: Separation of concerns: the MonadAPI, Conway Games and the

Well, it might not be so easy. Writing down these equations is often deceptively simple. Actually solving them might even get you a Turing Award :-)

- Steven

On 23.06.2011, at 22:03, Meredith Gregory wrote:

- Steven

On 23.06.2011, at 22:03, Meredith Gregory wrote:

Dear Steven,

Interesting! Your first comment corresponds exactly with my intuitions. Regarding Agda, i've not engaged it in earnest, yet. It just seemed like it might be the right sort of tool.

Best wishes,

--greg

On Thu, Jun 23, 2011 at 12:57 PM, Steven Obua <steven [dot] obua [at] googlemail [dot] com> wrote:

On 23.06.2011, at 20:49, Meredith Gregory wrote:Dear Steven,I think this could be done by a) extending HOLZF to HOLZF[A] by treating A as urelements in set theoryb) proceeding as in the paper (first define fixgames, and so on)

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
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?

I have no idea :-) Did you manage to construct the above monadic type in Agda?

- Steven

--

L.G. Meredith

Managing Partner

Biosimilarity LLC

7329 39th Ave SWSeattle, WA 98136

+1 206.650.3740

http://biosimilarity.blogspot.com

Fri, 2011-06-24, 09:17

#10
Re: Separation of concerns: the MonadAPI, Conway Games and the

Great post. I think the Coda though (at least the inheritance/variance part) could/should be split out into its own post rather than being at the end of a long post on MonadAPI. It is important enough in its own right.

On 23 June 2011 23:32, Meredith Gregory <lgreg [dot] meredith [at] gmail [dot] com> wrote:

On 23 June 2011 23:32, Meredith Gregory <lgreg [dot] meredith [at] gmail [dot] com> wrote:

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

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

Best wishes,

--greg

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

--

L.G. Meredith

Managing Partner

Biosimilarity LLC

7329 39th Ave SWSeattle, WA 98136

+1 206.650.3740

http://biosimilarity.blogspot.com