Questions tagged [monad]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
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-...
17
votes
2answers
2k 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 ...
12
votes
2answers
677 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 ...
12
votes
2answers
602 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 $$\...
11
votes
0answers
146 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
830 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 ...
8
votes
1answer
219 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 ...
7
votes
2answers
788 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 ...
5
votes
2answers
191 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 ...
5
votes
1answer
76 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 ...
4
votes
1answer
135 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 ...
4
votes
1answer
364 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 (...
4
votes
1answer
385 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, ...
3
votes
1answer
229 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
400 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 \...
2
votes
2answers
242 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 \...
2
votes
1answer
180 views

Non-termination, strict positivity and free monads

Using the standard encoding of a free monad in Haskell and its fmap instance: ...
1
vote
1answer
143 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 ...
0
votes
0answers
72 views

Is this a reader monad?

I'm unsure whether the following three equations constitute a valid instance of a reader/environment monad on the simply-typed lambda calculus, where $\alpha$ is any type (I subscript some terms with ...
-2
votes
1answer
73 views

Forming ordered pairs using monads and doing without the Kuratowski encoding of ordered pairs

Suppose we have a set $S$ of constants of the Simply-Typed Lambda Calculus (STLC) various types, and the operation of union $\cup$ which takes two constants and forms their union. For example, $S$ ...