<p>I'm unsure whether the following three equations constitute a valid instance of a reader/environment monad on the simply-typed lambda calculus, where <span class="math-container">$\alpha$</span> is any type (I subscript some terms with their types), <span class="math-container">$\mathbb{M}$</span> is the proposed monadic type modality), <span class="math-container">$\eta$</span> is the <em>unit</em> of the monad and <span class="math-container">$\mu:\mathbb{M} \mathbb{M}\alpha → \mathbb{M}\alpha$</span> is the <em>join</em> of the monad:</p>
<p><span class="math-container">$$\mathbb{M} \thinspace α = ((s → t) → t) → α  \hspace{1cm} ∀α$$</span>
<span class="math-container">$$ \eta \, a_{\alpha} = \lambda c_{((s \to t)\to t)}.\; a \hspace{2cm} ∀a_{\alpha}$$</span>
<span class="math-container">$$\mu\,b_{\mathbb{M}\mathbb{M} \alpha} = λc_{((s → t) → t)}.\; b_{\mathbb{M}\mathbb{M}\alpha}\, c\, c \hspace{1cm} ∀b_{\mathbb{M}\mathbb{M} \alpha} $$</span></p>
<p>I'm unsure because this would allow us to generate terms of type <span class="math-container">$((s → t) → t) → s$</span>, which is not constructively valid, given <span class="math-container">$((s → \bot) → \bot)$</span> does not constructively entail <span class="math-container">$s$</span>. However, in the type system I am using, type <span class="math-container">$s$</span> is not the type of truth values, but the type of Kripke states. I don't know whether this matters.</p>
<p>If I changed the definition of the monad so that the first equation was substituted by the following equation, would it be a valid instance of a reader monad?</p>
<p><span class="math-container">$$\mathbb{M} \thinspace α = ((\beta → t) → t) → α , \hspace{1cm} ∀α \text{ and where } \alpha \neq \beta$$</span></p>
<hr />
<p>Edit:</p>
<p>Following on from Andrej Bauer's comment below, I suppose I am confused about whether we can we always construct a reader monad by type synonyms of the form <span class="math-container">$u = x$</span>, for arbitrary function types <span class="math-container">$x$</span>?</p>

