A new project,
obviates my previous posts on automatic redis.
The team has created an algorithm, called static differentiation, which performs a
source to source translation on functions in the simply typed lambda calculs.
The resulting function takes twice as many arguments as the previous program, with every
other argument being a diff, or derivative, on the previous argument. When further
optimizations are applied to the source, such as constant reduction and dead code elimination,
arguments can sometimes be removed entirely. Here is an example from the paper:
typeMultiSet=MapStringNat-- | grandTotal counts the number of elements in each set and adds themgrandTotal::MultiSet->MultiSet->NatgrandTotalxsys=fold(+)0(mergexsys)where-- Imported:fold::(Nat->Nat->Nat)->Nat->MultiSet->Nat(+)::Nat->Nat->Nat0::Natmerge::MultiSet->MultiSet->MultiSet
-- The derivative of a natural number is an integer, since-- the natural number can either increase or decrease.typeNat'=InttypeMultiSet'=MapStringNat'grandTotal'::MultiSet->MultiSet'->MultiSet->MultiSet'->Nat'grandTotal'xsxs'ysys'=fold'(+)(+') 0 (derive 0) (merge xs ys) (merge'xsdxsysdys)where-- Imported:fold'::(Nat->Nat->Nat)->(Nat->Nat'->Nat->Nat'->Nat')->Nat->Nat'->MultiSet->MultiSet'->Nat'(+)::Nat->Nat->Nat(+') :: Nat -> Nat'->Nat->Nat'->Nat'0::Natderive::Nat->Nat'merge::MultiSet->MultiSet->MultiSetmerge'::MultiSet->MultiSet'->MultiSet->MultiSet'->MultiSet
When optimizations are applied, grandTotal' becomes the implementation
that a programmer would have written:
In this case, the resulting grandTotal' makes no reference to the original multisets at all.
The authors of the paper call this “self-maintainability”, by analogy to self-maintainable
views in databases.
The problem of infering redis update operations from database update operations, then,
is simply a matter of differentiating and then optimizing the cache schema. (“Cache schema” is
the mapping from redis keys to the database queries that populate those keys.)
The mappings whose derivatives are self-maintainable can be translated into redis commands.
Here is the source transformation described in the paper:
moduleDifferentiatewheretypeId=StringdataTermp=Primitivep|LambdaId(Termp)|App(Termp)(Termp)|VarIdderiving(Eq,Ord,Read,Show)differentiate::MonadIdm=>(p->m(Termp))->Termp->m(Termp)differentiatedifferentiatePrimitive=diffwherediffterm=casetermofPrimitivep->differentiatePrimitivepLambdavarterm->doletdvar="d"++varrememberIdvarvar$generateIddvar$\var'->doterm'<-rememberIddvarvar'$difftermreturn(Lambdavar(Lambdavar'term'))Appst->dos'<-diffs-- t and t' will often share common sub-expressions.-- A better implementation would factor their commonalities out,-- to avoid redundant computation at runtime.t'<-difftreturn(App(Apps't)t')Varvar->dovar'<-recallIdvarreturn(Varvar')classMonadm=>MonadIdmwhere-- Return a unique string that starts with the given string.generateId::String->(String->ma)->ma-- Add mapping from old variable name to new variable namerememberId::String->String->ma->ma-- Lookup the new variable name that was mapped to the given old variable name.recallId::String->mString
1: I’m being a little imprecise when I define
the derivative of a type as another type, since the type of the derivative can vary
depending on the value. The derivative of 3 is all integers from -3 to positive infinity,
not all integers.