Questions tagged [monad]
The monad tag has no usage guidance.
20
questions
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$ ...
