15
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 ...
- 32.8k
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 ...
- 32.8k
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 ...
- 29.4k
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 ...
- 595
5
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, ...
- 552
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.
- 29.4k
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 ...
- 29.4k
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 ...
- 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 ...
- 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 &...
- 552
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 ...
- 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 ...
- 552
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 ...
- 32.8k
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 ...
- 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