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.

Automatic Redis, Part Two: Sorting and Data Structures

| Comments

This post is part of a sequence I am calling automatic redis, which is my attempt to solve the cache invalidation problem.

In my previous post, I demonstrated that a library could infer cache update operations from database insert operations by performing algebraic manipulations on the queries that define the cache keys. The algebraic laws needed were the distribution laws between monoids. e.g. count distributes over the Set monoid to produce the Sum monoid. A library could also infer the arguments of the cache keys (e.g. taskIds.{userId} -> taskIds.65495) by performing functional logical evaluation on the cache key’s query. If the library’s goal became suspended during evaluation, it could proceed by unifying expressions of low multiplicity with all possible values. For instance, if the goal for a filter query became suspended, the library could proceed by considering the true and false cases of the filter separately.

In this post I would like to talk about sorting and limiting, as well as flesh out some of the data structures that might be used in an automatic redis library.

Set

Set is the simplest data structure, and forms the foundation for two of our other collection types.

1

type Set a = Data.Set.Set

The monoidal operation for Set is simply set union.

List

List is a Set with an embedded sorting function. Tracking the sorting function enables us to compute redis sorted set keys if necessary.

1

data List a b = (Ord b) => List (a -> b) (Set a)

A commonly used sorting function would be x => x.modifiedDate.

The monoidal operation for List is the merge operation from merge-sort, with one restriction: the sorting functions of both lists must be the same sorting function.

LimitedList

LimitedList is a List with an upper bound on its size.

1

data LimitedList a b = (Ord b) => LimitedList Integer (List a b)

The length of the contained List must be less than or equal to the upper bound. Tracking the length enables us to know how to trim cache entries, e.g. when using the ZREMRANGEBYRANK command.

The monoidal operation for LimitedList is to merge-sort the two lists and truncate the result to the limit. Similarly to List, the library expects both lists to have the same upper limit.

First and Last

First and Last are essentially LimitedLists whose upper bound is 1. Making specialized types for singleton LimitedLists makes working with non-collection redis data structures easier.

1
2

data First a b = (Ord b) => First (a -> b) (Maybe a)
data Last  a b = (Ord b) => Last  (a -> b) (Maybe a)

Although First and Last have the same representation, they have different monoidal operations, namely (x,y) => x and (x,y) => y.

Maybe

The Maybe type is useful for queries that always generate a unique result (such as lookup by primary key), and as such the Maybe type does not need to contain a sorting function.

1

data Maybe a = Nothing | Just a

The monoidal operation is to pick Just over Nothing, but with the restriction that both arguments cannot be Justs.

1
2
3
4
5

instance Monoid Maybe where
  Nothing  `mappend` Nothing  = Nothing
  Nothing  `mappend` (Just x) = Just x
  (Just x) `mappend` Nothing  = Just x
  (Just x) `mappend` (Just y) = error "This should never happen."

Collision of Justs can happen if the application developer misuses the The operation (defined below). Unfortunately this error cannot be caught by an automatic redis library, because the library never actually computes the value of mappend. The library only tracks monoidal types so that it can know what the final redis commands will be.

Speaking of query operations, it’s about time I defined them. But first… one more monoid.

1
2
3
4

data Sum = Sum Integer

instance Monoid Sum where
  mappend = (+)

Query operations

Query operations are parameterized over an input type and an output type.

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

-- QO = Query Operation
data QO input output where
  -- The operations Where, Count, Sum, The, and SortBy are not concerned with the ordering
  -- of their input, so they can work on Sets, Lists, LimitedLists, Firsts, Lasts,
  -- and Maybes. In these constructor definitions, 'coll' can mean any of those types.
  -- A real implementation might have multiples versions of these query operations,
  --   e.g. WhereSet, WhereList, WhereLimitedList, ..., CountSet, CountList, etc.
  Where :: Expr (a -> Boolean) -> QO (coll a)       (coll a)
  Count ::                        QO (coll a)       Sum
  Sum   ::                        QO (coll Integer) Sum

  -- 'The' takes a collection which is expected to have no more than one element
  -- and extracts the element.
  The   :: QO (coll a) (Maybe a)

  -- SortBy converts any kind of collection into a List.
  SortBy :: (Ord b) => Expr (a -> b) -> QO (coll a) (List a)

  -- Limit, First, and Last, are defined for any (seq)uence:
  --   Lists, LimitedLists, Firsts, and Lasts.
  Limit :: Integer -> QO (seq a) (LimitedList a)
  First ::            QO (seq a) (First a)
  Last  ::            QO (seq a) (Last a)

  -- Mapping only works on Set!
  Select :: Expr (a -> b) -> QO (Set a) (Set b)

  -- Well technically Select also works on Maybe, but we'll make a separate
  -- query operation for Maybes.
  Apply :: Expr (a -> b) -> QO (Maybe a) (Maybe b)

  -- Lists contain their sorting function, so we cannot allow arbitrary
  -- mapping on lists. We can, however, support monotonic mappings.
  SelectMonotonic        :: Expr (a -> b)          -> QO (seq a) (seq b)

  -- Mappings which scramble the order are also allowed, as long as we
  -- have a way to recover the order. i.e. 'a -> c' has to be monotonic,
  -- even though 'a -> b' and 'b -> c' do not.
  SelectReversible       :: Expr (a -> b) -> Expr (b -> c) -> QO (seq a) (seq b)

A few more data structures and we will have all the pieces necessary for an application developer to define a cache schema.

1
2
3
4
5
6
7
8
9
10
11
12
13
14

data Table t = Table String

-- A Query is a sequence of query operations that begins with a table
data Query output where
  From :: Table t -> Query (Set t)
  Compose :: Query input -> QO input output -> Query output

-- convenience constructor
(+>) = Compose

data CacheKeyDefinition = CacheKeyDefinition {
  keyTemplate :: String, -- e.g. "taskIds.{userId}"
  query :: Query -- e.g. from tasks where task.userId = userId select task.id
}

Putting it all together, we can showcase the cache schema for a simple task management website.

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

type TaskId = String
type UserId = String

data Task = {
    taskId :: TaskId,
    ownerId :: UserId,
    title :: String,
    completed :: Boolean,
    dueDate :: Integer }
 deriving (Eq, Ord, Read, Show)

taskTable = Table "tasks" :: Table Task

