Skip to main content
OverflowAI is here! AI power for your Stack Overflow for Teams knowledge community. Learn more
13 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 ...
Neel Krishnaswami's user avatar
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 ...
Neel Krishnaswami's 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 ...
Andrej Bauer's 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 ...
Henry Story's user avatar
4 votes
Accepted

A monad law about bind and function composition

The law bind m (f ∘ g) = f (bind m g) does not hold. The types of functions are: m : M a, ...
winitzki's user avatar
  • 442
4 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.
Andrej Bauer's user avatar
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 ...
Andrej Bauer's user avatar
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 ...
Max New's user avatar
  • 1,695
3 votes

Kleisli-like category for applicatives?

Yes, your definition does give a category. This is an instance of a somewhat general construction called change of base from enriched category theory. There is an nlab page on the construction but if ...
Max New's user avatar
  • 1,695
3 votes
Accepted

Is is true that every monad transformer is equivalent to its underlying/base monad?

The equation F Id ≅ ∀ (m: Monad). F m seems to be correct (for most transformers F, see below). However, I would not say that &...
winitzki's user avatar
  • 442
3 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 ...
Max New's user avatar
  • 1,695
2 votes

Explaining monad transformers in categorical terms

How could monad transformers be described in the terms of category theory? There are two definitions: the "weak" and the "functorial" one. The "functorial" definition is ...
winitzki's user avatar
  • 442
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 ...
Neel Krishnaswami's user avatar
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 ...
gallais's user avatar
  • 635
1 vote

Kleisli-like category for applicatives?

Your description of that category is correct. We can define a lawful category of this kind. Objects are all types A, B, ... and ...
winitzki's user avatar
  • 442
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 ...
Robert Long's user avatar

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