0
$\begingroup$

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 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 $u = x$, for arbitrary function types $x$?

Improve this question
$\endgroup$
8
  • 1
    $\begingroup$ 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? $\endgroup$
    – Andrej Bauer
    Aug 12, 2020 at 12:35
  • 1
    $\begingroup$ Also, you should probably spell out the monad unit, so we do not have to guess it. $\endgroup$
    – Andrej Bauer
    Aug 12, 2020 at 12:37
  • $\begingroup$ @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? $\endgroup$
    – user65526
    Aug 12, 2020 at 12:46
  • $\begingroup$ @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$. $\endgroup$
    – user65526
    Aug 12, 2020 at 12:54
  • $\begingroup$ $((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. $\endgroup$
    – Andrej Bauer
    Aug 12, 2020 at 16:58

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.