jcreed blog > Cache Types, Part 2

Cache Types, Part 2

Definitions

I want to organize some type-centric thoughts about small functional programs that maintain caches of expensive-to-compute data, and the reasons for their correctness. Let's say a "cache span" is a span of types: B←βG→γC \begin{CD} B @<{\beta}<< G @>{\gamma}>> C\\ \end{CD} BB is the "base type". This is the actual data we care about, before we start caching anything. CC is the "cache type". This probably looks like an extension of BB with more record fields, which are the cache. GG is the set of "good cache states", ones where the cached derived data in CC is consistent with BB. There may be multiple cache states in CC that correspond to any particular value in BB: maybe we have some dirty-bit bookkeeping which might be in various different legitimate states. So in general GG is a relation between BB and CC.

We write B\B for the cache span (B,β,G,γ,C)(B, \beta, G, \gamma, C).

A computation ff from type AA to type DD, over state B\B, is a triple of arrows (fB,fC,fG)(f_B, f_C, f_G) that form a commutative diagram A×B←A×βA×G→A×γA×CfB↓↓fG↓fCD×B←D×βD×G→D×γD×C \begin{CD} A\x B @<{A \x\beta}<< A\x G @>{A \x \gamma}>> A\x C\\ @V{f_B}VV @VV{f_G}V @VV{f_C}V\\ D\x B @<<{D \x\beta}< D\x G @>>{D \x \gamma}> D\x C\\ \end{CD} Each vertical arrow can be thought of as being a map A→DA \to D but in a state monad (for store type B,G,B, G, or CC). We can also with slightly more generality define a computation from type AA to type DD, over the state transition from B\B to B′\B', as a commutative diagram A×B←A×βA×G→A×γA×CfB↓↓fG↓fCD×B′←D×β′D×G′→D×γ′D×C′ \begin{CD} A\x B @<{A \x \beta}<< A\x G @>{A \x \gamma}>> A\x C\\ @V{f_B}VV @VV{f_G}V @VV{f_C}V\\ D\x B' @<<{D \x \beta'}< D\x G' @>>{D \x \gamma'}> D\x C'\\ \end{CD} In this case we write f:A×B→D×B′f : A \x \B \to D \x \B'. Composition of computations is composition of commutative diagrams. Let 1\mathbf{1} be the trivial cache span 1←1→11 \leftarrow 1 \to 1.

Lemma Suppose we have cache spans B0,…,Bn\B_0, \ldots, \B_n with B0\B_0 and Bn\B_n both being assumed to be the trivial cache span. Suppose we have types A0,…AnA_0, \ldots A_n. Suppose we have computations f0:A0×B0→A1×B1,…,fn−1:An−1×Bn−1→An×Bnf_0 : A_0 \x \B_0 \to A_1 \x \B_1, \ldots, f_{n-1} : A_{n-1} \x \B_{n-1} \to A_n \x \B_n Then f(n−1)B∘⋯∘f0B=f(n−1)C∘⋯∘f0C f_{(n-1)B}\o\cdots \o f_{0B} = f_{(n-1)C}\o\cdots \o f_{0C}
Proof
A straightforward diagram chase. A0=A0=A0f0B↓↓f0G↓f0CA1×B1←A1×β1A1×G1→A1×γ1A1×C1f1B↓↓f1G↓f1CA2×B2←A2×β2A2×G2→A2×γ2A2×C2f2B↓↓f2G↓f2C⋮ ⋮ ⋮f(n−2)B↓↓f(n−2)G↓f(n−2)CAn−1×Bn−1←An−1×βn−1An−1×Gn−1→An−1×γn−1An−1×Cn−1f(n−1)B↓↓f(n−1)G↓f(n−1)CAn=An=An \begin{CD} A_0 @= A_0 @= A_0\\ @V{f_{0B}}VV @VV{f_{0G}}V @VV{f_{0C}}V\\ A_1\x B_1 @<{A_1 \x \beta_1}<< A_1\x G_1 @>{A_1 \x \gamma_1}>> A_1\x C_1\\ @V{f_{1B}}VV @VV{f_{1G}}V @VV{f_{1C}}V\\ A_2\x B_2 @<{A_2 \x \beta_2}<< A_2\x G_2 @>{A_2 \x \gamma_2}>> A_2\x C_2\\ @V{f_{2B}}VV @VV{f_{2G}}V @VV{f_{2C}}V\\ \vdots @. \vdots @. \vdots \\ @V{f_{(n-2)B}}VV @VV{f_{(n-2)G}}V @VV{f_{(n-2)C}}V\\ A_{n-1}\x B_{n-1} @<{A_{n-1} \x \beta_{n-1}}<< A_{n-1}\x G_{n-1} @>{A_{n-1} \x \gamma_{n-1}}>> A_{n-1}\x C_{n-1}\\ @V{f_{(n-1)B}}VV @VV{f_{(n-1)G}}V @VV{f_{(n-1)C}}V\\ A_n @= A_n @= A_n\\ \end{CD}

We aim to interpret this lemma as saying that the "naive specification" f(n−1)B∘⋯∘f0Bf_{(n-1)B}\o\cdots \o f_{0B} is the same as the "optimized implementation" f(n−1)C∘⋯∘f0Cf_{(n-1)C}\o\cdots \o f_{0C}. Nothing in the above definitions really breaks the symmetry between BB and CC. So far it's just a matter of convention that we regard one arm of the relation GG as being "specification" and the other as "implementation".

Examples

Let's assume our base state type is BB, and that we have some type DD of data derived from BB and a presumed expensive function f:B→Df : B \to D that computes the derived data.

Naive Ref Cell with Push

We can define a cache span Bpush\B_{\mathsf{push}} to be B=B→γpushB×D \begin{CD} B @= B @>{\gamma_{\mathsf{push}}}>> B \x D\\ \end{CD} where γpush(b)=⟨b,f(b)⟩ \gamma_{\mathsf{push}}(b) = \langle b, f(b) \rangle We can define some computations for this cache span.
  1. An initialization computation init:B×1→1×Bpush\mathsf{init} : B \x \mathbf{1} \to 1 \x \B_{\mathsf{push}}: B=B=B∥∥↓γpushB=B→γpushB×D \begin{CD} B @= B @= B\\ @| @| @VV{\gamma_\mathsf{push}}V\\ B @= B @>>{\gamma_{\mathsf{push}}}> B \x D\\ \end{CD} This takes a value of type BB and a trivial store to a store with one ref cell of type BB, whose cache is already warmed up by computing ff.
  2. Given any u:B→Bu : B \to B, an update computation upd:1×Bpush→1×Bpush\mathsf{upd} : 1 \x \B_{\mathsf{push}} \to 1 \x \B_{\mathsf{push}}: B=B→γpushB×Du↓↓u↓updCB=B→γpushB×D \begin{CD} B @= B @>{\gamma_{\mathsf{push}}}>> B \x D\\ @V{u}VV @VV{u}V @VV{\mathsf{upd}_C}V\\ B @= B @>>{\gamma_{\mathsf{push}}}> B \x D\\ \end{CD} where updC⟨b,d⟩=  letb′=u(b)in ⟨b′,f(b′)⟩\mathsf{upd}_C\langle b, d\rangle = \ \ \blet b' = u(b) \bin \langle b', f(b')\rangle If we had decidable equality on BB, we could have checked whether the new value of the store was equal to the previous one, and decided to forgo the computation of ff in that case. For simplicity I won't write out the details here.
  3. A read computation to read out the value of type DD: read:1×Bpush→D×Bpush\mathsf{read} : 1 \x \B_{\mathsf{push}} \to D \x \B_{\mathsf{push}}: B=B→γpushB×DreadB↓↓readB↓readCD×B=D×B→D×γpushD×(B×D) \begin{CD} B @= B @>{\gamma_{\mathsf{push}}}>> B \x D\\ @V{\mathsf{read}_B}VV @VV{\mathsf{read}_B}V @VV{\mathsf{read}_C}V\\ D \x B @= D \x B @>>{D \x \gamma_{\mathsf{push}}}> D \x (B \x D)\\ \end{CD} where readB⟨b,d⟩=  ⟨f(b),b⟩\mathsf{read}_B\langle b, d\rangle = \ \ \langle f(b), b \rangle readC⟨b,d⟩=  ⟨d,⟨b,d⟩⟩\mathsf{read}_C\langle b, d\rangle = \ \ \langle d, \langle b, d \rangle \rangle Notice two things:

Ref Cell with Pull and Dirty Bit

Let's take what is essentially the option type Maybe D\mathtt{Maybe}\ D as a "dirty bit status" S(D)=clean(D)+dirty S(D) = \mathsf{clean}(D) + \mathsf{dirty} We can define a cache span Bpull\B_{\mathsf{pull}} to be B←βpullB×S(1)→γpullB×S(D) \begin{CD} B @<{\beta_{\mathsf{pull}}}<< B \x S(1) @>{\gamma_{\mathsf{pull}}}>> B \x S(D)\\ \end{CD} where βpull(b,s)=b \beta_{\mathsf{pull}}(b, s) = b γpull(b,clean(⋆))=⟨b,clean(f(b))⟩ \gamma_{\mathsf{pull}}(b, \mathsf{clean}(\star)) = \langle b, \mathsf{clean}(f(b)) \rangle γpull(b,dirty)=⟨b,dirty⟩ \gamma_{\mathsf{pull}}(b, \mathsf{dirty}) = \langle b, \mathsf{dirty} \rangle We can define some computations for this cache span.
  1. An initialization computation init:B×1→1×Bpull\mathsf{init} : B \x \mathbf{1} \to 1 \x \B_{\mathsf{pull}}: B=B=B∥↓initG↓initCB←βpullB×S(1)→γpullB×S(D) \begin{CD} B @= B @= B\\ @| @VV{\mathsf{init}_G}V @VV{\mathsf{init}_C}V\\ B @<<{\beta_{\mathsf{pull}}}< B \x S(1) @>>{\gamma_{\mathsf{pull}}}> B \x S(D)\\ \end{CD} where initG(b)=⟨b,dirty⟩ \mathsf{init}_G(b) = \langle b, \mathsf{dirty} \rangle initC(b)=⟨b,dirty⟩ \mathsf{init}_C(b) = \langle b, \mathsf{dirty} \rangle
  2. Given any u:B→Bu : B \to B, we can define an update computation upd:1×Bpull→1×Bpull\mathsf{upd} : 1 \x \B_{\mathsf{pull}} \to 1 \x \B_{\mathsf{pull}}: B←βpullB×S(1)→γpullB×S(D)u↓↓updG↓updCB←βpullB×S(1)→γpullB×S(D) \begin{CD} B @<{\beta_{\mathsf{pull}}}<< B \x S(1) @>{\gamma_{\mathsf{pull}}}>> B \x S(D)\\ @V{u}VV @VV{\mathsf{upd}_G}V @VV{\mathsf{upd}_C}V\\ B @<<{\beta_{\mathsf{pull}}}< B \x S(1) @>>{\gamma_{\mathsf{pull}}}> B \x S(D)\\ \end{CD} where updG(b,s)=⟨u(b),dirty⟩ \mathsf{upd}_G(b, s) = \langle u(b), \mathsf{dirty} \rangle updC(b,s)=⟨u(b),dirty⟩ \mathsf{upd}_C(b, s) = \langle u(b), \mathsf{dirty} \rangle
  3. A read computation to read out the value of type DD: read:1×Bpull→D×Bpull\mathsf{read} : 1 \x \B_{\mathsf{pull}} \to D \x \B_{\mathsf{pull}}: B←βpullB×S(1)→γpullB×S(D)readB↓↓readG↓readCD×B←D×βpullD×(B×S(1))→D×γpullD×(B×S(D)) \begin{CD} B @<{\beta_{\mathsf{pull}}}<< B \x S(1) @>{\gamma_{\mathsf{pull}}}>> B \x S(D)\\ @V{\mathsf{read}_B}VV @VV{\mathsf{read}_G}V @VV{\mathsf{read}_C}V\\ D \x B @<<{D \x \beta_{\mathsf{pull}}}< D \x (B \x S(1)) @>>{D \x \gamma_{\mathsf{pull}}}> D \x (B \x S(D))\\ \end{CD} where readB(b)=  ⟨f(b),b⟩\mathsf{read}_B(b) = \ \ \langle f(b), b \rangle readG⟨b,dirty⟩=  ⟨f(b),⟨b,clean(⋆)⟩⟩\mathsf{read}_G\langle b, \mathsf{dirty}\rangle = \ \ \langle f(b), \langle b, \mathsf{clean}(\star) \rangle \rangle readG⟨b,clean(⋆)⟩=  ⟨f(b),⟨b,clean(⋆)⟩⟩\mathsf{read}_G\langle b, \mathsf{clean}(\star)\rangle = \ \ \langle f(b), \langle b, \mathsf{clean}(\star) \rangle \rangle readC⟨b,dirty⟩=  letd=f(b)in ⟨d,⟨b,clean(d)⟩⟩\mathsf{read}_C\langle b, \mathsf{dirty}\rangle = \ \ \blet d = f(b) \bin \langle d, \langle b, \mathsf{clean}(d) \rangle \rangle readC⟨b,clean(d)⟩=  ⟨d,⟨b,clean(d)⟩⟩\mathsf{read}_C\langle b, \mathsf{clean}(d)\rangle = \ \ \langle d, \langle b, \mathsf{clean}(d) \rangle \rangle Notice: