Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
The principle at work here is that while call-by-push-value gives us a
syntax for an adjunction (between value and computation categories)
with a syntax for the profunctor the adjunction represents (the term
morphisms), we can also consider the \emph{Kleisli} categories of the
adjunction, which are equivalent to the images of the $\u F$ and $U$
types.
%
These are precisely the categories corresponding to call-by-value and
call-by-name languages respectively.
%
Then we can ask in what sense the connectives extend from functors on
the value and computation categories to ``functors'' on the
corresponding Kleisli and co-Kleisli categories.
%
We put ``functor'' in quotes because in fact, these will not quite
satisfy the ordinary sense of functoriality in multiple arguments.
%
Instead, the functors will be \emph{separately functorial} in each
argument, whereas ordinarily functor in several argument means
\emph{jointly functorial}.
%
So for example let $\cat C, \cat D , \cat E$ be categories, then we
would say that a separately functorial function $F : \cat C, \cat D
\to \cat E$ would consist of first an action on objects $F_0 : \cat
C_0, \cat D_0 \to \Cat E_0$ and then two actions: taking any object $d
\in D_0$ to a functor $F(-,id_d) : \cat C \to \cat E$ and similarly
one taking any object $c \in C_0$ to a functor $F(id_c,=): \cat D \to
\cat E$.
%
Then we have two candidates for a true joint functorial action that
are in general not equal: $F(f,id)\circ F(id,g)$ and vice-versa
$F(id,g) \circ F(f,id)$.
%
The fact that these are \emph{not} models the fact that evaluation
order matters.
\begin{theorem}[Effectful Functors]
Given a call-by-push-value adjunction model $V,C,R,F,U$ and given
any jointly functorial functor $G : D_1,\ldots,D_n \to E$ where all
of $D_1,\ldots,D_n,E$ are either $V,C,V^o,C^o$, that is
\emph{strong} in that for each argument category $D_i$, there are
morphisms of one of the following forms (whichever is well-sorted
for $G$ and $D_i$)
\[ G(D_1,\ldots,F(D_i),\ldots,D_n) \to F(G(D_1,\ldots,D_n)) \]
\[ G(D_1,\ldots,U(D_i),\ldots,D_n) \to F(G(D_1,\ldots,D_n)) \]
\[ G(D_1,\ldots,F(D_i),\ldots,D_n) \to U(G(D_1,\ldots,D_n)) \]
\[ G(D_1,\ldots,U(D_i),\ldots,D_n) \to U(G(D_1,\ldots,D_n)) \]
then there is an
associated separately functorial functor $\hat G : \hat
D_1,\ldots,\hat D_n \to \hat E$ where
\begin{align*}
\hat V = F(V)\\
\hat C = U(C)\\
\hat D^o = (\hat D)^o
\end{align*}
\end{theorem}
\begin{proof}
\end{proof}