schema = do
  -- The task objects.
  -- type: String
  -- expected redis commands on insert:
  --   SET
  "task.{taskId}" $= \tid ->
    From taskTable +>
    Where (\t -> taskId t == tid) +>
    The +>
    Apply show

  -- For each user, the ids of her most urgent tasks.
  -- type: Sorted Set, where the keys are the dueDate and the values are the taskIds.
  -- expected redis commands on insert:
  --   ZADD
  --   ZREMRANGEBYRANK
  "activeTaskIds.{userId}" $= \uid ->
    From taskTable +>
    Where (\t -> ownerId t == uid && not (completed t)) +>
    SortBy dueDate +>
    Limit 100 +>
    SelectReversible (\t -> (dueDate t, taskId t)) fst

  -- The number of tasks a user has successfully completed.
  -- type: integer
  -- expected redis commands on insert:
  --   INCR
  "numCompleted.{userId}" $= \uid ->
    From taskTable +>
    Where (\t -> ownerId t == uid && completed t) +>
    Count

It’s important to keep in mind that although I have made the above code look like haskell, no library in haskell could actually use the above code. The variables occuring after the $= sign are logic variables, not function parameters. An EDSL could get close to something like the above, but the normal types for == and && are unusable, and the lambdas inside the Where clauses would need to be reified anyway.

Still to come: deletes, updates, uniqueness constraints (maybe?), and psuedo-code for the generation of redis commands.

Automatic Redis, Part One: Inserts and Cache Key Extraction

| Comments

This post is part of a sequence I am calling automatic redis, which is my attempt to solve the cache invalidation problem.

These are some initial thoughts on how to automate cache updates. The question I want to answer is this: given a mapping from redis keys to the queries that produce their values, how can I infer which redis commands should be run when I add, remove, and update items in the collections which are my source of truth?

The code in this post is psuedo-haskell. What appears to the left of an = sign is not always a function, and the . is used for record field lookup as well as function composition.

I’ll start with a simple example. Suppose I run a website which is a task manager, and I want to display on my website the number of users who have signed up for an account. i.e. I want to display count users. I don’t want to count the entire collection every time I add an item to it, so instead I keep the count in redis, and increment it whenever a new account is created. Proving that INCR is the right command to send to redis is straightforward:

1
2
3
4
5

numUsers = count users
numUsers_new = count (users ++ [user])
numUsers_new = count users + count [user]
numUsers_new = numUsers + 1
-- INCR numUsers

Notice that when count distributes, it changes the plus operation from union (++) to addition (+).

Here is a similar example, this time storing the ids instead of a count.

1
2
3
4
5
6

userIds = map userId users
userIds_new = map userId (users ++ [user])
userIds_new = map userId users ++ map userId [user]
userIds_new = userIds ++ map userId [user]
userIds_new = userIds ++ [user.userId]
-- SADD userIds 65495

Obviously the appropriate redis command to use in this case is SADD.

Filtering is also straightforward.

1
2
3
4
5
6
7
8
9
10
11
12

activeUserIds = map userId (filter (\x -> x.status == ACTIVE) users)
activeUserIds_new = map userId (filter (\x -> x.status == ACTIVE) $
  (users ++
  [user]))
activeUserIds_new = map userId (
  filter (\x -> x.status == ACTIVE) users ++
  filter (\x -> x.status == ACTIVE) [user])
activeUserIds_new =
  map userId (filter (\x -> x.status == ACTIVE) users) ++
  map userId (filter (\x -> x.status == ACTIVE) [user])
activeUserIds_new = activeUserIds ++ map userId (filter (\x -> x.status == ACTIVE) [user])
-- SADD activeUserIds 65495

Obviously a pipeline of SADDs will be correct, and the expression to the right of the ++ gives my automatic cache system a procedure for determining which SADD operations to perform. When the cache system gets the user object to be added, it will learn that the number of SADD operations is either zero or one, but it doesn’t have to know that ahead of time.

A computer can easily verify the above three proofs, as long as they are properly annotated. But can I get the computer to create the proof in the first place?

Rewriting the activeUserIds example to use function composition suggests one approach.

1
2

activeUserIds = (map userId . filter (\x -> x.status == ACTIVE)) users
activeUserIds_new = activeUserIds ++ (map userId . filter (\x -> x.status == ACTIVE)) [user]

In general, it seems that queries of the form

1

values = (f . g . h {- ... -}) entities

become

1

values_new = values `mappend` (f . g . h {- ... -}) [entity]

provided f, g, h, etc. all distribute over mappend. The actual value of mappend will determine which redis operation to perform. Integer addition becomes INCR, set union becomes SADD, sorted set union becomes ZADD, list concatenation becomes LPUSH or RPUSH, etc. An important monoid which may not be obvious is the Last monoid (mappend x y = y), which becomes SET.

So much for updates on constant cache keys. Parameterized cache keys are much more interesting.

On my task manager website, I want to have one cache entry per user. The user’s id will determine the cache key that I use.

1

taskIds_'userId' = (map taskId . filter (\t -> t.owner == userId)) tasks

It’s tempting to think of this definition as a function:

1

taskIds :: UserId -> [TaskId]

But an automatic caching system will not benefit from this perspective. From it’s perspective, the input is a task object, and the output is any number of redis commands. The system has to implicitly discover the userId from the task object it receives. The userId parameter of taskIds.{userId} is therefore more like a logic variable (e.g. from prolog) than a variable in imperative or functional languages.

The monoidal shortcut rule is still valid for parameterized redis keys.

1
2

taskIds_'userId'_new = taskIds_'userId' ++
  (map taskId . filter (\t -> t.owner == userId)) [task]

The caching system does not need to reduce this expression further, until it receives the task object. When it does, it can evaluate the addend as an expression in a functional-logical language (similar to Curry).

1
2
3
4
5
6
7
8
9
10
11
12

taskIds_'userId'_new = taskIds_'userId' ++
  (map taskId . filter (\t -> t.owner == userId)) [task]
taskIds_'userId'_new = taskIds_'userId' ++
  (map taskId (filter (\t -> t.owner == userId) [task]))
taskIds_'userId'_new = taskIds_'userId' ++
  (map taskId (if (\t -> t.owner == userId) task then
    task : filter (\t -> t.owner == userId) [] else
           filter (\t -> t.owner == userId) []))
taskIds_'userId'_new = taskIds_'userId' ++
  (map taskId (if task.owner == userId then
    task : filter (\t -> t.owner == userId) [] else
           filter (\t -> t.owner == userId) []))

Unfortunately at this point the goal becomes suspended. The cache system can cheat a little by unifying task.owner == userId with True and False.

In the true case, userId unifies with task.owner, which I’ll say is 65495:

1
2
3
4
5
6
7
8
9
10
11
12
13

taskIds_65495_new = taskIds_65495 ++ (map taskId $
  if 65495 == 65495 then
    task : filter (\t -> t.owner == userId) [] else
           filter (\t -> t.owner == userId) [])
