Home

Arrows generalise monads and idioms

Two fresh papers from the Edinburgh theory stable:
  • Lindley, Wadler & Yallop, 2008. The Arrow Calculus, (Functional Pearl) (submitted to ICFP).
  • Lindley, Wadler & Yallop, 2008. Idioms are oblivious, arrows are meticulous, monads are promiscuous (submitted to MSFP)
    We revisit the connection between three notions of computation: Moggi’s monads, Hughes’s arrows and McBride and Paterson’s idioms (also called applicative functors ). We show that idioms are equivalent to arrows that satisfy the type isomorphism A ∼> B ≅ 1 ∼> (A -> B) and that monads are equivalent to arrows that satisfy the type isomorphism A ∼> B ≅A → (1 ∼> B). Further, idioms embed into arrows and arrows embed into monads.
The first paper introduce a reformulation of the Power/Thielecke/Paterson/McBride axiomatisation of arrows, which the authors argue is more natural, and shows that arrows generalise both monads and idioms. The second paper studies the relationships between the three formalisations in more formal depth; in particular the results about applicative functors struck me as significant.
By Charles Stewart at 2008-05-05 12:41 | Category Theory | other blogs | 26437 reads

Comment viewing options

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

And monotremes are oviparous

... and their ova meroblastic. :-)

By johnwcowan at Mon, 2008-05-05 13:26 | login or register to post comments

interesting observation

The second paper basically says, by adding new combinators and extra laws, one can either make Arrow more expressive (to become Monad) or less (to become Applicative Functor aka Idiom).

This is an interesting observation because conventional thinking is that more laws to satisfy brings more power (hence the claim in McBride and Paterson's paper). Apparently this is not always true.

By ninegua at Mon, 2008-05-05 16:23 | login or register to post comments

Constructors and laws

Right. It seems reasonable to define the expressivity of a theory in terms of the set of distinct programs that it contains.

Adding additional term constructors increases the number of programs in the theory, while adding additional equations (laws) decreases the number of distinct programs. Adding both constructors and equations can result in something either more or less expressive than the original theory.

By Jeremy at Mon, 2008-05-05 19:08 | login or register to post comments

Thanks for the interest in

Thanks for the interest in our work, but the post is slightly misleading.

The first paper gives a reformulation of Hughes's arrows using a calculus whose syntax is close to Paterson's (and GHC's) syntactic sugar.

I guess the reference to Power and Thielecke is regarding their work on Freyd categories. The implication in our introduction that Freyd categories are the same as arrows is a mistake. Bob Atkey has recently shown that this widely-held belief is false (arrows generalise Freyd categories).

The first paper does not deal with the relationship between idioms, arrows and monads. That's what the second paper does.

Finally, I don't think either of these papers fits under the heading 'Category Theory' — 'Lambda Calculus', 'Type Theory' or 'Semantics' would seem more appropriate. For a categorical approach see Bob's work.

By Sam Lindley at Mon, 2008-05-05 18:48 | login or register to post comments

Two counter clarifications

Thanks for the clarifications, and especially for the pointer to Atkey's paper, which I had not seen.

Two points about the story. First, I planned only to announce the second paper, until I realised it was kinder to allow LtUers to read the first paper first. The abstract I posted is the main news, and came from the second paper, but treats the formalisation of the first paper, and benefits from being read in its light. I apologise if my post was unclear due to my not making this clear.

Second, about which "department": IMO the headings there should not be read as if they were part of the Mathematics Subject Classification, but rather serve the purpose of grouping similar stories together. Past stories relating monads to arrows have gone in the "Category theory" department (eg. Combining computational effects, and Arrows, like Monads, are Monoids, about the paper that Atkey criticises); this is sometimes synchronically dubious, but from the view of LtU history makes sense.

By Charles Stewart at Wed, 2008-05-07 14:06 | login or register to post comments

A little more than syntax

but also the same types and semantics as a subset of the language described in my 2001 paper A New Notation for Arrows and implemented in GHC in 2003. The "arrow calculus" paper spells out the type rules (sketched in the Notation paper and implemented in GHC) for the subset, states beta and eta laws, and proves an adequacy result. It uses a variant syntax for application commands, but expressed in the original syntax the beta and eta laws come out simpler and closer to the lambda-calculus:

(beta)  (proc x -> Q) -< y  =  Q[x := y]
(eta)   proc x -> (f -< x)  =  f

and the language divides into two more or less independent fragments: abstraction/application and let/return.

I was somewhat surprised that the second paper did not even cite my work in this area.

By Ross Paterson at Sun, 2008-05-18 12:34 | login or register to post comments