CC BY-SA 4.0
2020-08-12T12:35:40.140Z
If you introduce the abbreviation $u = (s \to t) \to t$ and write your $\mathbb{M}$ using $u$, don't you just get the standard reader monad? What is the term of type $((s \to t) \to t) \to s$ that you are able to generate?
Andrej Bauer
CC BY-SA 4.0
2020-08-12T12:37:46.720Z
Also, you should probably spell out the monad unit, so we do not have to guess it.
Andrej Bauer
CC BY-SA 4.0
2020-08-12T12:46:06.203Z
@Andrej Bauer: Yes, I thought you just got the reader monad by a type synonym. But then applying $\mathbb{M}$ to $\alpha := s$, we get $((s \to t) \to s) \to s$, and that is of the same `shape' as $((s \to \bot) \to \bot) \to s$, and I thought $((s \to \bot) \to \bot) \to s$ was not typeable constructively because of the lack of double negation elimination in constructive logic. So I'm wondering whether, given $s$ is a particular type, which I have defined in my type theory (the type of Kripke states), does this matter?
user65526
CC BY-SA 4.0
2020-08-12T12:54:25.343Z
@Andrej Bauer: I suppose one way of putting my question would be this: can we always construct a reader monad by type synonyms of the form $u=x$, for arbitrary function types $x$? I think my confusion might be based on thinking about $((s \to t) \to t) \to \alpha$, as a co-monadic modality. For then we would have to have a function $\mathbb{M}\alpha \to \alpha$, for arbitrary $a$, and this is not always constructible when $\mathbb{M}\alpha = ((s \to t) \to t) \to \alpha$.
user65526
CC BY-SA 4.0
2020-08-12T16:58:55.867Z
$((s \to \bot) \to \bot) \to s$ is a type, so it does not make sense to say that it is "typeable" (terms might or might not be typeable), you probably mean "inhabited". But so what if it is not inhabited? Maybe we should move over t cs.stackexchange.com so we do not pollute this site, it's for research-level questions.
Andrej Bauer
CC BY-SA 4.0
2020-08-12T17:31:02.797Z
@Andrej I am confused because of what people said in response to a question posted here: https://stackoverflow.com/questions/62509788/the-intuition-behind-the-definition-of-the-co-reader-monad My confusion there relates to the confusion here. It doesn't make sense to me what was said there unless it is actually important whether a type is inhabited. For there it is commented that ``extract :: ((e -> a) -> a) -> e`` would not be implementable because not constructively valid.  But the $\eta$ above allows a function of this type. So this is very confusing.
user65526
CC BY-SA 4.0
2020-08-12T17:38:15.663Z
@AndrejBauer Maybe we should, if it is likely to receive an answer there. :)
user65526
CC BY-SA 4.0
2020-08-12T21:31:01.297Z
There's nothing to answer. You're confusing "type is well-formed' with "type is inhabited".
Andrej Bauer
<lambda-calculus><ct.category-theory><monad>
Is this a reader monad?
user65526
# Is this a reader monad?

(Asked by: username_0 on 2020-08-12)

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 their types), $\mathbb{M}$ is the proposed monadic type modality), $\eta$ is the *unit* of the monad and $\mu:\mathbb{M} \mathbb{M}\alpha → \mathbb{M}\alpha$ is the *join* of the monad:

$$\mathbb{M} \thinspace α = ((s → t) → t) → α \hspace{1cm} ∀α$$
$$ \eta \, a\_{\alpha} = \lambda c\_{((s \to t)\to t)}.\; a \hspace{2cm} ∀a\_{\alpha}$$
$$\mu\,b\_{\mathbb{M}\mathbb{M} \alpha} = λc\_{((s → t) → t)}.\; b\_{\mathbb{M}\mathbb{M}\alpha}\, c\, c \hspace{1cm} ∀b\_{\mathbb{M}\mathbb{M} \alpha} $$

I'm unsure because this would allow us to generate terms of type $((s → t) → t) → s$, which is not constructively valid, given $((s → \bot) → \bot)$ does not constructively entail $s$. However, in the type system I am using, type $s$ is not the type of truth values, but the type of Kripke states. I don't know whether this matters.

If I changed the definition of the monad so that the first equation was substituted by the following equation, would it be a valid instance of a reader monad?

$$\mathbb{M} \thinspace α = ((\beta → t) → t) → α , \hspace{1cm} ∀α \text{ and where } \alpha \neq \beta$$

---

Edit:

Following on from username_1's comment below, I suppose I am confused about whether we can we always construct a reader monad by type synonyms of the form $u = x$, for arbitrary function types $x$?

**Tags:** lambda-calculus, ct.category-theory, monad

> **Comments:**
> **username_1**: If you introduce the abbreviation $u = (s \to t) \to t$ and write your $\mathbb{M}$ using $u$, don't you just get the standard reader monad? What is the term of type $((s \to t) \to t) \to s$ that you are able to generate?  
> **username_1**: Also, you should probably spell out the monad unit, so we do not have to guess it.  
> **username_0**: @username_1: Yes, I thought you just got the reader monad by a type synonym. But then applying $\mathbb{M}$ to $\alpha := s$, we get $((s \to t) \to s) \to s$, and that is of the same `shape' as $((s \to \bot) \to \bot) \to s$, and I thought $((s \to \bot) \to \bot) \to s$ was not typeable constructively because of the lack of double negation elimination in constructive logic. So I'm wondering whether, given $s$ is a particular type, which I have defined in my type theory (the type of Kripke states), does this matter?  
> **username_0**: @username_1: I suppose one way of putting my question would be this: can we always construct a reader monad by type synonyms of the form $u=x$, for arbitrary function types $x$? I think my confusion might be based on thinking about $((s \to t) \to t) \to \alpha$, as a co-monadic modality. For then we would have to have a function $\mathbb{M}\alpha \to \alpha$, for arbitrary $a$, and this is not always constructible when $\mathbb{M}\alpha = ((s \to t) \to t) \to \alpha$.  
> **username_1**: $((s \to \bot) \to \bot) \to s$ is a type, so it does not make sense to say that it is "typeable" (terms might or might not be typeable), you probably mean "inhabited". But so what if it is not inhabited? Maybe we should move over t cs.stackexchange.com so we do not pollute this site, it's for research-level questions.  
> **username_0**: @Andrej I am confused because of what people said in response to a question posted here: https://stackoverflow.com/questions/62509788/the-intuition-behind-the-definition-of-the-co-reader-monad My confusion there relates to the confusion here. It doesn't make sense to me what was said there unless it is actually important whether a type is inhabited. For there it is commented that ``extract :: ((e -> a) -> a) -> e`` would not be implementable because not constructively valid.  But the $\eta$ above allows a function of this type. So this is very confusing.  
> **username_0**: @AndrejBauer Maybe we should, if it is likely to receive an answer there. :)  
> **username_1**: There's nothing to answer. You're confusing "type is well-formed' with "type is inhabited".  

---

## 0 answers

