We’re rewarding the question askers & reputations are being recalculated! Read more.

Questions tagged [monad]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
5
votes
2answers
151 views

What's the point of stack judgement in CBPV?

Call-by-push-value (CBPV) introduces two main families of types, values and computations, and their corresponding judgements. However, in some extensions/variants/adaptation of CBPV, there is a third ...
7
votes
2answers
651 views

What logic correponds via Curry-Howard to a Monad?

According to Moggi's 1991 paper "Notions of computation and monads" one can represent monadic equational logic with the well known monad $(T, \eta, \mu)$ with T an functor and the two natural ...
8
votes
1answer
172 views

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

This is a reference confusion. Sometimes I see people use the term "Moggi's computational metalanguage" to refer to the calculus presented by Moggi, and sometimes to "Moggi's computational lambda ...
4
votes
1answer
111 views

What are values relative to Hask?

According to ncatlab's page on category theory and haskell, "we can identify a subset of Haskell called Hask that is often used to identify concepts used in basic category theory. One considers ...
2
votes
2answers
216 views

Moggi's computational metalanguage

In Notions of Computation and Monads Moggi models the notion of a computation of type $A$, $TA$, using a monad $T$. Among other things this ensures the $T\eta$ rule: $$\frac{x: A \vdash a:TB}{x:A \...
4
votes
1answer
72 views

Does bisimulation or the approximation lemma work for monadic streams?

For ordinary streams $S_A := \nu X. A \times X$, there is a bisimulation lemma. It says that two streams are equal if there exists a bisimulation between them. A bisimulation is a relation $\sim$ on ...
16
votes
2answers
1k views

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

Background. I am a bachelor student who is interested in research related to category theory, monads and Haskell, and I want to find a topic for my bachelor’s thesis in that area. I have looked at ...
1
vote
1answer
130 views

Are the `ArrowApply` and `Monad` typeclasses equivalent?

It is stated e.g. on Hackage, that the ArrowApply and the Monad typeclasses are equivalent. I have my doubts about this. It is ...
2
votes
1answer
207 views

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

The Wikipedia page for Monad says just that for a monad $(T,\eta,\mu)$ we can define the category of all adjunctions that define the monad: Let $\textbf{Adj}(C,T)$ be the category whose objects ...
3
votes
0answers
338 views

Distributive law between monads in Haskell

A distributive law between monads must satisfy laws that are usually given in terms of the units $\eta$ and multiplications $\mu$ of the two monads. Among the four laws there are: $\mu^S T \circ S l \...
11
votes
0answers
141 views

Are the types that show monads are more powerful than continuations revealing something of fundamental importance?

In 1992 in the paper Imperative Functional Programming, Simon Peyton Jones and Philip Wadler write: So monads are more powerful than continuations, but only because of the types! It is not clear ...
8
votes
2answers
742 views

Explaining monad transformers in categorical terms

Most resource regarding categorical notions in programming describe monads, but I've never seen a categorical description of monad transformers. How could monad transformers be described in the terms ...
4
votes
1answer
365 views

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

I just read this blog post which argues that monads might be too obscure or difficult to understand as the default "interface to the impure world" in purely functional programming languages; instead, ...
13
votes
2answers
566 views

Continuation passing transform of binary functions

Recall the continuation passing transform (CPS transform) which takes $A$ to $\beta A \mathrel{{:}{=}} R^{R^A}$ (where $R$ is fixed) and $f : A \to B$ to $\beta f : \beta A \to \beta B$ defined by $$\...
4
votes
1answer
350 views

Aren't Monads F-Algebra's? And then if that could be said are Comonad's F-Coalgebra's?

So considering a Monad to be a Triple (T:C -> C, η, µ) with eta and mu as the Natural transformations with appropriate signatures, isn't this in essence an F-Algebra? My thinking is that being both (...
17
votes
3answers
2k views

Is there a concept of something like co-applicative functors sitting between comonads and functors?

Any monad is also an applicative functor and any applicative functor is a functor. Also, any comonad is a functor. Is there a similar concept between comonads and functors, something like co-...
12
votes
2answers
606 views

What are the relations between Alternative, MonadPlus(LeftCatch) and MonadPlus(LeftDistributive)?

Following up What’s an example of a Monad which is an Alternative but not a MonadPlus?: Assume $m$ is a monad. What are the relations betweem $m$ being an Alternative, a MonadPlusCatch and a ...