Home

Lawvere Theories and Monads

Martin Hyland and John Power (2007). The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads. ENTCS 172:437-458.

Both monads and Lawvere theories provide characterisations of algebraic structure, with monads providing the more general characterisation. The authors provide an introduction to Lawvere theories, discusses their relationship to sets, and why monads became the more popular treatment.

Then they tackle the application of the theory to the semantics of side effects, where they argue that the generality of monads allow them to characterise computational phenomena that are not to do with side effects such as partiality and continuations, and argue that Lawvere theories more cleanly characterise what side effects are.

This paper is a good introduction to an important line of recent research done by Hyland&Power; cf. also the LtU story Combining computational effects.

By Charles Stewart at 2009-03-13 12:50 | Category Theory | other blogs | 27157 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Speculations

At the end of the paper, the authors make speculations about how the semantics of computation might develop if it explores other characterisations of algebras:

  • Perhaps computational effects might be seen as an instance and development of
    universal algebra? Continuations would not be regarded as a computational effect
    but rather as a distinct notion. It would still have its own body of theory, and
    one would still study the relationship between it and computational effects; but
    perhaps it would not be regarded as a computational effect?

  • Monads appear quite directly in the study of continuations. So perhaps the notion
    of monad might be seen as a generalised semantics of continuations? With the
    unit and counit being regarded as generalised forms of thunk and force?

  • Perhaps the construction sending a Lawvere theory L to the monad TL might be
    seen as providing mathematical support to a CPS -transform? One could give se-
    mantics for the λc-calculus and the computational meta-language that look quite
    different to each other, the former in terms of closed Freyd-categories,
    and the latter in terms of monads. One might focus on the first-order fragment
    of the λc-calculus: Lawvere theories immediately provide models, and one can
    readily produce a sound and complete class of them.

I was led to wonder if the notion of monad can be factorised, so that the side-effectful part is captured by a Lawvere theory, and the part dealing with non-side-effectful computational effects is captured by a non-side-effectful monad. There's an issue: the transformation from the paper of Lawvere theories into monads only gives rise to a monad over Set, so considered as an inverse, this factorisation would be over the same base category. But maybe the question is interesting; the authors raise the question of other base theories.

Postscript — naasking picks up on this point in the story on Conal Elliott's Can functional programming be liberated from the von Neumann paradigm?

By Charles Stewart at Fri, 2009-03-13 13:04 | login or register to post comments

Woah.

This really is a fascinating paper, although most of it went straight over my head. I can definitely agree with the second conclusion/speculation that you mention, although I'd tend to turn it around. I'd say, in a somewhat more precise but mostly hand-waving way, that monads enable a representation-independent way of working with continuations.

Certainly, monads and continuations are in some sense equivalent concepts, although I personally found monads much easier to grasp at first, because they have simpler examples.

I'll see if I can't work through this paper in reverse order, starting with section 6 and then proceeding to the earlier sections. Are you aware of a gentler introduction to Lawvere Theories, starting with nice, well motivated, concrete examples, and then building up to Lawvere categories?

By Leon P Smith at Sun, 2009-03-22 16:42 | login or register to post comments

Gentility and impurity

I can't, off the top of my head, think of a gentle introduction to Lawvere theories, even less one that is online. I'm pretty sure the article I linked to is the easiest explanation of the link between these theories and monads. I'll look about a bit. It maybe that the easiest, if least reliable, way to get your elementary introduction would be to seed a Wikipedia article on the subject and wait.

To spell out more forcefully why I think this theory is important, I think it could lead to a better way of handling impure computation than what Haskell now has. By separating out elementary impurity, such as sequential state and sequential IO, and realising them in terms of Lawvere theories, we might obtain a representation which is much more amenable to transformation and being reasoned about. Hyland & Power say that continuations need the full power of monads; I guess also that facilities for impure computations that need some kind of coordination, such as concurrency and STM monads, also need this power.

By Charles Stewart at Mon, 2009-03-23 09:10 | login or register to post comments

A jumping-off point for Lawvere theories

nLab, the category theorist's community resource, has an article, Lawvere theory. You can get through most of it with knowledge of what cartesian categories and product-preserving functors are, and what the category of groups is.

Is this enough background for the Hyland&Power paper?

By Charles Stewart at Wed, 2010-03-31 09:10 | login or register to post comments

Monads and Continuations

Certainly, monads and continuations are in some sense equivalent concepts

I am no longer sure of the truth or falsity of this assertion. I recently wrote why in a post entitled Are continuations really the mother of all monads?

By Leon P Smith at Tue, 2009-12-22 20:00 | login or register to post comments

The counit of a monad...

Is not, I assume, the counit of the adjunction forming the monad? It is something that may exist if the monad has algebras at every type?

By Jason Dusek at Sun, 2009-11-29 00:35 | login or register to post comments

Right

There may be many possible adjunctions corresponding to a given monad construction: here they are interested in the adjunction over the Kleisli category. I think it was Hayo Thielecke who first called the unit and counit of this adjunction thunk and force: cf. Thielecke, 1997, Continuation Semantics and Self-Adjointness.

Thielecke calls the calls the internal calculus of the Kleisli category of Moggi's computational lambda-calculus, the CPS calculus. It is essentially the same thing as the Lafont/Streicher/Reus calculus for expressing implication by means of negation: cf. my refs in the Lectures on the Curry-Howard Isomorphism story.

By Charles Stewart at Tue, 2009-12-01 11:16 | login or register to post comments