Constructivism, Realizability, Computability

Category theory



A duploid is a category-like structure where objects have a specific polarity and composition is not necessarily associative.

Duploids are models of programming languages with side effects and explicitly polarized positive and negative types, accomodating both call-by-value? and call-by-name? programming paradigms. Duploids axiomatize the algebraic structure of effectful morphisms, and to a certain extent β€œpure” morphisms (those with no side effects) can be characterized by equational properties as thunkable and linear morphisms. Contrast with call-by-push-value which directly provides a syntax for the pure morphisms (as values and stacks).

A duploid can be constructed from an adjunction and the category of duploids is coreflective in the category of adjunctions, equivalent to the subcategory of adjunctions satisfying an equalizing requirement. The intuition is that a duploid is what is left of an adjunction if we only consider (co)Kleisli morphisms and duploids can be identified with adjunctions whose categories can be recovered from the Kleisli morphisms.


A pre-duploid π’Ÿ\mathcal{D} consists of

  1. a set |π’Ÿ||\mathcal{D}| of objects with a polarity map Ο–:|π’Ÿ|β†’{+,βˆ’}\varpi : |\mathcal{D}| \to \{+,-\}. If Ο–(A)=+\varpi(A) = +, we say AA is positive and otherwise negative.
  2. for every pair A,B∈|π’Ÿ|A,B \in |\mathcal{D}| a set of morphisms π’Ÿ(A,B)\mathcal{D}(A,B).
  3. for every compatible pair of morphisms fβˆˆπ’Ÿ(A,B),gβˆˆπ’Ÿ(B,C)f \in \mathcal{D}(A,B), g\in \mathcal{D}(B,C) a composite gβŠ™fβˆˆπ’Ÿ(A,C)g \odot f \in \mathcal{D}(A,C).
  4. for every object AA an morphism id Aβˆˆπ’Ÿ(A,A)id_A \in \mathcal{D}(A,A) that is the identity with respect to composition.
  5. For every fβˆˆπ’Ÿ(A,B),gβˆˆπ’Ÿ(B,C),hβˆˆπ’Ÿ(C,D)f \in \mathcal{D}(A,B), g \in \mathcal{D}(B,C), h \in \mathcal{D}(C,D), an associative law hβŠ™(gβŠ™f)=(hβŠ™g)βŠ™fh \odot (g \odot f) = (h \odot g) \odot f when BB is negative or CC is positive.

Note that when restricted to positive objects or negative objects, composition and identities form a category, written 𝒫\mathcal{P} and 𝒩\mathcal{N}. When the polarity is known we write positive objects as P,Q,RP,Q,R and negative objects as L,M,NL,M,N. We call composition where the middle object is positive β€œpositive composition” or β€œby-value composition” and notate it as gβ€’fg \bullet f and when the middle object is negative we call it β€œnegative composition” or β€œby-name composition” and notate it as g∘fg \circ f. Then the associativity laws can be restated as:

  1. β€’β€’\bullet\bullet: fβ€’(gβ€’h)=(fβ€’g)β€’hf \bullet (g \bullet h) = (f \bullet g) \bullet h
  2. ∘∘\circ\circ: f∘(g∘h)=(f∘g)∘hf \circ (g \circ h) = (f \circ g) \circ h
  3. β€’βˆ˜\bullet\circ: fβ€’(g∘h)=(fβ€’g)∘hf \bullet (g \circ h) = (f \bullet g) \circ h

and we can see that the only obstacle to associativity is that f∘(gβ€’h)f \circ (g \bullet h) is not necessarily equal to (f∘g)β€’h(f \circ g) \bullet h.

A duploid is a pre-duploid π’Ÿ\mathcal{D} plus two polarity shifts ⇓:|𝒩|β†’|𝒫|and⇑:|𝒫|β†’|𝒩|\Downarrow : |\mathcal{N}| \to |\mathcal{P}| and \Uparrow : |\mathcal{P}| \to |\mathcal{N}|, and for each P∈|𝒫|,N∈|𝒩|P \in |\mathcal{P}|, N \in |\mathcal{N}|, morphisms:

  1. delay P:P→⇑Pdelay_P : P \to \Uparrow P
  2. force P:⇑Pβ†’Pforce_P : \Uparrow P \to P
  3. wrap N:N→⇓Nwrap_N : N \to \Downarrow N
  4. unwrap N:⇓Nβ†’Nunwrap_N : \Downarrow N \to N

such that

  1. βˆ€f:Aβ†’P,force P∘(delay Pβ€’f)=f\forall f : A \to P, force_P \circ (delay_P \bullet f) = f
  2. βˆ€f:Nβ†’A,(f∘unwrap N)β€’wrap N=f\forall f : N \to A, (f \circ unwrap_N) \bullet wrap_N = f
  3. delay Pβ€’force P=id ⇑Pdelay_P \bullet force_P = id_{\Uparrow P}
  4. wrap N∘unwrap N=id ⇓Nwrap_N \circ unwrap_N = id_{\Downarrow N}

In light of the definition of linear and thunkable morphisms, these identities are equivalent to saying

  1. wrap Nwrap_N is thunkable.
  2. wrap N,unwrap Nwrap_N, unwrap_N is an isomorphism.
  3. force Pforce_P is linear.
  4. force P,thunk Pforce_P, thunk_P is an isomorphism.

Linear and Thunkable Morphisms

Just as thunkable morphisms can be defined in a thunk-force category and linear morphisms can be defined in a category with a runnable monad, they can be defined in a duploid in a similar way using delay Pdelay_P in place of the thunk and unwrap Nunwrap_N in place of the run morphism. However, thunkable and linear morphisms can also be defined in a pre-duploid, giving a simple characterization just in terms of associativity of composition.

