Partial application is not Schönfinkeling

The wages of pedantry

Automatic Redis Through Static Differentiation

| Comments

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:

1
2
3
4
5
6
7
8
9
10
11

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

-- 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:

1
2
3
4
5
6
7
8

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:

(Differentiate.hs) download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44

module Differentiate where

type Id = String

data Term p
  = Primitive p
  | Lambda Id (Term p)
  | App (Term p) (Term p)
  | Var Id
  deriving (Eq, Ord, Read, Show)

differentiate :: MonadId m => (p -> m (Term p)) -> Term p -> m (Term p)
differentiate differentiatePrimitive = diff where
  diff term =
    case term of
      Primitive p -> differentiatePrimitive p

      Lambda var term -> do
        let dvar = "d" ++ var
        rememberId var var $ generateId dvar $ \var' -> do
          term' <- rememberId dvar var' $ diff term
          return (Lambda var (Lambda var' term'))

      App s t -> do
        s' <- diff s

        -- t and t' will often share common sub-expressions.
        -- A better implementation would factor their commonalities out,
        -- to avoid redundant computation at runtime.
        t' <- diff t

        return (App (App s' t) t')

      Var var -> do
        var' <- recallId var
        return (Var var')

class Monad m => MonadId m where
  -- Return a unique string that starts with the given string.
  generateId :: String -> (String -> m a) -> m a
  -- Add mapping from old variable name to new variable name
  rememberId :: String -> String -> m a -> m a
  -- Lookup the new variable name that was mapped to the given old variable name.
  recallId :: String -> m String

Returning to an example from the first post:

1
2
3
4
5
6
7
8

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

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

1

usersTable' = Insert user

which means that userIds' can be reduced to

1
2

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.

Comments