Interpreters with Non-Determinism Using a Free Monad

Non-determinism can be a challenging language feature to give a definitional interpreter for. In this post we illustrate an approach to overcoming this challenge: a free monad.

This blog post is a literate Agda file. The contents of this post should be accessible to readers familiar with Haskell; and it should be possible to translate the definitions in this post to non-dependently typed languages, such as Haskell or Scala, by using slightly less precise encodings of free monads.

The contents of this post are based on joint work with Arjen Rouvoet.

Typos, comments, or questions? Let me know!

Why Free Monads and This Blog Post?

The purpose of this post is to illustrate the free monads approach to modeling non-determinism as an effect, in a way that does not require a deep understanding of the continuation monad, and in a way that lets us write a definitional interpreter and define its effects separately.

There are many other ways we could define and implement interpreters with non-determinism.1 Why use a free monad? As we will illustrate, free monads allow us to

  1. define a single definitional interpreter with multiple possible interpretations of effects.
  2. have fine-grained control over the interpreter state, as is necessary to define, e.g., non-determinism.

The combination of these two properties is attractive for many purposes, and this combination is hard to come by if we use general monads, unless we resort to the continuation monad (sometimes called “the mother of all monads”). On the other hand, free monads are less powerful than regular monads,2 and can be as involved to work with as general monads.

Contents of this Post

Command Trees (a Free Monad)

A free monad defines trees of chained sequences of effectful commands. We illustrate what we mean by this below, but first we define a data type Free, which defines a free monad that describes the structure of command trees:3

data Free (C : Set) (R : C  Set) (A : Set) : Set where
  ‵return : A  Free C R A
  _‵>>=_  : (c : C)  (R c  Free C R A)  Free C R A

Free is indexed by a set of commands (C : Set), a set of command-dependent responses (R : C → Set), and a set of values that the command tree will ultimately produce (A : Set).

Free has two data type constructors:

  • ‵return is a trivial command which simply returns a value of type A directly.
  • _‵>>=_ defines an infix operator which is used to chain together a command (c : C) and a continuation which takes a command-response as input and returns the remaining set of commands in the tree as output (R c → Free C R A).

The inhabitants of the Free data type are trees in the sense that continuations branch over all possible responses resulting from interpreting a command. In the continuation of _‵>>=_ in Free, R c represents the response type of a command c.

An Example: Coin Flip Command Trees

Say our set of commands consists of a single command for flipping a coin:

data FCmd : Set where
  !flip : FCmd

And say we expect a Boolean as the result of a flip command. The function below implements this precisely:

FResp : FCmd  Set
FResp ‵flip = Bool

Now the following command tree represents a program that returns one of two strings ("heads" or "tails") depending on the result of flipping a coin:4

flipping-example : Free FCmd FResp String
flipping-example =
  !flip ‵>>= λ where
    true   ‵return "heads"
    false  ‵return "tails"

The command tree above does not actually perform the flip action: it is an explicit representation of a program that flips a coin, and branches on the result of performing the flip.

In order to actually perform the flip, we should define an interpretation function for translating command trees of type Free FCmd FResp _ into actual effectful computation. We omit the interpretation function for coin flips here. Below we illustrate how to define such a command tree interpretation function. First, we introduce some convenience functions that we shall make use of in order to use a free monad to write definitional interpreters for languages with effects.

Free is a Monad

We define return and _>>=_ (pronounced “bind”) functions for Free.

We put these definitions in a module because we are going to be defining different return and _>>=_ functions later in this post:

module FreeMonad where

return is just an alias for constructing a trivial command tree:5

  return :  {C R A}  A  Free C R A
  return = ‵return

_>>=_ takes a command tree and a continuation as input, and splices the two together:

  _>>=_ :  {C R A B} 
          Free C R A 
          (A  Free C R B) 
          Free C R B
  ‵return x  >>= k = k x
  (c ‵>>= f) >>= k = c ‵>>=  r  f r >>= k)