taskIds_65495_new = taskIds_65495 ++ (map taskId $
  if true then
    task : filter (\t -> t.owner == userId) [] else
           filter (\t -> t.owner == userId) [])
taskIds_65495_new = taskIds_65495 ++ (map taskId $
  task : filter (\t -> t.owner == userId) [])
taskIds_65495_new = taskIds_65495 ++ (map taskId [task])
taskIds_65495_new = taskIds_65495 ++ task.id
-- SADD taskIds_65495 ${task.id}

In the false case, userId remains unbound, but that’s ok, because the expression reduces to a no-op:

1
2
3
4
5
6
7
8
9
10

taskIds_'userId'_new = taskIds_'userId' ++
  (map taskId (if false then
    task : filter (\t -> t.owner == userId) [] else
           filter (\t -> t.owner == userId) []))
taskIds_'userId'_new = taskIds_'userId' ++
  (map taskId (filter (\t -> t.owner == userId) []))
taskIds_'userId'_new = taskIds_'userId' ++
  (map taskId [])
taskIds_'userId'_new = taskIds_'userId' ++ []
-- nothing to do

In general, whenever the cache system’s goals become suspended, it can resume narrowing/residuation by picking a subexpression with low multiplicity (e.g. booleans, enums) and nondeterministically unifying it with all possible values.

Most of the time, each unification will result in either a no-op, or a redis command with all parameters bound. An exception (are there others?) is queries which affect an inifinite number of redis keys, e.g. caching all tasks that do NOT belong to a user.

1

taskIds_'userId' = (map taskId . (filter (\t -> t.owner != userId))) tasks

This is clearly a bug, so the caching system can just log an error and perform no cache updates. It may even be possible for the caching system to catch the bug at compile time by letting the inserted entity (e.g. a task) be an unbound variable, and seeing if a non-degenerate redis command with unbound redis key parameters can be produced.

This post has focused mostly on inserts and queries that fit the monoidal pattern. In another post I’ll take a look at deletes and queries which are not so straightforward.

The Hundred-Year Function

| Comments

What will programming languages look like one hundred years from now? Where will all of those wasted cycles end up going?

I think it is safe to say that the programming language of the future, if it exists at all, will involve some kind of artificial intelligence. This post is about why I think that theorem provers will be standard in languages of the future.

The hundred year function
1

solve :: (a -> Bool) -> Size -> Random (Maybe a)

This simple function takes two arguments. The first is a predicate distinguishing between desirable (True) and undesirable (False) values for A. The second is a size restriction on A (e.g. number of bytes).

The function returns a random value of A, if one exists, meeting two constraints:

  1. It satisfies the predicate.
  2. It is no larger than the size constraint.

Also, the solve function is guaranteed to terminate whenever the predicate terminates.

First I will try to convince you that the solve function is more important than any of your petty opinions about syntax, object-orientation, type theory, or macros. After that I will make a fool of myself by explaining how to build the solve function with today’s technology.

Why it matters

It can find fix-points:

“Put down fahrenheit,” said the explorer. “I don’t expect it to matter.”
1
2
3
4
5
6
7

def c2f(temp):
  return temp * 9.0 / 5 + 32

def is_fixpoint(temp):
  return temp == c2f(temp)

print solve(is_fixpoint, 8) # outputs -40.0

It can invert functions:

Crazy Canadians think 37 is hot.
1
2
3
4

def f2c(temp):
  return (temp - 32) * 5 / 9.0

print solve(lambda fahr: 37.0 == f2c(fahr), 8) # 100.0 IS hot!

It can solve Project Euler problems:

Problem 9
1
2
3
4
5
6
7
8
9
10

def is_pythagorean_triple(a, b, c):
  return a*a + b*b == c*c

def is_solution(triple):
  if len(triple) != 3: return False
  if sum(triple) != 1000: return False
  if !is_pythagorean_triple(*triple): return False
  return True

print solve(is_solution, 12)

It can check that two functions are equal:

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

def the_obvious_max_subarray(A):
  answer = 0
  for start in range(0, len(A) - 1):
    for end in range(start + 1, len(A)):
      answer = max(answer, sum(A[start:end]))
  return answer

def the_fast_max_subarray(A):
  max_ending_here = max_so_far = 0
  for x in A:
    max_ending_here = max(x, max_ending_here + x)
    max_so_far = max(max_so_far, max_ending_here)
  return max_so_far

def differentiates(input):
  return the_obvious_max_subarray(input) != the_fast_max_subarray(input)

# Prints None if the two functions are equal for all
#   input sequences of length 5 and smaller.
# Otherwise prints a counter-example.
print solve(differentiates, 4 * 5)

So it’s useful for detecting the introduction of bugs when you are optimizing things.

In fact, the solve function can find a more efficient implementation on your behalf.

My computer is smarter than Kadane, if you’ll just be patient.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

def steps(algorithm, input):
  (_result, steps) = eval_with_steps(algorithm, input)
  return steps

def is_fast_max_subarray(algorithm):
  # Check that algorithm is equivalent to the_obvious_max_subarray
  if solve(lambda input: the_obvious_max_subarray(input) != eval(algorithm, input), 4 * 5):
    return False
  # Check that algorithm is faster than the_obvious_max_subarray
  for example in example_inputs:
    if steps(algorithm, input) > steps(the_obvious_max_subarray, input):
      return False
  return True

print solve(is_fast_max_subarray, 1000) # prints a function definition

The speed check is crude, but the idea is there.

Keeping the size constraint reasonable prevents the solve function from just creating a giant table mapping inputs to outputs.

Curry and Howard tell us that programs and proofs are one and the same thing. If our solve function can generate programs, then it can also generate mathematical proofs.

Ten years too late for Uncle Petros
1
2
3
4
5
6
7
8
9
10
11

goldbach = parse("forall a > 2: exists b c: even(a) => prime(b) && prime(c) && b + c == a")

def proves_goldbach(proof):
  if proof[-1] != goldbach:
    return False
  for step in range(0, len(proof) - 1):
    if not proof[step].follows_from(proof[0:step]):
      return False
  return True

print solve(proves_goldbach, 10000)

If the proof is ugly, we can decrease the search size, and we will get a more elegant proof.

The solve function can find bugs:

Like fuzz testing, but more exhaustive
1
2
3
4
5

def does_not_go_wrong(input):
  result = eval(my_program, input)
  return not is_uncaught_exception(result)

print solve(does_not_go_wrong, 10000)

The solve function will never get people to stop arguing, but it will at least change the dynamic vs static types argument from a pragmatic one to an artistic one.

One last example:

Test-driven development advocates writing tests which are sufficient to construct the missing parts of a program. So why write the program at all?

