Return to Question

Simply typed lambda calculus in one type variable in a Cartesian closed category $\mathbf{C}$ can be interpreted as a family of Cartesian closed functors (described below, do they have a name?) from the Cartesian closed category $\mathbf{STLC_1}$ of simply typed lambda calculus signatures with products with one type variable and all terms between them (also described below and does this category have a name?). I will loosely prove that when these functors are endofunctors, they are not monads, and if they were, $\mathbf{STLC_1}$ would be strong enough to interpret untyped lambda calculus. My question is if there is some other category, similar to $\mathbf{STLC_1}$ where the (similar) family of endofunctors are monads, so that untyped lambda calculus can be interpreted in that category.

According to the well known functorial interpretation of simply typed lambda calculus, each pair of signatures $s_1, s_2 \in \mathbf{STLC_1}$ and each term $t : s_1 \to s_2$ corresponds to a pair of functors $F_1, F_2 \in \mathbf{C}^{op} \times \mathbf{C} \to \mathbf{C}$ and a dinatural transformation between them, typically depicted as a commuting hexagon.

This can be turned into a functor $\operatorname{I} : \mathbf{STLC_1} \times \mathbf{C}^{op} \times \mathbf{C} \to \mathbf{C}$. For each pair of objects $a, b \in \mathbf{C}$, each arrow $f : b \to a$, each pair of signatures $s_1, s_2 \in \mathbf{STLC_1}$ and each term $t : s_1 \to s_2$, the functor indicates a commuting hexagon in $\mathbf{C}$. With a little imagination (or some kind hearted editor who masters the LaTeX array environment) it can be depicted:

Since $\mathbf{STLC_1}$ is also Cartesian closed, each signature $s$ can be used to indicate an endofunctor $\operatorname{T_s} \in \mathbf{STLC_1}\to \mathbf{STLC_1}$. Capital $\operatorname{T}$ is usually reserved for endofunctors that are monads, but the functors $\operatorname{T_s}$ are not, or at least not in general. The existence of such a family of monads would imply $\mathbf{STLC_1}$ would be strong enough to interpret untyped lambda calculus. Since the Cartesian closed category $\mathbf{C}$ by definition has all the structure of $\mathbf{STLC_1}$, such monads would imply $\mathbf{C}$, in general, could also implement untyped lambda calculus (I think). Since this is clearly not the case, the endofunctors $\operatorname{T_s}& are not monads (I think).

For any signatures $s_1, s_2 \in \mathbf{STLC_1}$ and any two terms $t_1 : s_2^{s_1}$, $t_2 : s_1$, the universal arrow $eval_{s_1, s_2} : (s_2^{s_1} \times s_1) \to s_2$ of exponentiation in $\mathbf{STLC_1}$ evaluates application of terms. It is the uncurried version of the identity function $id_{s_1, s_2}: (s_1 \to s_2) \to s_1 \to s_2$. With $\pi_1$ and $\pi_2$ as product projections, it can be implemented as

In general, any signature $s$ gives a functor $\operatorname{T_s}$ with a evaluation-function:

The most annoying thing is that there is such a mapping, it is just a set theoretic function, not a lambda calculus one. For all signatures $s_1, s_2 \in \mathbf{STLC_1}$, $\operatorname{T_s}$ takes each term (arrow) $t : s_1 \to s_2$ to an arrow $\operatorname{T_s} t : (\operatorname{T_s}\ s_1) \to (\operatorname{T_s}\ s_2)$. These arrows correspond to points in the corresponding exponential objects $s_2^{s_1}$ and $(\operatorname{T_s}\ s_2)^{\operatorname{T_s}\ s_1}$, so $\operatorname{T_s}$ gives a mapping from points in $s_2^{s_1}$ to points in $(\operatorname{T_s}\ s_2)^{\operatorname{T_s}\ s_1}$, but $\mathbf{STLC_1}$ has no corresponding arrow.

Simply typed lambda calculus in one type variable in a Cartesian closed category $\mathbf{C}$ can be interpreted as a family of Cartesian closed functors (described below, do they have a name?) from the Cartesian closed category $\mathbf{STLC_1}$ of simply typed lambda calculus types with products with one type variable and all terms between them (also described below and does this category have a name?). I will loosely prove that when these functors are endofunctors, they are not monads, and if they were, $\mathbf{STLC_1}$ would be strong enough to interpret untyped lambda calculus. My question is if there is some other category, similar to $\mathbf{STLC_1}$ where the (similar) family of endofunctors are monads, so that untyped lambda calculus can be interpreted in that category.