A Language with Non-Deterministic Choice

Our goal is to write interpreters for languages with non-determinism. For the purpose of studying how we can reach this goal, we shall focus on a rather tiny and mostly-uninteresting language that nonetheless holds many of the same challenges for dealing with non-determinism as more interesting languages. The language is a calculator language with numbers (‵num), addition expressions (_‵+_), and operations for recalling (‵recall) and setting (‵set) the value of a single memory cell. That is, the language runtime tracks the state of a single memory cell which can hold a single number in it, and which can be recalled and mutated during run time.

data Expr : Set where
  ‵num    :   Expr
  _‵+_   : Expr  Expr  Expr
  ‵recall : Expr
  ‵set    :   Expr

The order of evaluation for addition expressions is undefined for this language. Consider the following expression:

nondet-expr-example : Expr
nondet-expr-example =
  ‵recall ‵+ (‵set 1)

If the initial value of the memory cell is 0, then nondet-expr-example should return either 1 or 2, depending on whether the ‵recall expression is interpreted before or after (‵set 1), and assuming that the result of evaluating a ‵set expressions is the number that ‵set is applied to (i.e., 1 in the program above).

An Interpreter with Committed‑Choice Non‑Determinism

We shall define an interpreter with non-deterministic evaluation order between the left and right sub-expression branches of addition expressions. We define the interpreter in three steps:

  1. We define a set of commands and responses that our interpreter shall make use of to define effectful computations.
  2. We define an evaluation function which translates an Expression into a command tree. This step will give us an explicit representation of which effectful actions an Expression gives rise to.
  3. We define the meaning of command trees.

Commands and Responses (Step 1)

Our interpreter will make use of three different commands as defined by the Cmd data type:6

mutual
  data Cmd : Set where
    !set    :   Cmd
    !recall : Cmd
    !fork   : Free Cmd Resp  
              Free Cmd Resp  
              Cmd

  Resp : Cmd  Set
  Resp (!set n)      = 
  Resp !recall       = 
  Resp (!fork f₁ f₂) =  × 

Here:

  • !set n sets the memory cell to n, and returns n as the result of command evaluation.
  • !recall recalls the current value of the memory cell.
  • !fork f₁ f₂ evaluates two command trees f₁ and f₂. The order in which the two command trees are evaluated (left-to-right or right-to-left) is decided by flipping a coin.

The Resp data type tells us what the return type is for each of these commands.

Our interpreter shall make use of the following “liftings” of each command to a command tree:

recall : Free Cmd Resp 
recall = !recall ‵>>= ‵return

set :   Free Cmd Resp 
set n = !set n ‵>>= ‵return

fork : Free Cmd Resp  
       Free Cmd Resp  
       Free Cmd Resp ( × )
fork f₁ f₂ = !fork f₁ f₂ ‵>>= ‵return

Evaluation (Step 2)

Now let us define an evaluation function that takes an expression as input, and returns as output a command tree that represents a program with non-deterministic choice (using fork) and a stateful memory cell (set and recall).

The eval function below makes use of the _>>=_ and return of Free, using Agda’s support for do notation.

module _ where
  open FreeMonad

  eval : Expr  Free Cmd Resp 
  eval (‵num n) =
    return n
  eval (e₁ ‵+ e₂) = do
    (n₁ , n₂)  fork (eval e₁) (eval e₂)
    return (n₁ + n₂)
  eval ‵recall = do
    recall
  eval (‵set n) =
    set n

Here we have put eval in an anonymous module (named _) in order to locally open the FreeMonad module which defines _>>=_.

An Example

We can now evaluate the nondet-expr-example program from earlier by turning the object language program into a command tree that tells us which effects the program gives rise to, and in which order:

  nondet-free-example : Free Cmd Resp 
  nondet-free-example =
    eval (‵recall ‵+ (‵set 1))

