# Tag Info

### Status quo of category theory and monads in theoretical computer science research?

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 ...
• 26.8k
Accepted

### What logic correponds via Curry-Howard to a Monad?

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 ...
• 31.8k
Accepted

### Explaining monad transformers in categorical terms

According to Oleksandr Manzuk, they are "translation of a monad along an adjunction", see "Calculating Monad Transformers with Category Theory". By the way, that's the third hit on Google for "monad ...
• 26.8k
Accepted

• 2,637
Accepted

### What's the point of stack judgement in CBPV?

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 ...
• 26.8k

### What's the point of stack judgement in CBPV?

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 ...
• 1,494

### Dependently typed monad

Some of the following may be relevant: Relative monads by Thorsten Altenkirch, James Chapman and Tarmo Uustalu. Flexibly graded monads and graded algebras by Dylan McDermott and Tarmo Uustalu.
• 26.8k
Accepted

### Non-termination, strict positivity and free monads

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 ...
• 636
Accepted

### What's the difference between Moggi's computational metalanguage and Moggi's lambda calculus?

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 ...
• 1,494
Accepted

### Moggi's computational metalanguage

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 ...
• 31.8k
1 vote

### Status quo of category theory and monads in theoretical computer science research?

This paper gives some important recent work using monads.
1 vote
Accepted

### Are the ArrowApply and Monad typeclasses equivalent?

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 ...
• 1,494
1 vote

### Explaining monad transformers in categorical terms

I would highly recommend the book book by Bartosz Milewski "Category Theory for Programmers" which goes into some detail about Monads from a Category Theoretic perpective. And it's also ...
• 111
1 vote

### How can the actor model be applied to allow pure functional languages to have side-effects?

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

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