According to the well known functorial interpretation of simply typed lambda calculus, each pair of types $s_1, s_2 \in \mathbf{STLC_1}$ (s is for signature, CS lingo for lambda types) and each term $t : s_1 \to s_2$ corresponds to a pair of functors $F_1, F_2 \in \mathbf{C}^{op} \times \mathbf{C} \to \mathbf{C}$ and a dinatural transformation between them, typically depicted as a commuting hexagon.

This can be turned into a functor $\operatorname{I} : \mathbf{STLC_1} \times \mathbf{C}^{op} \times \mathbf{C} \to \mathbf{C}$. For each pair of objects $a, b \in \mathbf{C}$, each arrow $f : b \to a$, each pair of types $s_1, s_2 \in \mathbf{STLC_1}$ and each term $t : s_1 \to s_2$, the functor indicates a commuting hexagon in $\mathbf{C}$. With a little imagination (or some kind hearted editor who masters the LaTeX array environment) it can be depicted:

Since $\mathbf{STLC_1}$ is also Cartesian closed, each type $s$ can be used to indicate an endofunctor $\operatorname{T_s} \in \mathbf{STLC_1}\to \mathbf{STLC_1}$. Capital $\operatorname{T}$ is usually reserved for endofunctors that are monads, but the functors $\operatorname{T_s}$ are not, or at least not in general. The existence of such a family of monads would imply $\mathbf{STLC_1}$ would be strong enough to interpret untyped lambda calculus. Since the Cartesian closed category $\mathbf{C}$ by definition has all the structure of $\mathbf{STLC_1}$, such monads would imply $\mathbf{C}$, in general, could also implement untyped lambda calculus (I think). Since this is clearly not the case, the endofunctors $\operatorname{T_s}& are not monads (I think).

For any types $s_1, s_2 \in \mathbf{STLC_1}$ and any two terms $t_1 : s_2^{s_1}$, $t_2 : s_1$, the universal arrow $eval_{s_1, s_2} : (s_2^{s_1} \times s_1) \to s_2$ of exponentiation in $\mathbf{STLC_1}$ evaluates application of terms. It is the uncurried version of the identity function $id_{s_1, s_2}: (s_1 \to s_2) \to s_1 \to s_2$. With $\pi_1$ and $\pi_2$ as product projections, it can be implemented as

In general, any type $s$ gives a functor $\operatorname{T_s}$ with a evaluation-function:

The most annoying thing is that there is such a mapping, it is just a set theoretic function, not a lambda calculus one. For all types $s_1, s_2 \in \mathbf{STLC_1}$, $\operatorname{T_s}$ takes each term (arrow) $t : s_1 \to s_2$ to an arrow $\operatorname{T_s} t : (\operatorname{T_s}\ s_1) \to (\operatorname{T_s}\ s_2)$. These arrows correspond to points in the corresponding exponential objects $s_2^{s_1}$ and $(\operatorname{T_s}\ s_2)^{\operatorname{T_s}\ s_1}$, so $\operatorname{T_s}$ gives a mapping from points in $s_2^{s_1}$ to points in $(\operatorname{T_s}\ s_2)^{\operatorname{T_s}\ s_1}$, but $\mathbf{STLC_1}$ has no corresponding arrow.

$$\lambda\ n . \lambda\ m. (\operatorname{T_{a \to a}}\ m)\ n$$

$$\lambda\ n : ((a \to a) \to a \to a) . \lambda\ m : ((a \to a) \to a \to a). (\operatorname{T_{a \to a}}\ m)\ n$$

Simply typed lambda calculus in one type variable in a Cartesian closed category $\mathbf{C}$ can be interpreted as a family of Cartesian closed functors from the Cartesian closed category $\mathbf{STLC_1}$ of simply typed lambda calculus signatures with products with one type variable and all terms between them (does this category have a name?). The objects $s$ of $\mathbf{STLC_1}$ are defined recursively as

This can be turned into a functor $I : \mathbf{STLC_1} \times \mathbf{C}^{op} \times \mathbf{C} \to \mathbf{C}$. For each pair of objects $a, b \in \mathbf{C}$, each arrow $f : b \to a$, each pair of signatures $s_1, s_2 \in \mathbf{STLC_1}$ and each term $t : s_1 \to s_2$, the functor indicates a commuting hexagon in $\mathbf{C}$

