# Tag Info

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

### 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 ...
• 29.4k

### 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 ...
• 595
Accepted

The law bind m (f ∘ g) = f (bind m g) does not hold. The types of functions are: m : M a, ...
• 552

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

### 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,695

### 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 ...
• 1,695
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 &...
• 552
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,695

### 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 ...
• 552
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 ...
• 32.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 ...
• 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 ...
• 552
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

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