Partial application is not SchönfinkelingThe wages of pedantryRSSBlogArchivesAutomatic Redis Through Static DifferentiationMar 1st, 2015| CommentsA new project,“Incremental λ-Calculus”,obviates my previous posts on automatic redis.The team has created an algorithm, called static differentiation, which performs asource to source translation on functions in the simply typed lambda calculs.The resulting function takes twice as many arguments as the previous program, with everyother argument being a diff, or derivative, on the previous argument. When furtheroptimizations are applied to the source, such as constant reduction and dead code elimination,the non-derivativearguments can sometimes be removed entirely. Here is an example from the paper:1234567891011type MultiSet = Map String Nat-- | grandTotal counts the number of elements in each set and adds themgrandTotal :: MultiSet -> MultiSet -> NatgrandTotal xs ys = fold (+) 0 (merge xs ys) where-- Imported:fold :: (Nat -> Nat -> Nat) -> Nat -> MultiSet -> Nat(+) :: Nat -> Nat -> Nat0 :: Natmerge :: MultiSet -> MultiSet -> MultiSetAfter static differentiation, the code becomes:112345678910111213141516171819202122-- The derivative of a natural number is an integer, since-- the natural number can either increase or decrease.type Nat' = Inttype MultiSet' = Map String Nat'grandTotal' :: MultiSet -> MultiSet' -> MultiSet -> MultiSet' -> Nat'grandTotal' xs xs' ys ys' =fold' (+) (+') 0 (derive 0) (merge xs ys) (merge' xs dxs ys dys) 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' -> MultiSetWhen optimizations are applied, grandTotal' becomes the implementationthat a programmer would have written:12345678grandTotal' :: MultiSet' -> MultiSet' -> IntgrandTotal' xs' ys' = fold' (+) 0 (merge' xs' ys')-- Imported:fold' :: (Int -> Int -> Int) -> Int -> MultiSet' -> Int(+) :: Int -> Int -> Int0 :: Intmerge' :: MultiSet' -> MultiSet' -> MultiSet'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-maintainableviews 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” isthe mapping from redis keys to the database queries that populate those