# Tag Info

16

There have been a number of developments with regards to the use of monads in the theory of computation since Eugenio Moggi's work. I am not able to give a comprehensive account, but here are some points that I am familiar with, others can chime in with their answers. Specific examples of monads You do not have to study super-general theory all the time. ...

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

10

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

8

8

The definition of morphism of adjunctions may be found in MacLane's book. Let $F:\mathcal C\rightarrow\mathcal D$, $G:\mathcal D\rightarrow\mathcal C$, $F':\mathcal C'\rightarrow\mathcal D'$, $G':\mathcal D'\rightarrow\mathcal C'$, and let $(F,G,\eta,\varepsilon)$, $(F',G',\eta',\varepsilon')$ be adjunctions. A map of adjunctions from the first to the second ...

7

Augmenting Andrej's answer: There is still no widespread agreement on the appropriate interface monad transformers should support in the functional programming context. Haskell's MTL is the de-facto interface, but Jaskelioff's Monatron is an alternative. One of the earlier technical reports by Moggi, an abstract view of programming languages, discusses ...

7

The closest I've seen to an answer to this question is the first picture in the Gallery of Doctor Melliès, illustrating the map $$\neg\neg A \otimes \neg\neg B \longrightarrow \neg\neg(A \otimes B)$$ which exists in any dialogue category (i.e., a monoidal category with closures into a fixed object). Note that the left-to-right CPS transform of general ...

6

At the level of precision used in the nlab page, values are global elements -- i.e., a value of type $A$ corresponds to a morphism $1 \to A$. If you want to be serious about this, there are some technicalities to account for: First, actual Haskell does not actually form a category in the sense that we would hope -- the seq operator breaks a lot of the ...

5

It is an interesting problem to figure out what bothers the OP. First of all, it is not at all the case that the equation put forward by the OP says "different computations have the same value". For instance, the computations do _ <- putStr "foo" return 42 and do _ <- putStr "bar" return 42 both "have" value 42 but are different, since one ...

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.

4

Augmenting Noam's answer: Removing the implicit currying, $f : A \to B \to C$ is the same thing as $uncurry( f) : A \times B \to C$. Strong monads $T$ give a map (two, actually!): $dblstr : T A \times T B \to T (A\times B)$. We therefore have a map: $T A \times T B \xrightarrow {dblstr} T(A\times B) \xrightarrow{uncurry(f)} TC$ If we instantiate this ...

4

The point of stacks is that they are in a sense the dual concept to computations. A computation does not run in a vacuum. It is always "surrounded" by some sort of an environment, or evaluation context, telling us what the current "state of progress" is, or is recording "where we are, and where we're going". Often this sort of information has stack-like ...

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

3

Since Andrej has somewhat covered the operational side, I'll take the more semantic/category theoretic perspective of why we care about stacks, that is especially relevant in EEC. The general philosophy of categorical logic is that all types should be defined by a universal property. In CBPV without stacks, you cannot give a universal property to the $F$ ...

2

Using Free, you can have a HOAS embedding of the untyped lambda calculus. And then write a structurally recursive function firing the top-level redex again and again. Good luck trying to normalise reduce omega. {-# NO_POSITIVITY_CHECK #-} data Free (f : Set → Set) (a : Set) : Set where Pure : a → Free f a Roll : f (Free f a) → Free f a data LAMF (T : ...

2

The terminology can be a bit confusing but yes there are two languages in for instance Moggi's "Notions of Computations as Monads" (free link here: https://core.ac.uk/download/pdf/21173011.pdf). In that paper, the languages are called $\lambda_{ml}$, the metalanguage, and $\lambda_{pl}$ the "programming language". I believe $\lambda_{pl}$ plays the role of ...

1

I still don't quite understand what having a value means, but just considering the question of "can we give up the eta rule for monads", the answer is yes, this is an entirely reasonable thing to consider. As a rule of thumb, having the eta rule in the syntax corresponds to the uniqueness condition on a universal property. So if you want to add natural ...

1

This paper gives some important recent work using monads.

1

The problem with your counterexample is that the type you presented is not a valid instance of ArrowApply as far as I can tell. You didn't present what the implementation of app but the only one I could come up with (where you use the input stream function once and then discard it) doesn't satisfy the 2nd and 3rd ArrowApply laws. What definition of app did ...

1

Erlang is an example. I actually don't know Erlang, so I'm going to use some pseudocode: Suppose you have two threads, Alice and Bob. They talk by calling each other's Send member route, which blocks until the other end replies. Alice can keep some "mutable state" for a single integer as follows: Alice: function main_loop(state): message = Receive() ...

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