A new project, “Incremental λ-Calculus”, 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, the non-derivative arguments can sometimes be removed entirely. Here is an example from the paper:
type MultiSet = Map String Nat -- | grandTotal counts the number of elements in each set and adds them grandTotal :: MultiSet -> MultiSet -> Nat grandTotal xs ys = fold (+) 0 (merge xs ys) where -- Imported: fold :: (Nat -> Nat -> Nat) -> Nat -> MultiSet -> Nat (+) :: Nat -> Nat -> Nat 0 :: Nat merge :: MultiSet -> MultiSet -> MultiSet
After static differentiation, the code becomes:1
-- The derivative of a natural number is an integer, since -- the natural number can either increase or decrease. type Nat' = Int type 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 :: Nat derive :: Nat -> Nat' merge :: MultiSet -> MultiSet -> MultiSet merge' :: MultiSet -> MultiSet' -> MultiSet -> MultiSet' -> MultiSet
When optimizations are applied,
grandTotal' becomes the implementation
that a programmer would have written:
grandTotal' :: MultiSet' -> MultiSet' -> Int grandTotal' xs' ys' = fold' (+) 0 (merge' xs' ys') -- Imported: fold' :: (Int -> Int -> Int) -> Int -> MultiSet' -> Int (+) :: Int -> Int -> Int 0 :: Int merge' :: 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-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:
File /home/jball/git/joshua.ball.name/downloads/code/static-differentiation/Differentiate.hs could not be found
Returning to an example from the first post:
userIds :: RedisSet userIds = setToRedisSet (mapProjection userId (dbTableToSet usersTable)) setToRedisSet :: Set Id -> RedisSet mapProjection :: (User -> Id) -> Set User -> Set Id userId :: User -> Id dbTableToSet :: DbTable User -> Set User usersTable :: DbTable User
The derivative is
userIds' :: RedisSet' userIds' = setToRedisSet' (mapProjection userId (dbTableToSet usersTable)) (mapProjection' userId userId' (dbTableToSet usersTable) (dbTableToSet' usersTable usersTable')) setToRedisSet' :: Set Id -> Set' Id Id' -> RedisSet' mapProjection :: (User -> Id) -> Set User -> Set Id mapProjection' :: (User -> Id) -> (User -> User' -> Id') -> Set User -> Set' User User' -> Set' Id Id' userId :: User -> Id userId' :: User -> User' -> Id' dbTableToSet :: DbTable User -> Set User dbTableToSet' :: DbTable User -> DbTable' User User' -> Set' User User' usersTable :: DbTable User usersTable' :: DbTable' User User' data RedisSet' = SAdd String | ... data DbTable' a a' = Insert a | ...
In the case of an insert, we have
usersTable' = Insert user
which means that
userIds' can be reduced to
userIds' :: RedisSet' userIds' = SAdd (userId user)
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.