# Tag Info

15

First of all: Any monad is also an applicative functor and any applicative functor is a functor. This is true in the context of Haskell, but (reading Applicative as "strong lax monoidal functor") not in general, for the rather trivial reason that you can have "applicative" functors between different monoidal categories, whereas monads (and comonads) are ...

10

The two papers to look at it are Benton, Bierman and de Paiva's Computational Types from a Logical Perspective, which directly gives a proof theory for Moggi's computational lambda-calculus; and Rowan Davies and Frank Pfenning's A Judgmental Reconstruction of Modal Logic, which gives a constructive proof theory for S4 modal logic with box and diamond, and ...

8

In this post on SO I found an interesting answer - decisive functors. If we replace () by Void, (,) by Either and reverse the arrows, we get: class Functor f => Decisive f where nogood :: f Void -> Void orwell :: f (Either s t) -> Either (f s) (f t) The blog post also gives some laws that decisive functors adhere to. And, every Comonad is ...

5

The paper with a rather suggestive title "Algebras, Coalgebras, Monads and Comonads" (2001) by Neil Ghani, Christoph Lüth, Federico De Marchi, John Power addresses this topic.

5

McBride and Patterson (Section 7) show that an applicative functor, also known as an idiom, is a strong lax monoidal functor. You are looking for a strong colax monoidal functor also known as an strong oplax monoidal functor. As mentioned in a comment, an oplax monoidal functor is a lax monoidal functor between the opposite categories, which ends up being a ...

4

I'll add this in addition to Neel Krishnaswami's answer. The article he refers to A Judgemental Reconstruction of Modal Logic cites the article by Satoshi Kobayashi Monad As Modality which I had come across via Abramsky's article Game Semantics for Access Control. (That article then is built on in Game Semantics for Dependent Types to give a foundation for ...

Only top voted, non community-wiki answers of a minimum length are eligible