$$ \begin{array}{ccccc} & & \operatorname{I}\ t\ b\ b & & \ & & \operatorname{I}\ s_1\ b\ b \rightarrow \operatorname{I}\ s_2\ b\ b& & \

\operatorname{I}\ s_1\ f\ b \rightuparrow & & & & \rightdownarrow \operatorname{I}\ s_2\ b\ f\

\operatorname{I}\ s_1\ a\ b & & & & \operatorname{I}\ s_2\ b\ a \

\operatorname{I}\ s_1\ a\ f \rightdownarrow & & & & \rightuparrow \operatorname{I}\ s_2\ f\ a\

& &\operatorname{I}\ s_1\ a\ a \rightarrow \operatorname{I}\ s_2\ a\ a & & \ & & \operatorname{I}\ t\ a\ a & & \ \end{array}$$

For any signatures $s_1, s_2 \in \mathbf{STLC_1}$ and any two terms $t_1 : s_2^{s_1}$, $t_2 : s_1$, the universal arrow $eval_{s_1, s_2} : (s_2^s_1 \times s_1) \to s_2$ of exponentiation in $\mathbf{STLC_1}$ evaluates application of terms. It is the uncurried version of the identity function $id_{s_1, s_2}: (s_1 \to s_2) \to s_1 \to s_2$. With $\pi_1$ and $\pi_2$ as product projections, it can be implemented as

So, what I am hoping to find is a category with similar properties as $\mathbf{STLC_1}$, but with the desired units, but really, right now any thoughts or hints are appreciated.

Simply typed lambda calculus in one type variable in a Cartesian closed category $\mathbf{C}$ can be interpreted as a family of Cartesian closed functors (described below, do they have a name?) from the Cartesian closed category $\mathbf{STLC_1}$ of simply typed lambda calculus signatures with products with one type variable and all terms between them (also described below and does this category have a name?). I will loosely prove that when these functors are endofunctors, they are not monads, and if they were, $\mathbf{STLC_1}$ would be strong enough to interpret untyped lambda calculus. My question is if there is some other category, similar to $\mathbf{STLC_1}$ where the (similar) family of endofunctors are monads, so that untyped lambda calculus can be interpreted in that category. 

The objects $s$ of $\mathbf{STLC_1}$ are defined recursively as

This can be turned into a functor $\operatorname{I} : \mathbf{STLC_1} \times \mathbf{C}^{op} \times \mathbf{C} \to \mathbf{C}$. For each pair of objects $a, b \in \mathbf{C}$, each arrow $f : b \to a$, each pair of signatures $s_1, s_2 \in \mathbf{STLC_1}$ and each term $t : s_1 \to s_2$, the functor indicates a commuting hexagon in $\mathbf{C}$. With a little imagination (or some kind hearted editor who masters the LaTeX array environment) it can be depicted:

$$ \operatorname{I}\ s_1\ a\ b \stackrel{\operatorname{I} s_1\ f\ b}{\to} \operatorname{I}\ s_1\ b\ b \stackrel{\operatorname{I}\ t\ b\ b}{\to} \operatorname{I}\ s_2\ b\ b \stackrel{\operatorname{I}\ s_2\ b\ f}{\to} \operatorname{I}\ s_2\ b\ a $$

$$ \operatorname{I}\ s_1\ a\ b \stackrel{\operatorname{I}\ s_1\ a\ f}{\to} \operatorname{I}\ s_1\ a\ a \stackrel{\operatorname{I}\ t\ a\ a}{\to} \operatorname{I}\ s_2\ a\ a \stackrel{\operatorname{I}\ s_2\ f\ a}{\to} \operatorname{I}\ s_2\ b\ a $$

For any signatures $s_1, s_2 \in \mathbf{STLC_1}$ and any two terms $t_1 : s_2^{s_1}$, $t_2 : s_1$, the universal arrow $eval_{s_1, s_2} : (s_2^{s_1} \times s_1) \to s_2$ of exponentiation in $\mathbf{STLC_1}$ evaluates application of terms. It is the uncurried version of the identity function $id_{s_1, s_2}: (s_1 \to s_2) \to s_1 \to s_2$. With $\pi_1$ and $\pi_2$ as product projections, it can be implemented as

So, what I am hoping to find is a category with similar properties as $\mathbf{STLC_1}$, but with the desired units, but really, right now any thoughts or hints are appreciated. Maybe some free category of lambda calculus/cartesian closedness?