A morphism ff is thunkable if for all compatible g,hg,h,

hβŠ™(gβŠ™f)=(hβŠ™g)βŠ™f.h \odot (g \odot f) = (h \odot g) \odot f.

and a morphism ff is linear if for all compatible g,hg,h,

fβŠ™(gβŠ™h)=(fβŠ™g)βŠ™h.f \odot (g \odot h) = (f \odot g) \odot h.

Observe that all f:Pβ†’Bf : P \to B are trivially linear and g:Aβ†’Ng : A \to N are trivially thunkable. Further thunkable and linear morphisms form (non-full) subcategories π’Ÿ t,π’Ÿ l\mathcal{D}_t, \mathcal{D}_l.

To understand these concepts, consider the non-trivial situation where f:A→Pf : A \to P is thunkable:

h∘(gβ€’f)=(h∘g)β€’f.h \circ (g \bullet f) = (h \circ g) \bullet f.

on the left side, since we have a by-name composition, hh is β€œevaluated first”, whereas on the right side we have a by-value composition, so ff is evaluated first. Thus these two morphisms being equal implies in many semantics ff cannot perform any side-effect?. For instance if ff prints to the screen and so does hh, then each composite will print in a different order. Furthermore, if ff can manipulate its continuation? explicitly, it has to treat it linearly otherwise hh may be evaluated twice or not at all.

In the dual, if f:N→Bf : N \to B and ff is linear:

f∘(gβ€’h)=(f∘g)β€’hf \circ (g \bullet h) = (f \circ g) \bullet h

holds and similarly ff is evaluated first in the left morphism and hh is evaluated first in the right. Then as above it cannot perform any effects and has to treat its input linearly, as duplicating or dropping hh would make the equation fail to hold.

Relation to Adjunctions

Briefly, the category of duploids and duploid functors is a reflective subcategory of the category of adjunctions and morphisms of adjunctions.

A Duploid from an Adjunction

First, we construct a duploid from an adjunction, which we think of as a forgetful functor that only remembers the Kleisli morphisms of the adjunction. To keep the proof unbiased, we start with a profunctor O:C βˆ’β‡ΈC +O : C_- ⇸ C_+ that the adjunction represents. This gives us a notion of β€œoblique-” or hetero-morphism from a positive object P∈C +P \in C_+ to a negative object N∈Cβˆ’N \in C- as O(P,N)O(P,N) and can be used to define the Kleisli and coKleisli categories. In programming applications these are the β€œpossibly effectful” morphisms. Then let F⊣GF \dashv G be adjoint functors representing OO, i.e. there is a natural equivalence:

C +(FP,N)β‰…O(P,N)β‰…C βˆ’(P,GN). C_+(F P, N) \cong O(P,N) \cong C_-(P, G N).

The pre-duploid π’Ÿ\mathcal{D} has as objects |π’Ÿ|=|C +|+|C βˆ’||\mathcal{D}| = |C_+| + |C_-| with Ο–(P)=+,Ο–(N)=βˆ’\varpi(P) = +, \varpi(N) = -. The morphisms are defined as:

π’Ÿ(A,B)=O(A +,B βˆ’)\mathcal{D}(A,B) = O(A^+,B^-)


P +=PP^+ = P
N +=GNN^+ = G N
P βˆ’=FPP^- = F P
N βˆ’=NN^- = N

and identities are given by the identities/unit and counit of the adjunction:

id P:O(P,FP)≑C βˆ’(FP,FP)\id_P : O(P, F P) \equiv C_-(F P,F P)
id N:O(GN,N)≑C +(GN,GN)\id_N : O(G N, N) \equiv C_+(G N,G N)

To define composition of fβˆˆπ’Ÿ(A,B),gβˆˆπ’Ÿ(B,C)f \in \mathcal{D}(A,B), g \in \mathcal{D}(B,C), we inspect BB. If B=PB = P is positive, composition is interpreted as composition in C βˆ’C_-, or equivalently in the Kleisli category of GFGF, using

f∈O(A +,FP)β‰…C βˆ’(FA +,FP)f \in O(A^+,F P) \cong C_-(F A^+, F P)
g∈O(P,C βˆ’)β‰…C βˆ’(FP,C βˆ’)g \in O(P, C^-) \cong C_-(F P, C^-)

and similarly if B=NB = N is negative, composition is interpreted as composition in C +C_+, or equivalently in the Kleisli category of FGFG, using

f∈O(A +,N)β‰…C +(A +,GN)f \in O(A^+,N) \cong C_+(A^+, G N)
g∈O(GN,C βˆ’)β‰…C +(GN,GC βˆ’)g \in O(G N, C^-) \cong C_+(G N, G C^-)

This definition makes it clear that the identities are identity and the β€’β€’\bullet\bullet and ∘∘\circ\circ laws hold from identity and associativity of C +,C βˆ’C_+,C_-.

Adjunction from a Duploid

From a duploid, we can construct the β€œcofree” adjunction: i.e., a right adjoint to the forgetful functor just defined. Intuitively, we want to recover the homomorphisms just from the heteromorphisms. The maximal choice is to consider all thunkable morphisms between positive types and linear morphisms between negative types to be homomorphisms.

Furthermore, this functor is fully faithful, making the category of duploids a reflective subcategory of adjunctions: they can be identified with exactly those adjunctions in which the unit and counit are mono and epi respectively and in which all thunkable heteromorphisms are the image under FF of some homomorphism and vice-versa all linear heteromorphisms are in the image of GG. This is equivalent to saying that the unit Ξ·\eta is the equalizer of GFΞ·GF\eta and Ξ·GF\eta GF and dually that the counit Ο΅\epsilon is the coequalizer of FGΟ΅FG\epsilon and Ο΅FG\epsilon FG


Duploids were introduced in chapter II of