Beck’s revenge
1
2
3
4
5
6
7
8

def passes_tests(patches):
  return unit_tests.pass(partial_program.with(patches))

patches = solve(passes_tests, 10000)
if patches:
  print partial_program.with(patches)
else
  print "Tests not passable within search space"

In fact, unit_tests can be replaced with any assertion about the desired program: e.g. that it type checks under Hindley-Milner, that it terminates within a certain number of steps, that it does not deadlock within the first X cycles of the program’s execution, and so on.

Are you excited yet? Programming in the future is awesome!

Implementation

Always start with the obvious approach:

Exhaustive search
1
2
3
4
5

def solve(predicate, size):
  for num in range(0, 2 ^ (size * 8) - 1):
    val = decode(num)
    if predicate(val):
      return val

Correct, but useless. If the predicate consisted of only one floating point operation, the Sequoia supercomputer would take 17 minutes to solve a mere 8 bytes.

The complexity of solve is clear. The variable num can be non-deterministically chosen from the range in linear time (size * 8), decode takes linear time, and predicate takes polynomial time in most of our examples from above. So solve is usually in NP, and no worse than NP-complete as long as our predicate is in P.

It’s a hard problem. Were you surprised? Or did you get suspicious when the programmers of the future started exemplifying godlike powers?1

Thankfully, a lot of work has been put into solving hard problems.

Today’s sat solvers can solve problems with 10 million variables. That’s 1.2 megabytes of search space, which is large enough for almost all of the examples above, if we’re clever enough. (The Kadane example is the definite exception, since the predicate takes superpolynomial time.)

The Cook-Levin theorem gives us a procedure for writing the solve function more efficiently.

  1. Imagine a large number of processors, each with its own memory, lined up and connected so that the output state of each processor and memory becomes the input state of the next processor and memory. The state of the entire assembly is determined solely by the state of the first processor. The state of the whole system is static.
  2. Represent each (unchanging) bit in the assembly with a boolean variable, and generate constraints on those variables by examining the logic gates connecting the bits.
  3. Assign values to some of the variables in a way that corresponds to the first processor containing the machine code of the predicate.
  4. Likewise, assign values so that the accumulator register of the last processor contains the value True.
  5. Apply a sat solver to the variables and their constraints.
  6. Extrapolate a solution by examining the first processor’s total state.

I call this approach “solving the interpreter trace” because the imaginary processors act as an interpreter for the predicate, and we ask the sat solver to trace out the processor execution.

The approach is elegant, but it has three major problems:

  1. The formula given to the sat solver is enormous, even for small predicates and input sizes. (It’s polynomial, but the coefficient is large.)
  2. The formula is highly symmetrical, which means the sat solver will perform a lot of redundant computation.
  3. The meaning of bits in later processors is highly dependent on the value of bits in earlier processors (especially if the predicate starts off with a loop). This will force our sat solver to work a problem from beginning to end, even when a different order (such as end to beginning) would be more intelligent.

We can get rid of these problems if we compile our predicate directly into a boolean formula. Compilation is easy enough if our predicate contains neither loops nor conditionals.

An example without loops or branches
1
2
3
4
5
6

def isReadableAndWriteable(x):
  y = x & 4
  z = x & 2
  a = y == 4
  b = z == 2
  return a && b

becomes

The sat formula, assuming 3-bit values.
1
2
3
4
5

