This page is no longer maintained — Please continue to the home page at www.scala-lang.org

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

10 replies
Meredith Gregory
Joined: 2008-12-17,
User offline. Last seen 42 years 45 weeks ago.
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
Meredith Gregory
Joined: 2008-12-17,
User offline. Last seen 42 years 45 weeks ago.
Re: Separation of concerns: the MonadAPI, Conway Games and the
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
Sebastien Bocq
Joined: 2008-12-18,
User offline. Last seen 42 years 45 weeks ago.
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>
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
phlegmaticprogrammer
Joined: 2010-07-23,
User offline. Last seen 2 years 15 weeks ago.
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:
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

Meredith Gregory
Joined: 2008-12-17,
User offline. Last seen 42 years 45 weeks ago.
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
  • 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?
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:
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




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

+1 206.650.3740

http://biosimilarity.blogspot.com
Meredith Gregory
Joined: 2008-12-17,
User offline. Last seen 42 years 45 weeks ago.
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
  • 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?
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:
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




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

+1 206.650.3740

http://biosimilarity.blogspot.com
Meredith Gregory
Joined: 2008-12-17,
User offline. Last seen 42 years 45 weeks ago.
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:
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



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

+1 206.650.3740

http://biosimilarity.blogspot.com
phlegmaticprogrammer
Joined: 2010-07-23,
User offline. Last seen 2 years 15 weeks ago.
Re: Separation of concerns: the MonadAPI, Conway Games and the

On 23.06.2011, at 20:49, Meredith Gregory wrote:
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
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)

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

I have no idea :-) Did you manage to construct the above monadic type in Agda?
- Steven
Meredith Gregory
Joined: 2008-12-17,
User offline. Last seen 42 years 45 weeks ago.
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:

On 23.06.2011, at 20:49, Meredith Gregory wrote:
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
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)

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

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
phlegmaticprogrammer
Joined: 2010-07-23,
User offline. Last seen 2 years 15 weeks ago.
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:
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,
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
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)

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

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

Jed Wesley-Smith
Joined: 2011-06-24,
User offline. Last seen 42 years 45 weeks ago.
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:
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

Copyright © 2012 École Polytechnique Fédérale de Lausanne (EPFL), Lausanne, Switzerland