Type formation rules for a monad

Question

In type theory there are type forming rules, e.g., for product:

judging $$ \Gamma \vdash A : \text{Type} \ \ \Gamma \vdash B : \text{Type} $$ allows us to judge $$ \Gamma \vdash A \times B : \text{Type} $$

I would like a set of type forming rules which would encapsulate the idea of "a monad on Type". It would consist probably of a morphism $T : \text{Type} \rightarrow \text{Type}$, and morphisms $TT \rightarrow T$, $\text{Id} \rightarrow T$ (with whatever type forming rules are necessary to make sense of this). But the coherence is tripping me up, and I cannot seem to find this written anywhere.

Having monads like this would be nice, since one could then do modal type theory, and I would have a better understanding of how haskell translates to formal type theory.

Answer 1

This is a nice idea that was investigated 30 years ago by Moggi:

Moggi, Eugenio (1991). Notions of Computation and Monads. Information and Computation. 93 (1): 55–92. doi:10.1016/0890-5401(91)90052-4

Answer 2

Moggi gives a categorical semantics for monads but doesn't give an operational one.

I'm not really sure of the best resources on operational semantics for monadic types.

You do want some core reduction like

$$ (\mathop{\textbf{do}} x \leftarrow \mathop{\textbf{pure}} e ; e') \longrightarrow [x := e] e' $$

And for something like a writer monad a reduction like

$$ (\mathop{\textbf{do}} x \leftarrow \mathop{\textbf{write}} e_1 ; \mathop{\textbf{write}} e_2 ) \longrightarrow \mathop{\textbf{write}} e_1 \cdot [x := \mathop{\textbf{tt}}] e_2$$

Now every monad arises from an adjunction so you could also use call by push value as an option which is based around reductions

$$ \mathop{\textbf{return}} e \mathop{\textbf{to}} x. e' \longrightarrow [x := e] e' $$

$$ \mathop{\textbf{force}} (\mathop{\textbf{thunk}} e) \longrightarrow e$$

Call by push value is itself subsumed by linear logic. IIRC the "best" behaving fragment of linear logic without commuting conversions is pretty small basically just being linear functions.

You also mentioned modal logic and not every modality is a monad.

For a lax monoidal functor (basically applicative functor) you want something based on Day convolution.

$$ (\mathop{\textbf{do}} \, (x, y) \leftarrow (\mathop{\textbf{pure}} e_1, \mathop{\textbf{pure}} e_2) ; e_3) \longrightarrow [x := e_1, y := e_2] e_3 $$

But I'm unsure of how well it computes.

Unfortunately I suspect all of these approaches suffer from commuting conversions which are kind of ugly. Extremely simple approaches like hereditary substitution fail there.

IIRC the usual semantics for modal logic is based around Kripke semantics but I don't really understand it.

It would help to know what you need modal logic for. You probably don't need canonical forms. Stuff like hereditary substitution are just one of those games logicians play like trying to prove 1+1=2 in as many pages as possible.