Hot answers tagged

17 votes

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 ...
user avatar
  • 26.7k
12 votes
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 ...
user avatar
9 votes
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 ...
user avatar
  • 26.7k
8 votes
Accepted

What are the morphisms of Adj(C,T) - the category whose objects are the adjunctions of a given monad?

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':\...
user avatar
7 votes

Explaining monad transformers in categorical terms

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 ...
user avatar
  • 2,637
6 votes
Accepted

What are values relative to Hask?

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 ...
user avatar
5 votes

What logic correponds via Curry-Howard to a Monad?

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 ...
user avatar
5 votes

Moggi's computational metalanguage

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 ...
user avatar
  • 26.7k
4 votes

Continuation passing transform of binary functions

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 \...
user avatar
  • 2,637
4 votes
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 ...
user avatar
  • 26.7k
3 votes

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 ...
user avatar
  • 1,474
3 votes

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.
user avatar
  • 26.7k
2 votes
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 ...
user avatar
  • 636
2 votes
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 ...
user avatar
  • 1,474
2 votes
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 ...
user avatar
1 vote

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

This paper gives some important recent work using monads.
user avatar
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 ...
user avatar
  • 1,474
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 ...
user avatar
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 ...
user avatar
  • 181

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