(y0 == x0 & 0) & (y1 == x1 & 0) & (y2 == x2 & 1) &
(z0 == x0 & 0) & (z1 == x1 & 1) & (z2 == x2 & 0) &
(a == ((y0 == 0) & (y1 == 0) & (y2 == 1)) &
(b == ((z0 == 0) & (z1 == 1) & (z2 == 0)) &
a && b

Actually conditionals aren’t that hard either

A contrived branching example
1
2
3
4
5
6
7
8

def predicate(x):
  b = isEven(x)
  if b:
    w = x & 7
  else:
    z = x & 2
    w = z << 1
  return w < 3

becomes

The sat formula, again assuming 3-bit values.
1
2
3
4
5

(b == (x0 == 0)) &
(b -> ((w0 == (x0 & 1)) & (w1 == (x1 & 1)) & (w2 == (x2 & 1)))) &
(~b -> ((z0 == (x0 & 0)) & (z1 == (x1 & 1)) & (z2 == (x2 & 0)))) &
(~b -> ((w0 == 0) & (w1 == z0) & (w2 == z1))) &
(w2 == 0 & (w1 == 0 | w0 == 0))

A sat solver would immediately assign w2 the value 0. If we were solving over an interpretational trace, w2 wouldn’t be a single variable, but would be one of two variables depending on whether b was True or False.

By compiling the predicate, we have enabled the solver to work from end to beginning (if it so chooses).

Can we handle loops?

A six is a
1
2
3
4
5
6
7
8

def is_palindrome(str):
  i = 0
  j = len(str) - 1
  while i < j:
    if str[i] != str[j]: return False
    i += 1
    j -= 1
  return True

One approach is to unroll the loop a finite number of times.

A six is a six is a six is a
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

def is_palindrome(str):
  i = 0
  j = len(str) - 1
  if i < j:
    if str[i] != str[j]: return False
    i += 1
    j -= 1
    if i < j:
      if str[i] != str[j]: return False
      i += 1
      j -= 1
      if i < j:
        if str[i] != str[j]: return False
        i += 1
        j -= 1
        if i < j:
          _longer_loop_needed = True
          i = arbitrary_value() # in case rest of function depends on i or j
          j = arbitrary_value() # (It doesn't in this example.)
  return True

With branching and conditionals, we are turing complete. Function calls can be in-lined up until recursion. Tail recursive calls can be changed to while loops, and the rest can be reified as loops around stack objects with explicit push and pop operations. These stack objects will introduce symmetry into our sat formulas, but at least it will be contained.

When solving, we assume the loops make very few iterations, and increase our unroll depth as that assumption is violated. The solver might then look something like this:

Solver for a predicate with one loop
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

def solve(predicate, size):
  unroll_count = 1
  sat_solver = SatSolver()
  limit = max_unroll_count(predicate, size)
  while True:
    unrolled = unroll_loop(predicate, unroll_count)
    formula = compile(unrolled)
    sat_solver.push(formula)
    sat_solver.push("_longer_loop_needed == 0")
    sol = sat_solver.solve()
    if sol: return sol
    sat_solver.pop()
    sol = sat_solver.solve()
    if sol == None: return None # even unrolling more iterations won't help us
    sat_solver.pop()
    if unroll_count == limit: return None
    unroll_count = min(unroll_count * 2, limit)

max_unroll_count does static analysis to figure out the maximum number of unrolls that are needed. The number of unrolls will either be a constant (and so can be found out by doing constant reduction within the predicate), or it will somehow depend on the size of the predicate argument (and so an upper bound can be found by doing inference on the predicate).

The solver is biased toward finding solutions that use fewer loop iterations, since each loop iteration sets another boolean variable to 1, and thus cuts the solution space down by half. If the solver finds a solution, then we return it. If not, then we try again, this time allowing _longer_loop_needed to be true. If it still can’t find a solution, then we know no solution exists, since i and j were set to arbitrary values. By “arbitrary”, I mean that, at compilation time, no constraints will connect the later usages of i and j (there are none in this example) with the earlier usages.

I admit that this approach is ugly, but the alternative, solving an interpreter trace, is even more expensive. The hacks are worth it, at least until somebody proves P == NP.

Some of the examples I gave in the first section used eval. Partial evaluation techniques can be used to make these examples more tractable.

I’ve only talked about sat solvers. You can probably get better results with an smt solver or a domain-specific constraint solver.

In thinking about this problem, I’ve realized that there are several parallels between compilers and sat solvers. Constant reduction in a compiler does the same work as the unit clause heuristic in a sat solver. Dead code removal corresponds to early termination. Partial evaluation reduces the need for symmetry breaking. Memoization corresponds to clause learning. Is there a name for this correspondance? Do compilers have an analogue for the pure symbol heuristic? Do sat solvers have an analogue for attribute grammars?

Today

If you want to use languages which are on the evolutionary path toward the language of the future, you should consider C# 4.0, since it is the only mainstream language I know of that comes with a built-in theorem prover.

Update (2013-11-24):

I am happy to report that I am not alone in having these ideas. “Search-assisted programming”, “solver aided languages”, “computer augmented programming”, and “satisfiability based inductive program synthesis” are some of the names used to describe these techniques. Emily Torlak has developed an exciting language called Rosette, which is a dsl for creating solver aided languages. Ras Bodik has also done much work combining constraint solvers and programming languages. The ExCAPE project focuses on program synthesis. Thanks to Jimmy Koppel for letting me know these people exist.

1: Even many computer scientists do not seem to appreciate how different the world would be if we could solve NP-complete problems efficiently. I have heard it said, with a straight face, that a proof of P = NP would be important because it would let airlines schedule their flights better, or shipping companies pack more boxes in their trucks! One person who did understand was Gödel. In his celebrated 1956 letter to von Neumann, in which he first raised the P versus NP question, Gödel says that a linear or quadratic-time procedure for what we now call NP-complete problems would have “consequences of the greatest magnitude.” For such a procedure “would clearly indicate that, despite the unsolvability of the Entscheidungsproblem, the mental effort of the mathematician in the case of yes-or-no questions could be completely replaced by machines.” But it would indicate even more. If such a procedure existed, then we could quickly find the smallest Boolean circuits that output (say) a table of historical stock market data, or the human genome, or the complete works of Shakespeare. It seems entirely conceivable that, by analyzing these circuits, we could make an easy fortune on Wall Street, or retrace evolution, or even generate Shakespeare’s 38th play. For broadly speaking, that which we can compress we can understand, and that which we can understand we can predict. — Scott Aaronson

Foreach Mutation

| Comments

Many languages have adopted some form of the “foreach” keyword, for traversing elements of a collection. The advantages are obvious: fencepost errors are impossible, and programs are easier to read. Foreach loops are not places where I expect to find bugs. But about a month ago, I found one, in a piece of code similar to the code below. The expected behavior of the program is to print out the numbers zero and one, on separate lines. Do not read past the end of the program if you want to find the bug yourself, because I explain it below.

(foreach.py) download
1
2
3
4
5
6
7
8
9
10

nums = [0, 1]
numclosures = []
for num in nums:
    numclosures.append(lambda: num)
for numclosure in numclosures:
    print numclosure()

# output from Python 2.5.2
# 1
# 1

The solution has to do with the implementation of the for loop in python. (I ran the program in cpython; it may be interesting to see what other implementations of python do.) Rather than creating a new binding for the num variable on every iteration of the loop, the num variable is mutated (probably for efficiency or just simplicity of implementation). Thus, even though numclosures is filled with distinct anonymous functions, they both refer to the same instance of num.

I tried writing similar routines in other languages. Ruby and C# do the same thing as Python:

(foreach.rb) download
1
2
3
4
5
6
7
8
9
10
11
12

nums = Array[0, 1]
numclosures = Array.new
for num in nums
    numclosures.push lambda { return num }
end
for numclosure in numclosures
    print numclosure.call, "\n"
end

# output from Ruby1.8
# 1
# 1
(foreach.cs) 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

using System;
using System.Collections.Generic;

public static class Foreach
{
    public delegate int NumClosure(); // Func<int> does not exist in the latest Mono???

    public static void Main()
    {
        int[] nums = new int[] { 0, 1 };
        List<NumClosure> numclosures = new List<NumClosure>();
        foreach (int num in nums)
        {
            numclosures.Add(delegate() { return num; });
        }
        foreach (NumClosure numclosure in numclosures)
        {
            Console.WriteLine(numclosure());
        }
    }
}

// output from Mono 1.2.6
// 1
// 1

Please excuse the use of the NumClosure delegate. For some reason I could not get Mono to compile with Func.

Fortunately, all of these languages provide some kind of work-around. Ruby has Array#each, and C# has List<>.ForEach. Python has the map built-in.

(foreach_rebind.py) download
1
2
3
4
5
6
7
8
9
10
11

nums = [0, 1]
numclosures = []
def body(num):
    numclosures.append(lambda: num)
map(body, nums)
for numclosure in numclosures:
    print numclosure()

# output from Python 2.5.2
# 0
# 1
(foreach_rebind.rb) download
1
2
3
4
5
6
7
8
9
10
11
12

nums = Array[0, 1]
numclosures = Array.new
nums.each { |num|
    numclosures.push lambda { return num }
}
for numclosure in numclosures
    print numclosure.call, "\n"
end

# output from Ruby1.8:
# 0
# 1
(foreach_rebind.cs) 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

using System;
using System.Collections.Generic;

public static class Foreach
{
    public delegate int NumClosure(); // Func<int> does not exist in the latest Mono???

    public static void Main()
    {
        int[] nums = new int[] { 0, 1 };
        List<NumClosure> numclosures = new List<NumClosure>();
        new List<int>(nums).ForEach(delegate (int num)
        {
            numclosures.Add(delegate() { return num; });
        });
        foreach (NumClosure numclosure in numclosures)
        {
            Console.WriteLine(numclosure());
        }
    }
}

// output from Mono 1.2.6
// 0
// 1

Not everybody mutates their enumerators, however. Lisp, the language which normally requires every programmer to be an expert in variable scoping, handles iteration very cleanly:

(foreach.cl) download
1
2
3
4
5
6
7
8
9
10
11

(let ((nums (list 0 1))
      (numclosures (list)))
  (progn
    (dolist (num nums)
      (push #'(lambda () num) numclosures))
    (dolist (numclosure numclosures)
      (format t "~a~%" (funcall numclosure)))))

; output from SBCL 1.0.11.debian
; 1
; 0

And despite its messy syntax, Perl also scores a 10 for clean variable semantics:

(foreach.pl) download
1
2
3
4
5
6
7
8
9
10
11
12

my @nums = (0, 1);
my @numclosures = ();
for my $num (@nums) {
  push (@numclosures, sub { return $num; });
}
for my $numclosure (@numclosures) {
  print &$numclosure() . "\n";
}

# output from Perl 5.8.8:
# 0
# 1

Faking Continuation Based Web Serving Using Exceptions

| Comments

A friend has pointed out to me that the command line and web interface in my last post do not need to interact with the main game through an iterator. He proposed that the web interface could pause the execution of the game by using exceptions. I played with the idea, and discovered that he was right. The upshot is that continuation-based web serving can be faked in any language which has exceptions. (Lexical closures are also helpful, but can also be faked using objects.) The approach given below relies on neither CPS nor monads, and so has the added advantage of being fairly idiomatic in most mainstream languages.

As before, our game is the children’s “Guess a number between 1 and 100” game:

(game.py) 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

import random

rgen = random.Random()

class RandomNumberGame(object):
    def __init__(self, interface):
        self.interface = interface

    def start_game(self):
        name = self.interface.prompt_string(
                "Greetings. What is your name? ")
        self.interface.display("Hello, %s." % (name,))

        self.__play_game()

    def __play_game(self):
        self.interface.display("I am thinking of a number between 1 and 100.")
        my_number = self.interface.get(lambda: rgen.randint(1,100))
        num_guesses = 0
        while True:
            user_number = self.interface.prompt_int("Guess: ")
            num_guesses += 1
            if my_number == user_number:
                break
            elif my_number < user_number:
                self.interface.display("Try lower.")
            else:
                self.interface.display("Try higher.")

        self.interface.display("Correct in %s guesses." % num_guesses)
        play_again = self.interface.prompt_yes_no("Play again? ")

        if play_again:
            self.__play_game()
        else:
            self.interface.display("Thank you for playing.")

I like this version much better because the ugly wart of before:

The trouble with calling a generator from a generator
1
2
3
4
5
6
7
8

# The coroutine equivalent of self.__play_game()
iter = self.__play_game()
try:
    y = yield iter.next()
    while True:
        y = yield iter.send(y)
except StopIteration:
    pass

has been simplified to:

Regular method invocation
1

self.__play_game()

The interface between the game and the user interface is the same as before, with one addition:

Interface
1
2
3
4
5
6

display(text)       # displays the given text to the user and returns None
prompt_string(text) # displays the given text to the user and returns a string input by the user
prompt_int(text)    # display the given text to the user and returns an int input by the user
prompt_yes_no(text) # display the given text to the user and returns True for yes and False for no

get(callback)       # invokes the callback and returns what it returns

The new method “get” is made use of in the game when generating the answer for the game:

Get usage
1

my_number = self.interface.get(lambda: rgen.randint(1,100))

Retrieving the random number through self.interface.get ensures that the game will not be constantly changing its answer while a user is playing through the web interface.

As before, the command line interface is very simple:

(cli.py) 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

#!/usr/bin/env python

class CommandLineInterface:
    def __init__(self, routine):
        self.routine = routine(self)

    def run(self):
        self.routine.start_game()

    def get(self, f):
        return f()

    def display(self, prompt):
        print prompt

    def prompt_string(self, prompt):
        return raw_input(prompt)

    def prompt_int(self, prompt):
        return int(raw_input(prompt))

    def prompt_yes_no(self, prompt):
        response = raw_input(prompt)
        return response.startswith('y') or response.startswith('Y')

if __name__=="__main__":
    from game import RandomNumberGame
    cmd = CommandLineInterface(RandomNumberGame)
    cmd.run()

The web interface works by raising a StopWebInterface exception when execution of the game needs to be paused so that the user can input some data into a form. Our abstraction is thus slightly leaky, in that a game which at some point generically caught all types of exceptions might interfere with the behavior of the web interface. The yield lambda solution did not have this problem.

(web.py) 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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141

#!/usr/bin/env python

import cgi
from wsgiref.simple_server import make_server

# Everytime we generate an html page, we create a hidden input element
# with this name. It lets us know which saved history must be resumed
# in order to continue the program.
HISTORY_FORM_NAME = 'WebInterface_history_index'

class History(object):
    """A record of past values returned by the routine. Useful for playback.
       self.get_pending is a function which takes a dictionary like object
           corresponding to the POST variables, and returns the new value
           to be added to the history.
       self.old_values is all of the results of functions yielded by the routine.
       """
    def __init__(self, get_pending, old_values):
        self.get_pending = get_pending
        self.old_values = old_values

class StopWebInterface(Exception):
    def __init__(self, get_pending):
        self.get_pending = get_pending

class WebInterface(object):
    """WebInterface wraps around a routine class to allow for the routine to
       be executed through a browser. It works by remembering the results
       of functions that were yielded by the routine. In order to pick up
       where it left off, the routine is re-run with the remembered values,
       a new value is parsed from the POST variables, and the routine keeps
       running until it reaches another prompt."""
    def __init__(self, routine_class):
        self.routine_class = routine_class
        self.histories = [History(None, [])]

    def respond(self, environ, start_response):
        responder = WebInterface.Response(self, environ, start_response)
        return responder.respond()

    class Response:
        """The Response class is instantiated for every HTTP request.
           It grabs the appropriate history according to the value in the POST
           variable 'WebInterface_history_index'. Using that history, it
           re-runs the routine with the contained old_values, parses the POST
           variables for any new values using get_pending, and continues the
           routine until it needs to make another request. For simplicity,
           it modifies web_interface.histories directly. A real
           implementation would need to protect this variable using locks
           (or find a mutation-free solution), since it is possible for
           the wsgi server to make concurrent calls to WebInterface.respond.
           """
        def __init__(self, web_interface, environ, start_response):
            self.web_interface = web_interface
            self.environ = environ
            self.start_response = start_response

        def respond(self):
            routine = self.web_interface.routine_class(self)
            self.form = cgi.FieldStorage(fp=self.environ['wsgi.input'],environ=self.environ)
            history_index = int(self.form.getvalue(HISTORY_FORM_NAME, default="0"))
            if len(self.web_interface.histories) <= history_index:
                self.start_response('412 Cannot read the future', [('Content-type', 'text/html')])
                return ["That history has not yet been written."]

            # Copy the history in order to create a new history.
            history_orig = self.web_interface.histories[history_index]
            self.history = History(history_orig.get_pending, history_orig.old_values[:])
            self.start_response('200 OK', [('Content-type', 'text/html')])
            self.output = [ '<form method="POST">\n' ]

            self.paused = False
            self.iter = self.iterate_old_values()
            try:
                routine.start_game()
            except StopWebInterface, inst:
                self.history.get_pending = inst.get_pending

            self.web_interface.histories.append(self.history)
            self.output += '<input type="hidden" name="%s" value="%s">\n' % (HISTORY_FORM_NAME, len(self.web_interface.histories) - 1)
            self.output += '</form>\n'
            return self.output

        def iterate_old_values(self):
            for val in self.history.old_values:
                yield val
            if self.history.get_pending != None:
                val = self.history.get_pending(self)
                self.history.old_values.append(val)
                yield val

        def get(self, f):
            try:
                return self.iter.next()
            except StopIteration:
                val = f()
                self.history.old_values.append(val)
                return val

        def display(self, str):
            try:
                return self.iter.next()
            except StopIteration:
                self.output += str + "<br/>\n"
                self.history.old_values.append(None)

        def prompt_string(self, prompt):
            return self.prompt_type(prompt, str)

        def prompt_int(self, prompt):
            return self.prompt_type(prompt, int)

        def prompt_yes_no(self, prompt):
            return self.prompt_and_pause(
                    prompt,
                    [("submit", "btn_yes", "Yes"), ("submit", "btn_no", "No")],
                    lambda form: form.has_key('btn_yes'))

        def prompt_type(self, prompt, type_parse):
            return self.prompt_and_pause(
                    prompt,
                    [("text", "prompt", ""), ("submit", "btn_submit", "Enter")],
                    lambda form: type_parse(form["prompt"].value))

        def prompt_and_pause(self, prompt, inputs, parse_form):
            try:
                val = self.iter.next()
                return val
            except StopIteration:
                self.output += prompt
                for input in inputs:
                    self.output += '<input type="%s" name="%s" value="%s">\n' % input
                def read_from_form(responder):
                    return parse_form(responder.form)
                raise StopWebInterface(read_from_form)

if __name__=="__main__":
    from game import RandomNumberGame
    interface = WebInterface(RandomNumberGame)
    httpd = make_server('', 8000, interface.respond)
    httpd.serve_forever()

De-coupling Interfaces With ‘Yield Lambda’

| Comments

Though separation of concerns may be the most important design principle in software, its effective implementation is often elusive. A common problem in web design is how to link a sequence of pages together without scattering their logic all over the application. While this problem has been almost completely solved by continuation based web servers, not every language supports continuations. There is a middle ground however: coroutines. This post describes a light-weight approach to doing continuation-style web programming using Python’s coroutines.

Our target application will be the following “guess a number” game.

(simple.py) 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

#!/usr/bin/env python

import random

rgen = random.Random()

def start_game():
    name = raw_input("Greetings. What is your name? ")
    print "Hello, %s." % (name,)

    play_game()

def play_game():
    print "I am thinking of a number between 1 and 100."
    my_number = rgen.randint(1,100)
    num_guesses = 0
    while True:
        user_number = int(raw_input("Guess: "))
        num_guesses += 1
        if my_number == user_number:
            break
        elif my_number < user_number:
            print "Try lower."
        else:
            print "Try higher."

    print "Correct in %s guesses." % num_guesses
    play_again = raw_input("Play again? ")

    if play_again.startswith('y') or play_again.startswith('Y'):
        play_game()
    else:
        print "Thank you for playing."

if __name__=="__main__":
    start_game()

Here is what the program looks like using coroutines:

(game.py) 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
45
46
47
48
49
50

import random

rgen = random.Random()

class RandomNumberGame(object):
    def __init__(self, interface):
        self.interface = interface

    def __iter__(self):
        name = yield lambda: self.interface.prompt_string(
                "Greetings. What is your name? ")
        yield lambda: self.interface.display("Hello, %s." % (name,))

        # The coroutine equivalent of self.__play_game()
        iter = self.__play_game()
        try:
            y = yield iter.next()
            while True:
                y = yield iter.send(y)
        except StopIteration:
            pass

    def __play_game(self):
        yield lambda: self.interface.display("I am thinking of a number between 1 and 100.")
        my_number = yield lambda: rgen.randint(1,100)
        num_guesses = 0
        while True:
            user_number = yield lambda: self.interface.prompt_int("Guess: ")
            num_guesses += 1
            if my_number == user_number:
                break
            elif my_number < user_number:
                yield lambda: self.interface.display("Try lower.")
            else:
                yield lambda: self.interface.display("Try higher.")

        yield lambda: self.interface.display("Correct in %s guesses." % num_guesses)
        play_again = yield lambda: self.interface.prompt_yes_no("Play again? ")

        if play_again:
            # The coroutine equivalent of self.__play_game()
            iter = self.__play_game()
            try:
                y = yield iter.next()
                while True:
                    y = yield iter.send(y)
            except StopIteration:
                pass
        else:
            yield lambda: self.interface.display("Thank you for playing.")

Essentially, all read and write actions with the outside world have been replaced with the yield lambda pattern. That includes the call to rgen.randint, because rgen has been initialized according to the current time.

All we need now is an interface that implements the following methods:

Interface
1
2
3
4
5
6
7
8
9
10
11

# displays the given text to the user and returns None
interface.display(text)

# displays the given text to the user and returns a string input by the user
interface.prompt_string(text)

# display the given text to the user and returns an int input by the user
interface.prompt_int(text)

# display the given text to the user and returns True for yes and False for no
interface.prompt_yes_no(text)

We’ll start with the simpler command line version:

(cli.py) 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

#!/usr/bin/env python

class CommandLineInterface(object):
    def __init__(self, routine):
        self.routine = routine(self)

    def run(self):
        iter = self.routine.__iter__()
        try:
            action = iter.next()
            while True:
                action = iter.send(action())
        except StopIteration:
            pass

    def display(self, prompt):
        print prompt

    def prompt_string(self, prompt):
        return raw_input(prompt)

    def prompt_int(self, prompt):
        return int(raw_input(prompt))

    def prompt_yes_no(self, prompt):
        response = raw_input(prompt)
        return response.startswith('y') or response.startswith('Y')

if __name__=="__main__":
    from game import RandomNumberGame
    cmd = CommandLineInterface(RandomNumberGame)
    cmd.run()

The behavior of cli.py + game.py is completely identical to simple.py. Remarkably, though, the core logic of the game (in game.py) is now re-usable with any user interface supporting the four methods given above.

A typical web-MVC-style solution to the “guess a number” game would probably have a controller which dispatched on one of three different situations: the user has input her name, the user has input a guess, or the user has told us whether or not she would like to keep playing. The three different situations would likely be represented as distinct URIs. In our game.py, however, a situation corresponds to the “yield lambda” at which execution has been paused.

The essential idea to writing a coroutine-based web interface is this: only run the game routine up to the point where more information is needed. Store the result of every lambda yielded so far. On successive page requests, replay the routine with the stored results, but only invoke the lambdas that were not invoked on a previous page request. The medium for storing the results of the lambdas does not matter. It could be embedded in hidden input elements in HTML (though this raises issues of trust), or stored in a database tied to a session ID. For simplicity, the following implementation stores the values in memory, tied to a value stored in a hidden input element.

(web.py) 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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133

#!/usr/bin/env python

import cgi
from wsgiref.simple_server import make_server

# Everytime we generate an html page, we create a hidden input element
# with this name. It lets us know which saved history must be resumed
# in order to continue the program.
HISTORY_FORM_NAME = 'WebInterface_history_index'

class History(object):
    """A record of past values returned by the routine. Useful for playback.
       self.get_pending is a function which takes a dictionary like object
           corresponding to the POST variables, and returns the new value
           to be added to the history.
       self.old_values is all of the results of functions yielded by the routine.
       """
    def __init__(self, get_pending, old_values):
        self.get_pending = get_pending
        self.old_values = old_values

class WebInterface(object):
    """WebInterface wraps around a routine class to allow for the routine to
       be executed through a browser. It works by remembering the results
       of functions that were yielded by the routine. In order to pick up
       where it left off, the routine is re-run with the remembered values,
       a new value is parsed from the POST variables, and the routine keeps
       running until it reaches another prompt."""
    def __init__(self, routine_class):
        self.routine_class = routine_class
        self.histories = [History(None, [])]

    def respond(self, environ, start_response):
        responder = WebInterface.Response(self, environ, start_response)
        return responder.respond()

    class Response(object):
        """The Response class is instantiated for every HTTP request.
           It grabs the appropriate history according to the value in the POST
           variable 'WebInterface_history_index'. Using that history, it
           re-runs the routine with the contained old_values, parses the POST
           variables for any new values using get_pending, and continues the
           routine until it needs to make another request. For simplicity,
           it modifies web_interface.histories directly. A real
           implementation would need to protect this variable using locks
           (or find a mutation-free solution), since it is possible for
           the wsgi server to make concurrent calls to WebInterface.respond.
           """
        def __init__(self, web_interface, environ, start_response):
            self.web_interface = web_interface
            self.environ = environ
            self.start_response = start_response

        def respond(self):
            routine = self.web_interface.routine_class(self)
            self.form = cgi.FieldStorage(fp=self.environ['wsgi.input'],environ=self.environ)
            history_index = int(self.form.getvalue(HISTORY_FORM_NAME, default="0"))
            if len(self.web_interface.histories) <= history_index:
                self.start_response('412 Cannot read the future', [('Content-type', 'text/html')])
                return ["That history has not yet been written."]

            # Copy the history in order to create a new history.
            history_orig = self.web_interface.histories[history_index]
            self.history = History(history_orig.get_pending, history_orig.old_values[:])
            self.start_response('200 OK', [('Content-type', 'text/html')])
            self.output = [ '<form method="POST">\n' ]

            self.paused = False
            iter = routine.__iter__()
            try:
                # Re-run the routine over all old_values.
                action = iter.next()
                for history_value in self.history.old_values:
                    action = iter.send(history_value)

                # If a get_pending was previously set, invoke it in order
                # to parse the POST variables for any new values.
                if self.history.get_pending != None:
                    val = self.history.get_pending(self)
                    self.history.old_values.append(val)
                    action = iter.send(val)

                # Continue the routine until another prompt is made.
                while not self.paused:
                    new_value = action()
                    if not self.paused:
                        self.history.old_values.append(new_value)
                        action = iter.send(new_value)

            except StopIteration:
                pass

            self.web_interface.histories.append(self.history)
            self.output += '<input type="hidden" name="%s" value="%s">\n' % (HISTORY_FORM_NAME, len(self.web_interface.histories) - 1)
            self.output += '</form>\n'
            return self.output

        def display(self, str):
            self.output += str + "
\n"

        def prompt_string(self, prompt):
            self.prompt_type(prompt, str)

        def prompt_int(self, prompt):
            self.prompt_type(prompt, int)

        def prompt_yes_no(self, prompt):
            self.prompt_and_pause(
                    prompt,
                    [("submit", "btn_yes", "Yes"), ("submit", "btn_no", "No")],
                    lambda form: form.has_key('btn_yes'))

        def prompt_type(self, prompt, type_parse):
            self.prompt_and_pause(
                    prompt,
                    [("text", "prompt", ""), ("submit", "btn_submit", "Enter")],
                    lambda form: type_parse(form["prompt"].value))

        def prompt_and_pause(self, prompt, inputs, parse_form):
            self.output += prompt
            for input in inputs:
                self.output += '<input type="%s" name="%s" value="%s">\n' % input
            self.paused = True
            def read_from_form(responder):
                return parse_form(responder.form)
            self.history.get_pending = read_from_form

if __name__=="__main__":
    from game import RandomNumberGame
    interface = WebInterface(RandomNumberGame)
    httpd = make_server('', 8000, interface.respond)
    httpd.serve_forever()

Lorem Ipsum

| Comments

But I must explain to you how all this mistaken idea of denouncing pleasure and praising pain was born and I will give you a complete account of the system, and expound the actual teachings of the great explorer of the truth, the master-builder of human happiness. No one rejects, dislikes, or avoids pleasure itself, because it is pleasure, but because those who do not know how to pursue pleasure rationally encounter consequences that are extremely painful. Nor again is there anyone who loves or pursues or desires to obtain pain of itself, because it is pain, but because occasionally circumstances occur in which toil and pain can procure him some great pleasure. To take a trivial example, which of us ever undertakes laborious physical exercise, except to obtain some advantage from it? But who has any right to find fault with a man who chooses to enjoy a pleasure that has no annoying consequences, or one who avoids a pain that produces no resultant pleasure?