Evaluation yields the command tree shown below:7 8

  nondet-example :
      nondet-free-example
    
      !fork (!recall ‵>>= ‵return)
            (!set 1 ‵>>= ‵return) ‵>>= (λ{ (n₁ , n₂) 
     ‵return (n₁ + n₂) })
  nondet-example = refl

This program represents that there is a fork in our interpreter: the interpreter may choose to evaluate the recall branch first; or it may choose to evaluate the ‵set 1 branch first. The result of either order of evaluation is going to be a pair of two natural numbers which are added together in the continuation expression (λ{ (n₁ , n₂) → ‵return (n₁ + n₂) }).

Command Tree Meaning (Step 3)

We define the meaning of command trees, by translating trees into actual computations. Our notion of computation will have to encode some notion of non-determinism. There are multiple ways we could choose to encode non-determinism, such as accumulating the set of all possible outcomes that a program can have, or by “flipping a coin” to decide which branch to follow at fork points. We opt for the latter, but the former would have been equally fine.

module CommandTreeMeaning where

We translate command trees into computations that consume streams of coin flips and can mutate a stateful memory cell. We represent coin flips as a stream of booleans (e.g., true for heads; false for tails). The CM type defines computations:

  CM : Set  Set
  CM A = Stream Bool  
          
         A × Stream Bool  × 

A computation of type CM A expects as input a(n infinite) stream of coin flips (Stream Bool ∞9), and a memory cell value (), and returns as output a value of type A, as well as the remaining stream of coin flips and the (possibly) updated memory cell value.

CM is a monad, and we define return and _>>=_ functions over CM, to be used by the translation function from command trees to CM that we define shortly.10

  return :  {A}  A  CM A
  return a cs n = a , cs , n

  _>>=_ :  {A B}  CM A  (A  CM B)  CM B
  (f >>= k) cs n =
    case (f cs n) of λ where
      (a , cs′ , n′) 
        k a cs′ n′

  _>>_ :  {A B}  CM A  CM B  CM B
  f >> k = f >>= const k

Our translation function will also make use of the following effectful operations over CM:

  • do-set n mutates the state of the memory cell to n.
  • do-recall recalls the state of the memory cell.
  • do-flip flips a coin and returns the (Boolean) result.
  do-set :   CM 
  do-set n cs _ = n , cs , n

  do-recall : CM 
  do-recall cs n = n , cs , n

  do-flip : CM Bool
  do-flip cs n = head cs , tail cs , n

We define a handle function which translates a command into a computation, and a ⟦_⟧ function which translates command trees into computations by handleing each command in the tree, thereby turning it into a computation:

  mutual
    handle : (c : Cmd)  CM (Resp c)
    handle (!set n)      = do-set n
    handle !recall       = do-recall
    handle (!fork f₁ f₂) = do
      b  do-flip
      if b
         then (do
           n₁   f₁ 
           n₂   f₂ 
           return (n₁ , n₂))
         else (do
           n₂   f₂ 
           n₁   f₁ 
           return (n₁ , n₂))

The handle function makes use of the ⟦_⟧ function (below) in the !fork f₁ f₂ case, because the definition of !fork requires us to turn each of f₁ and f₂ into computations. The !fork case does so by first flipping a coin to decide which order in which to evaluate f₁ and f₂. The ⟦_⟧ function uses handle to turn commands into computations, and chains command tree branch computations by using the _>>=_ of CM:

    ⟦_⟧ : Free Cmd Resp   CM 
     ‵return n  = return n
     c ‵>>=  k  = handle c >>= λ r   k r 

Given eval and ⟦_⟧, we can define an interp function for interpreting expressions to numbers:

  interp : Expr  Stream Bool   
  interp e cs = proj₁ ( eval e  cs 0)

Running It

The semantics lets us interpret the nondet-expr-example program from above using different orders of evaluation to yield different results:

  true-stream  = repeat true  -- infinite stream of `true`s
  false-stream = repeat false -- infinite stream of `false`s

  interp-nondet-expr-example=1 :
      1
    
      interp nondet-expr-example true-stream
  interp-nondet-expr-example=1 = refl

  interp-nondet-expr-example=2 :
      2
    
      interp nondet-expr-example false-stream
  interp-nondet-expr-example=2 = refl

Intermezzo

We have defined a semantics for committed-choice non-determinism for a simple calculator language. We have done so by first translating calculator language expressions into command trees, and subsequently giving meaning to these command trees. Command trees serve as explicit representations of the effect semantics of object language programs. This representation lets us control the order in which semantic actions happen — which is exactly what we need to define an interleaving order of evaluation. In the rest of this post, we reuse evaluator eval from above, but give new meaning to the !fork command, which interleaves the order of evaluation of expressions at fork points.

An Interpreter with Interleaving Non‑Determinism

Consider the following program:

interleave-example : Expr
interleave-example =
  ((‵set 1) ‵+ ‵recall)
  ‵+
  (‵set 2)

Using our interpreter from above, there are two possible outcomes from evaluation:

  1. 3 = 0 + 1 + 2 (corresponding to this sequence of memory effects: ‵recall; (‵set 1); (‵set 2)
  2. 4 = 1 + 1 + 2 (corresponding to this sequence of memory effects: (‵set 1); ‵recall; (‵set 2)

The interpreter above is non-deterministic, but after deciding which branch to evaluate first, the interpreter is committed to fully evaluating the first branch before evaluating the second branch. That means that the following outcome is not valid with the interpreter above:

  1. 5 = 1 + 2 + 2 (corresponding to this sequence of memory effects: (‵set 1); (‵set 2); recall)

With an interleaving semantics, all of i.-iii. are valid outcomes, because we allow interpreters to do computation in any branch.

We will write an interpreter with interleaving order of evaluation, which can yield either of the three results above. We follow the same recipe as before. That is, we first define a set of commands and responses, then an evaluation function that translates source language expressions into command trees, and finally we define the meaning of these command trees separately.

module InterleavingEval where
  open FreeMonad

Commands, Responses, and Evaluation

The commands, responses, and evaluation function is exactly the same as above. Only the command tree meaning changes. Free monads allow us to define a single definitional interpreter with multiple possible interpretations of effects.

Command Tree Meaning

We define the meaning of commands and command trees, by translating command trees into actual computations.

module InterleavingMonad where
  
  open InterleavingEval

The notion of computation we shall use keeps track of a pool of Threads, where each Thread represents an interleavingly executing computation.

There are two kinds of threads: running threads, and blocked threads that are waiting to join the results of two other threads in the current thread pool:
  data Thread (A : Set) : Set where
    running : Free Cmd Resp A  Thread A
    join    :     (A × A  Free Cmd Resp )  Thread A

The join constructor is parameterized by two natural numbers, say n₁ and n₁, representing two thread identifiers in the current thread pool. The meaning of join should be to fetch the final results (of type A) produced by the threads at position n₁ and n₂, and pass these two results to the continuation of the join expression (A × A → Free Cmd Resp ℕ).

Our notion of computation is given by the IM type:
  IM : Set  Set
  IM A = List (Thread ) 
         Stream   
          
         Maybe (A × List (Thread ) × Stream   × )

A computation takes as input:

  1. A list of threads (a thread pool).
  2. A stream of natural numbers, representing an interleaving order. For example, a stream whose first three numbers are 1, 2, and 0 would first do a single computation step of the thread at position 1 in the current thread pool; then a single computation step of the thread at position 2; and then a single computation step of the thread at position 0.
  3. A natural number representing a stateful memory cell (of type ).

Unless computations fail (the Maybe in the return type of IM indicates possible-failure), a computation returns some value of type A, an updated thread pool (List (Thread ℕ)), an updated stream of interleaving choices, and an updated memory cell ().

The reason for possible-failure in IM has to do with the fact that thread pool lookups may fail.11 For example, if the thread pool only has two threads in it, and we try to do a computation step of a thread at position 3, this will fail.

IM is a monad:12

  return :  {A}  A  IM A
  return a ts cs n = just (a , ts , cs , n)

  _>>=_ :  {A B} 
          IM A  (A  IM B)  IM B
  (f >>= k) ts cs n =
    case (f ts cs n) of λ where
      (just (a , ts′ , cs′ , n′)) 
        k a ts′ cs′ n′
      nothing 
        nothing

  _>>_ :  {A B}  IM A  IM B  IM B
  f >> k = f >>= const k

We define the following effectful operations over IM:

  • fail aborts a computation.
  • get-thread n tries to get the thread at position n in the current thread pool.
  • set-thread n θ updates the thread at position n in the current thread pool to be θ (where θ is of type Thread).
  • new-thread θ adds a new thread θ to the current thread pool, and returns a pointer to the newly created thread.
  • do-set and do-recall are as before.
  • do-choice consumes a thread pool pointer from the stream of natural numbers representing the interleaving order for the currently executing program.
  fail :  {A}  IM A
  fail _ _ _ = nothing

  get-thread :   IM (Thread )
  get-thread t ts cs n =
    case (ts  t) of λ where
      nothing  nothing
      (just θ)  just (θ , ts , cs , n)

  set-thread :   Thread   IM 
  set-thread t θ ts cs n =
    case (t [ ts ]≔ θ) of λ where
      nothing  nothing
      (just ts′) 
        just (tt , ts′ , cs , n)

  new-thread : Thread   IM 
  new-thread θ ts cs n =
    let t = length ts in
    just (t , ts ++ θ  [] , cs , n)

  do-set :   IM 
  do-set n ts cs _ =
    just (tt , ts , cs , n)

  do-recall : IM 
  do-recall ts cs n =
    just (n , ts , cs , n)

  do-choice : IM 
  do-choice ts cs n =
    just (head cs , ts , tail cs , n)

We define a step f function for doing a single step of interpretation for a command tree f, and yield a thread representing the result of doing the computation step. step is a function over IM, so it may alter the underlying thread state; e.g., by allocating new threads in the case of interpreting a !fork:

  step : Free Cmd Resp   IM (Thread )
  step (‵return x)          =
    return (running (‵return x))
  step (!set n ‵>>= k)      = do
    do-set n
    return (running (k n))
  step (!recall ‵>>= k)     = do
    n  do-recall
    return (running (k n))
  step (!fork f₁ f₂ ‵>>= k) = do
    t₁  new-thread (running f₁)
    t₂  new-thread (running f₂)
    return (join t₁ t₂ k)

step-thread does a single computation step for a thread. Running threads are interpreted by using the definition of step from above, whereas join threads are interpreted by getting the thread states at each of the thread positions that join indicates that it has forked. Doing a steo of a join thread only succeeds if both of the forked threads have actually yielded a result.

  step-thread : Thread   IM (Thread )
  step-thread (running f)    = step f
  step-thread (join t₁ t₂ k) = do
    (running (‵return n₁))  get-thread t₁
      where _  fail
    (running (‵return n₂))  get-thread t₂
      where _  fail
    return (running (k (n₁ , n₂)))

step-pool uses the interleaving order to decide which thread to do a computation step of. After doing a step in a thread, the thread state of the computation IM is updated to reflect the thread update.

  step-pool : IM 
  step-pool = do
    c  do-choice
    θ  get-thread c
    θ′  step-thread θ
    set-thread c θ′

We can run threads by continuing to iterate the state of the thread pool by calling step-pool, until the main thread (given by the thread at position 0) has yielded a result, or until evaluation fails for some reason:

  run :   IM 
  run (suc k) = do
    θ  get-thread 0
    case θ of λ where
      (running (‵return n)) 
        return n
      _  do
        step-pool
        run k
  run _ = fail

run is parameterized by a natural number indicating how many steps we should do before giving up and failing.13

Given the functions defined so far, we can define the following meaning function which turns a command tree into a computation that we can run n steps of, where steps can happen in interleaved order of evaluation:

  ⟦_⟧ : Free Cmd Resp     IM 
   f  k ts = run k (running f  ts)

We can now also define an interp function that uses eval and ⟦_⟧ to interpret an expression into a number (unless the computation crashes):

  interp : Expr    Stream    Maybe 
  interp e k cs =
    case ( eval e  k [] cs 0) of λ where
      nothing  nothing
      (just (n , _))  just n

Running It

The following interleaving orders (interleaving1-3) correspond gives us the three different outputs (i.-iii.) summarized earlier when we discussed the interleave-example program:

  interleaving1 : Stream  
  interleaving1 = (0  1  4  3  1  2  []) ++ˢ (repeat 0)

  interleaving2 : Stream  
  interleaving2 = (0  1  3  4  1  2  []) ++ˢ (repeat 0)

  interleaving3 : Stream  
  interleaving3 = (0  1  3  2  4  1  []) ++ˢ (repeat 0)

  interp-interleave-example=3 :
      just 3
    
      interp interleave-example 100 interleaving1
  interp-interleave-example=3 = refl

  interp-interleave-example=4 :
      just 4
    
      interp interleave-example 100 interleaving2
  interp-interleave-example=4 = refl

  interp-interleave-example=5 :
      just 5
    
      interp interleave-example 100 interleaving3
  interp-interleave-example=5 = refl

Conclusion

We have illustrated how to use a free monad for modeling non-determinism as an effect, in a way that does not require a deep understanding of the continuation monad, and in a way that lets us write a definitional interpreter and define its effects, completely separately from the interpreter itself.


  1. For example, we could have used a small-step interpreter, or an interpreter in continuation-passing style.

  2. To be more specific, free monads can be used to implement most monads except for the continuation monad.

  3. The command tree nomenclature, and (more importantly) the core idea of this post, is due to Hancock and Setzer. This representation of command trees is borrowed from Baanen and Swierstra’s recent work on predicate transformer semantics.

  4. The λ where true → … ; false → … is Agda notation for a function that pattern matches on the input.

  5. The syntax ∀ {A B} → … means that Agda will automatically try to infer which types A and B the function implicitly takes as input.

  6. The mutual keyword tells Agda that the definitions may be mutually recursive. That is, the definition of Cmd can refer to Resp, and Resp can refer to Cmd.

  7. nondet-example is an Agda proof that eval (nondet-expr-example) is equal to the command tree shown in the type of the program.

  8. λ{ (n₁ , n₂) → … } is Agda notation for a pattern matching lambda, similarly to λ where (n₁ , n₂) → ….

  9. The index in Stream Bool ∞ is a size annotation, required by the Stream type in the Agda Standard Library.

  10. For the purpose of this blog post, we are content with claiming that CM is a monad, and shall not bother with proving the monad laws for the notion of _>>=_ and return of CM.

  11. Since we are working in Agda, we might avoid this use of Maybe by using more precise (dependent) types. We are more concerned with explaining to the programmer how effects are actually intended to be interpreted here than we are with explaining this to Agda’s type checker. (Even if the two tend to be connected in practice.)

  12. Once again we are content with claiming that IM is a monad, and shall not bother with proving the monad laws for the notion of _>>=_ and return of IM.

  13. This parameterization by a natural number is a folklore technique known by many names, such as fueled, petrol-driven, gas-driven, or step-indexed interpretation. We use this technique because Agda insists that function should be obviously terminating or obviously non-terminating. It is not obvious (to Agda) that our notion of thread pool will always be terminating. We could have helped Agda realize that it is by using sized types, but that is beyond the scope of this post.