This blog post show that execution in a lazy language is both understandable and predictable.

Haskell is in essence a heavily sugared and extended version of a typed λ-calculus (i.e. λ-calculus with a type system attached). If you don’t understand simple λ-calculus, you should read a tutorial, such as the first two chapters of Introduction to Lambda Calculus[pdf]. We won’t be doing anything too complicated with it, but you should understand the basic syntax and ideas behind it. If we want to understand Haskell’s execution, we should should first understand call-by-need evaluation of λ-calculus.

In 1993 Launchbury wrote A Natural Semantics for Lazy Evaluation [pdf], which provided a simple operational semantics (I’ll explain what that is in a second) for understanding the lazy evaluation of an extended λ-calculus. The most important extension is the let statements: “lets are irreplaceable in lazy functional programming in that they may create cyclic structures in the heap. This cannot be achieved without them (or without something essentially equivalent), and cyclic structures have a huge implication for the amount of computation that may be performed” . He also includes constructors, case statements, and primitives in an extension to the base semantics. Operational semantics is very appropriately named: it provides semantics, or a meaning, to the code in terms of its operation on some abstract machine. What precisely is an abstract machine? Basically, it’s a mathematical model of a machine. Rather than create a physical machine with moving or electronic parts, you create a transition function. This function takes the current state (e.g. the current heap, stack, and the expression you want to reduce), and produces the next state (say, the heap remained the same, but you pushed something onto the stack and you’re evaluating some subexpression). Launchbury’s semantics are reasonably high-level and simple, but still capture sharing and heap usage.

Before we continue, let’s remind ourselves how the λ-calculus is evaluated. There are several strategies for reducing a λ-term, which have different pros and cons. In normal order reduction, the outermost leftmost redex (reducible expression, i.e. something of the form (λx.y)z is reduced. This means that you don’t evaluate the arguments to a function until after they’re plugged into the function. Call-by-name is similar to normal order, except that you don’t reduce anything inside a λ-abstraction. Call-by-need is very similar to call-by-name, but with one key difference: call-by-name implements sharing (I’ll explain what that is momentarily). Call-b-name and call-by-need stand in contrast with call-by-value reduction, where you reduce the outermost redex only after you reduce its right hand side (i.e. the arguments to the function get evaluated before the function does).

What does sharing mean? It means that arguments to a function are only evaluated once; the calculated values are “shared” between their uses. For example, consider the expression (λx. mult x x) (ackermann 4 1). Under call-by-value, you first reduce this to (λx. mult x x) 65533, and then to mult 65533 65533, then to 4,294,574,089. In call-by-name, you first reduce it to mult (ackermann 4 1) (ackermann 4 1). You then evaluate (ackermann 4 1) twice, because it appears twice. Call-by-need gets rid of this repeated evaluation: the first time you evaluate (ackermann 4 1), you replace both occurrences of it with 65533. Obviously, this is a very important optimization. It’s important to point out here that sharing doesn’t mean Common Subexpression Elimination; it only means that arguments are evaluated only once.

Before you can apply the reduction rules, Launchbury’s semantics require a term to be normalized. A Launchbury-normalized term is one in which every name is unique (so scope isn’t important because something in an inner scope cannot shadow something in an outer scope), and which every application involves applying a variable to an expression. Normalization is simple: just replace every variable with a fresh variable (so everything becomes distinctly named), and replace constructs of the form “e1 e2″ with “let x = e2 in e1 x”. So, in our previous example, (λx. mult x x) (ackermann 4 1) is normalized to let z = expensive 4 1 in (λx. mult x x) z. Since we will store our let-bound variables on the heap, this means that implementing sharing is trivial: we update the reference on the heap the first time we evaluate it, and just use that value every other time.

In order to help illustrate the semantics, I’ve written up a small interpreter which takes in a normalized expression and reduces it, returning both the reduced expression and a log of how it got there. I didn’t implement a normalizer; instead expressions need to be normalized by hand.

Let’s go over the interpreter. I’ll leave out constructors, primitives and case statements, although they’re on hackage. I’ll also leave out the implementation of the various helper functions; their details aren’t important to understanding the semantics.

To start out with, we should define some types to represent an expression:

type Name = String 
 
data Expr =  Lambda Name Expr
           | Apply Expr Name
           | Var Name
           | Let Bindings Expr
           deriving (Eq, Show)
 
type Binding = (Name,Expr)
type Bindings = [Binding])
 
type Heap = [(Var, Expr)]
 
type ReduceM a =  ...
 
--record that current state
data ReduceState = ...

Expr is fairly simple: It represents the syntax tree of lambda expressions extended with let. We’ll represent variables as strings, because it’s convenient. A Heap, with respect to the paper, is “a partial function from variables to expressions”, however, you can also think of it as “an unordered set of variable/expression pairs, binding distinct variable names to expressions”. The latter interpretation is easier to work with, so we’ll be using it. I’m leaving out the implementation of Show, but the Hackage code includes an instance of show that outputs reasonable looking code. ReduceM keeps track of the state of the heap, the fresh variables, and the log, as well as allowing reduce to fail.

Here are the functions to make working with ReduceM reasonable:

 
 
rmRun :: ReduceM a → ReduceState → (Either String a, ReduceState)
 
-- hides the implementation detail of failing; makes it easier to
-- swap out the underlying monad.
rmErr :: String → ReduceM Expr
 
-- |Like sub, but for a list of things to substite
-- useful for implementing recursive lets (i.e. letrec)
subs :: [(Name,Name)] → (Expr → Expr)
 
-- |e[x/y] in Launchbury's notation
--  [x ↦ y]e in Pierce's notation in TaPL
--  recursively descend expression tree to substitute a free variable
sub ::  Name → Name → (Expr → Expr)
 
-- |freshen takes an expression, and returns the same expression with every 
-- bound variable substituted for a fresh variable. 
freshen :: Expr → ReduceM Expr
 
type ErrorOr a = Either String a
type Log = String
 
-- look up a binding on the heap
heapLookup :: Name → ReduceM Expr
 
-- remove a binding from the heap
heapRemove :: Name → ReduceM ()
 
-- create a new binding on the heap
heapAdd :: Name → Expr → ReduceM ()
 
--  get the next fresh variable.  Fresh variables are of the form $23, for random
-- values of 23
getFreshVar :: ReduceM Name
 
-- reduces an expression.
reduceM :: Expr → ReduceM Expr

Freshen and sub are important, but the real work of the program is done in reduceM; that’s where the reduction actually happens. So what does the code for it look like?

reduceM :: Expr → ReduceM Expr
reduceM e =
    case e of
        Lambda e' x → return (Lambda e' x)  
        Apply e' x  →  do Lambda y' e'' ← reduceM e'
                          reduceM (sub y' x e'')
        Var x →       do e' ← heapLookup x
                         heapRemove x
                         z ← reduceM e'
                         heapAdd x z
                         freshen z
        Let bs e' →  do mapM_ (uncurry heapAdd) bs
                        reduceM e'

Let’s go through each of these cases one by one.

First: Lambda. The only sensible thing to do here is to just return the λ-abstraction, because we’re not allowed to reduce inside of a λ-abstraction.

Second: Apply. In order to actually apply a variable to a subexpression, we need a function to apply it to. However, the subexpression might not be a λ-abstraction. Instead, it could be something that returns a λ-abstraction – a variable, a let, or even another apply! The only sensible thing to do here is to reduce our subexpression, and then apply the variable to it.

Third: Variable. In order to reduce a variable x, we must first know what it is bound to on the heap. So, we look up the expression e that it is bound to. The next step is less obvious: we reduce e with x’s binding removed from the heap, before returning a freshened version of the result, to avoid unwanted variable capture. Is this correct?

Obviously, if the expression isn’t recursive, we’re fine – it’s never going to look at its own binding. What happens in that case if x is recursive? Well, there are two possibilities – either the sub-expression depends on itself before it reduces, or it depends on itself after it reduces. If it depends on itself after it reduces, then we’re obviously fine – the binding will already be back on the heap. What about the other case? We’re actually still fine: If you depend on yourself before you reduce to a value, then you must be an infinite loop. In this case, we fail outright, because we’re trying to look up a binding which doesn’t exist. Failing outright and having an infinite loop are the same thing, semantically speaking, so we’re actually still fine.

Here’s some examples of recursion, both good and bad. Assume the appropriate functions have been defined for the third example. It also hasn’t been properly normalized, but ignore that as well. Can you figure out what these will do? The answers will be at the bottom of the post

let x = x in x 
let f = λx.f x in f 2
let len = λlist. if (empty? list) 0 (1 + (len (cdr list))) in len some-list

Fourth: Let. Since everything is distinctly named, we don’t need to worry about scope; names will never clash because each name can only be used once. Therefore, it’s obviously correct to just add the bindings to the heap.

Now that we’ve explained this, let’s look at the output of some runthroughs:

Reducing let: let u = 3 + 2, v = u + 1 in v + v : {}

How should we interpret this? Well, it’s fairly simple. In the beginning,we start to reduce the expression ‘let u = 3 + 2, v = u + 1 in v + v’, using an empty heap (denoted ‘{}’).

|Reducing primitive: v + v : {v → u + 1, u → 3 + 2}

We then add the bindings to the heap and take a look at the addition ‘v + v’.

||Reducing variable: v : {v → u + 1, u → 3 + 2}

In order to reduce ‘v + v’, you first need to evaluate v.

|||Reducing primitive: u + 1 : {u → 3 + 2}
||||Reducing variable: u : {u → 3 + 2}

To calculate v, we need to evaluate u.

|||||Reducing primitive: 3 + 2 : {}
||||||Returning constructor: 3 : {}
||||||Returning constructor: 2 : {}
|||||Primitive evaluated to 5
||||Rebinding var u to 5
||||Returning constructor: 1 : {u → 5}
|||Primitive evaluated to 6
||Rebinding var v to 6

So we evaluate u, then evaluate v with the result of u.

||Reducing variable: v : {v → 6, u → 5}

We’re re-grabbing v here for the second usage of v in v+v

|||Returning constructor: 6 : {u → 5}
||Rebinding var v to 6
|Primitive evaluated to 12
Ans: 12

Note that we access v two times in this, but we only access u a single time.

For another two test cases, let’s take a look at two examples from Launchbury’s paper:

First: let u = 2 + 3, f = \x.let v = u + 1 in v + x, a = 2, b = 3 in f a + f b

and

Second: let u = 2 + 3, f = let v = u + 1 in \x.v + x, a = 2, b = 3 in f a + f b

Note that the expressions are the same except for f’s definition; in the first, f is “\x.let v = u + 1 in v + x,” and in the second f is “let v = u + 1 in \x.v + x”. Obviously, these two are going to evaluate to the same thing. However, what’s going to be the difference in terms of how they reduce? Does one share sub-computations more effectively than the other to reduce the amount of computation needed? Let’s take a look at the log produced by running them to figure that out.

Reducing let: let u = 2 + 3, f = \x.let v = u + 1 in v + x, a = 2, b = 3 in f a + f b : {}
|Reducing primitive: f a + f b : {b → 3, a → 2, f → \x.let v = u + 1 in v + x, u → 2 + 3}
||Reducing apply: f a : {b → 3, a → 2, f → \x.let v = u + 1 in v + x, u → 2 + 3}
|||Reducing variable: f : {b → 3, a → 2, f → \x.let v = u + 1 in v + x, u → 2 + 3}
||||Returning lambda: \x.let v = u + 1 in v + x : {b → 3, a → 2, u → 2 + 3}
|||Rebinding var f to \x.let v = u + 1 in v + x
|||Reducing let: let $2 = u + 1 in $2 + a : {f → \x.let v = u + 1 in v + x, b → 3, a → 2, u → 2 + 3}
||||Reducing primitive: $2 + a : {$2 → u + 1, f → \x.let v = u + 1 in v + x, b → 3, a → 2, u → 2 + 3}
|||||Reducing variable: $2 : {$2 → u + 1, f → \x.let v = u + 1 in v + x, b → 3, a → 2, u → 2 + 3}
||||||Reducing primitive: u + 1 : {f → \x.let v = u + 1 in v + x, b → 3, a → 2, u → 2 + 3}
|||||||Reducing variable: u : {f → \x.let v = u + 1 in v + x, b → 3, a → 2, u → 2 + 3}
||||||||Reducing primitive: 2 + 3 : {f → \x.let v = u + 1 in v + x, b → 3, a - > 2}
|||||||||Returning constructor: 2 : {f → \x.let v = u + 1 in v + x, b → 3, a - > 2}
|||||||||Returning constructor: 3 : {f → \x.let v = u + 1 in v + x, b → 3, a - > 2}
||||||||Primitive evaluated to 5
|||||||Rebinding var u to 5
|||||||Returning constructor: 1 : {u → 5, f → \x.let v = u + 1 in v + x, b → 3, a → 2}
||||||Primitive evaluated to 6
|||||Rebinding var $2 to 6
|||||Reducing variable: a : {$2 → 6, u → 5, f → \x.let v = u + 1 in v + x, b → 3, a → 2}
||||||Returning constructor: 2 : {$2 → 6, u → 5, f → \x.let v = u + 1 in v + x, b → 3}
|||||Rebinding var a to 2
||||Primitive evaluated to 8
||Reducing apply: f b : {a → 2, $2 → 6, u → 5, f → \x.let v = u + 1 in v + x , b → 3}
|||Reducing variable: f : {a → 2, $2 → 6, u → 5, f → \x.let v = u + 1 in v + x, b → 3}
||||Returning lambda: \x.let v = u + 1 in v + x : {a → 2, $2 → 6, u → 5, b → 3}
|||Rebinding var f to \x.let v = u + 1 in v + x
|||Reducing let: let $4 = u + 1 in $4 + b : {f → \x.let v = u + 1 in v + x, a - > 2, $2 → 6, u → 5, b → 3}
||||Reducing primitive: $4 + b : {$4 → u + 1, f → \x.let v = u + 1 in v + x, a → 2, $2 → 6, u → 5, b → 3}
|||||Reducing variable: $4 : {$4 → u + 1, f → \x.let v = u + 1 in v + x, a → 2, $2 → 6, u → 5, b → 3}
||||||Reducing primitive: u + 1 : {f → \x.let v = u + 1 in v + x, a → 2, $2 → 6, u → 5, b → 3}
|||||||Reducing variable: u : {f → \x.let v = u + 1 in v + x, a → 2, $2 → 6, u → 5, b → 3}
||||||||Returning constructor: 5 : {f → \x.let v = u + 1 in v + x, a → 2, $2 → 6, b → 3}
|||||||Rebinding var u to 5
|||||||Returning constructor: 1 : {u → 5, f → \x.let v = u + 1 in v + x, a → 2, $2 → 6, b → 3}
||||||Primitive evaluated to 6
|||||Rebinding var $4 to 6
|||||Reducing variable: b : {$4 → 6, u → 5, f → \x.let v = u + 1 in v + x, a → 2, $2 → 6, b → 3}
||||||Returning constructor: 3 : {$4 → 6, u → 5, f → \x.let v = u + 1 in v + x, a → 2, $2 → 6}
|||||Rebinding var b to 3
||||Primitive evaluated to 9
|Primitive evaluated to 17
Ans: 17
 
Reducing let: let u = 2 + 3, f = let v = u + 1 in \x.v + x, a = 2, b = 3 in f a + f b : {}
|Reducing primitive: f a + f b : {b → 3, a → 2, f → let v = u + 1 in \x.v + x , u → 2 + 3}
||Reducing apply: f a : {b → 3, a → 2, f → let v = u + 1 in \x.v + x, u → 2 + 3}
|||Reducing variable: f : {b → 3, a → 2, f → let v = u + 1 in \x.v + x, u → 2 + 3}
||||Reducing let: let v = u + 1 in \x.v + x : {b → 3, a → 2, u → 2 + 3}
|||||Returning lambda: \x.v + x : {v → u + 1, b → 3, a → 2, u → 2 + 3}
|||Rebinding var f to \x.v + x
|||Reducing primitive: v + a : {f → \x.v + x, v → u + 1, b → 3, a → 2, u → 2 + 3}
||||Reducing variable: v : {f → \x.v + x, v → u + 1, b → 3, a → 2, u → 2 + 3}
|||||Reducing primitive: u + 1 : {f → \x.v + x, b → 3, a → 2, u → 2 + 3}
||||||Reducing variable: u : {f → \x.v + x, b → 3, a → 2, u → 2 + 3}
|||||||Reducing primitive: 2 + 3 : {f → \x.v + x, b → 3, a → 2}
||||||||Returning constructor: 2 : {f → \x.v + x, b → 3, a → 2}
||||||||Returning constructor: 3 : {f → \x.v + x, b → 3, a → 2}
|||||||Primitive evaluated to 5
||||||Rebinding var u to 5
||||||Returning constructor: 1 : {u → 5, f → \x.v + x, b → 3, a → 2}
|||||Primitive evaluated to 6
||||Rebinding var v to 6
||||Reducing variable: a : {v → 6, u → 5, f → \x.v + x, b → 3, a → 2}
|||||Returning constructor: 2 : {v → 6, u → 5, f → \x.v + x, b → 3}
||||Rebinding var a to 2
|||Primitive evaluated to 8
||Reducing apply: f b : {a → 2, v → 6, u → 5, f → \x.v + x, b → 3}
|||Reducing variable: f : {a → 2, v → 6, u → 5, f → \x.v + x, b → 3}
||||Returning lambda: \x.v + x : {a → 2, v → 6, u → 5, b → 3}
|||Rebinding var f to \x.v + x
|||Reducing primitive: v + b : {f → \x.v + x, a → 2, v → 6, u → 5, b → 3}
||||Reducing variable: v : {f → \x.v + x, a → 2, v → 6, u → 5, b → 3}
|||||Returning constructor: 6 : {f → \x.v + x, a → 2, u → 5, b → 3}
||||Rebinding var v to 6
||||Reducing variable: b : {v → 6, f → \x.v + x, a → 2, u → 5, b → 3}
|||||Returning constructor: 3 : {v → 6, f → \x.v + x, a → 2, u → 5}
||||Rebinding var b to 3
|||Primitive evaluated to 9
|Primitive evaluated to 17
Ans: 17

As you can immediately see, the first one has a larger heap than the second one does. The reason for that becomes clear when you look at it more closely: In the second one, when we reduce f we add the let bindings to the heap once, because it’s outside the enclosing lambda. In the first one, on the other hand, f doesn’t reduce at all, because the lambda is the outermost thing. On account of that, we end up adding “v = u + 1″ to the heap twice in the first case, which leads to performing that calculation twice. In the second expression, on the other hand, v is added to the heap the first time we call f, so both invocations share the same heap space for v, which means that u is only accessed a single time.

Based off of those logs, it is reasonable to expect that the first expression will run faster. So, lets test that. Here are those two functions, translated straightforwardly into Haskell. We’ll run them in Hugs, since Hugs will print the number of heap cells used and reductions made. Smaller numbers for both are better.

slowExprHaskell = let u = 3+2
                      f = \x → let v = u+1 in v + x
                  in f 2 + f 3
 
fastExprHaskell = let u = 3+2
                      f = let v = u+1 in \x → v + x
                  in f 2 + f 3
–- results from Hugs:
Main$ slowExprHaskell
17
(47 reductions, 86 cells)
Main$ fastExprHaskell
17
(43 reductions, 78 cells)

This is what we expected.

What key lessons can you take from this to use in your everyday Haskell coding? First, always prefer to create a let outside of a lambda rather than inside of a lambda, to take greater advantage of sharing. Second, lazy evaluation is not black magic, it doesn’t evaluate things in an order based off of the phase of the moon; it is deterministic and follows fairly simple semantics. While tracing impure lazy computations is very difficult, it is not too hard to get a reasonable idea of how a pure lazy function will be evaluated.

(The answers to the questions posed earlier are that the first expression halts because it uses itself before it has been rebound on the heap, the second expression is an infinite loop, and the third one is a normal recursive function that will reduce to the correct answer.)

Semantic Editor Combinators - Conal Elliott [link]

Strictly speaking this isn’t a paper. On the other hand, the functional pearl therein is a must for any Haskeller’s box of tools. The essence of the presented technique allows one to write easy to understand transforms of functions, or function like things. For example:

f :: Int -> (Int,Char) -> String
-- Want to convert into type g . . .
g :: Int -> (Int,Int) -> String
-- with transformer z.
z :: Int -> Char
-- Implementation using semantic editor combinators:
g = (result . argument . second) z f

The g implementation can be read backwards as “apply the z transformation to the second element of the tuple of the argument of the result of f”. Recall that functions only have one argument and one result and that the result of a curried function is another function.

It takes a bit of getting used to, but it is definitely worth the investment in time learning. It frequently makes code more elegant and concise.

Note, if you ever get stumbled by an (fmap.fmap.fmap) in code, this is where to go.

Naturally, many will reject such a subjective list. I concede that the list is heavily influenced by my own interests and lack of prerequisite knowledge in some cases. However, I’d argue that it isn’t entirely useless. First, I’d expect several of these papers to be well respected by experts in their respective fields. In this way, my list does shadow the objective truth. Second, my rare occupation as a commercial Haskell contractor makes my personal viewpoints of particular interest.

So, without further ado, the list.

The List

#7 Experience Report: Haskell in the “Real World” - Curt J. Sampson [abstract][pdf]

This paper showcases the decision of a software business to use functional programming without any prior experience with the paradigm. The business’s choice of Haskell for a programming language was outlined as well as the benefits they enjoyed. What struck me in particular were the problems and disadvantages the programming team encountered. It was refreshing to see my own experiences with these issues put so clearly. I point business associates primarily to this paper for an introduction to using Haskell commercially.

#6 Algebra of programming in Agda: Dependent types for relational program derivation - Shin-Cheng Mu et al.[abstract][pdf]

Agda, a dependently typed programming language with a syntax similar to Haskell, is fueling a lot of research this year. After reading many papers such as this one, I can’t help but think that the future lies in dependent types.

This paper presents an unorthodox approach to writing programs called relational program derivation. One starts by encoding a proposition, for example “the algorithm x sorts all lists”, and then deriving a program that the proposition is true for, like quicksort. The authors created an algebra for encoding these derivations in Agda. By using Agda, the derived programs include a computer verified proof of correctness.

I think it is going to take a while before the programming community, myself included, becomes fully aware of the implications of this paper.

#5 Fun with Type Functions - Oleg Kiselyov, Simon Peyton Jones, Chung-chieh Shan [link][pdf]

Reaching a limitation of the type checker is a common cause of ire for Haskell programmers. Type families, a new feature of ghc, removes a sizable amount of these limitations. Superseding an earlier compiler extension, functional dependencies, type families opens up many new areas of generic programming as well. One of the most interesting examples from the paper is a simple type-safe implementation of printf and scanf.

Note that the final version of this paper has not been published yet.

#4 Commercial uses: Going functional on exotic trades - Simon Frankau et al.[abstract][pdf]

Where the #7 spot paper expounds on the implications of switching to Haskell, this paper gives an in depth detail of a commercial domain specific embedded language (DSEL) using Haskell. The explanations within were atypically clear and well referenced. After studying this paper I felt confidant in using Haskell as a host language for DSEL’s.

For someone new to DSEL’s, this paper is great first read. In my opinion, DSEL’s are one of the most lucrative uses of Haskell commercially.

#3 Safe Functional Reactive Programming through Dependent types - Neil Sculthorpe, Henrik Nilsson [abstract][pdf]

This paper contributed two important findings to the field of functional reactive programming (FRP). First, it presented several obvious defects in current FRP implementations. Those who’ve programed with FRP in any depth are painfully aware of how easy it is to accidentally create programs that loop or leak memory at run-time. Sculthorpe and Nilsson pinpoint the exact cause of these issues.

The second major contribution is an FRP implementation that they proved does not have these problems. The aforementioned proof is computer verified. Can you guess how they did it? If you guessed that they used Agda, you’d be right! Amazing stuff.

#2 Typeclassopedia - Brent Yorgey [pdf]

Brent Yorgey’s Typeclassopedia, published in the Monad.Reader is the most comprehensive tutorial on the basic Haskell type classes (like Monoids, Monads, etc.) thus far. It stands out in both its accessibility to all levels of Haskell developers and its vast coverage. The paper can be used both as a tutorial and a reference. For more in-depth studies, lots of useful references are also included.

This paper is a great contribution to the Haskell community and will surely become a classic.

#1 Finally Tagless, Partially Evaluated - Jacques Carette, Oleg Kiselyov and Chung-Chieh Shan [abstract][pdf]

The essence of this paper is so simple, it bears repeating right here

varZ env = fst env
varS vp env = vp $ snd env
b b env = b
lam a env = \x -> a (x,env)
app a b env = (a env) (b env)

What you’re looking at is a simple implementation of a typed embedded language using Haskell98 as a host for both the language and the type checking. Prior to this paper, embedded language designers took advantage of Haskell98’s syntax, but not its type system.

The problem the authors so elegantly solve using Haskell98 was a main motivation behind the complex generalized algebraic data type (GADT) extensions to Haskell. Perhaps this extension isn’t necessary after all.

They further describe how to extend this simple interpreter to various efficient compilers and interpreters without modification of the original embedded language. Although the paper primarily uses OCaml, they provide equivalent Haskell code on their website.

I’m looking forward to seeing more complex embedded languages built on the ideas of this paper. It wins first prize for elegance, utility, and cleverness.

Notes

Runner-ups

The Arrow Calculus (Technical Report) - Sam Lindley, Philip Wadler, and Jeremy Yallop [link]. This paper describes a new syntax for arrows that more closely resembles the lambda calculus. It remains to be seen if this syntax is easier to use than our current proc syntax.

Push-pull functional reactive programming - Conal Elliott [link]. This paper is a theoretically elegant refactoring of FRP using standard type classes. Had I not directly encountered the subtle, and serious, bugs of this implementation in a commercial setting, it probably would have made the list.

Denotational Semantics - David Schmidt [link]. This is a book written in 1982 that I read last year. It is just as relevant today as it was back then. An excellent exposition of denotational semantics. My programming has substantially changed for the better since that read. It was regretfully disqualified for the medium and date of publication.

Where I hear about these papers

Journal of Functional Programming. I purchased a paper subscription.

The Monad.Reader. A must-read, freely available Haskell journal.

Haskell Weekly News. A weekly summary of community activity. A great place to discover powerful blog posts or pre-releases of journal articles.

Proceedings of ICFP (International Conference of Functional Programming) and affiliated SIGPLANs. I have access to these from the ACM website because I’m an alumnus of the University of Rochester. It took me a long time to get through the great quantity of papers available here, but it was very worthwhile.

Apology

I apologize for all mistakes and especially all my omissions. I am certain there are papers that would have made the list had I only read or understood them. I invite my readers to point out their favorites in the comments below.

Thanks to all who contribute to this field and give me countless hours of enjoyable reading and pondering.

See a short note on a blog post that I really wanted to be on this list.

I’m a seasoned freelance software developer. There’s no PhD after my name and I’ve written heaps of C++ and python code for commercial projects. For me, concepts need to be both practical and time-saving before I integrate them into my development work. On the other hand, I enjoy thinking about and studying concepts that are thought provoking and clever, like first class patterns in pure pattern calculus for example.

My focus, for these posts, is where these two categories merge. Maybe we can call this fuzzy area applied theory. All too often, applied theory isn’t taught or written about and doesn’t reach Joe the programmer who can actually use it on his project.

After reading interesting research papers, I often ask myself one or both of two questions: “What problems, that I’ve encountered or might encounter, would I want to solve with this?”, and “What are the details required to put this to use?”. Working out the answers to these questions is a real joy for me. I don’t always figure out how to make clever ideas useful or practical, but when I do, and subsequently use it in a commercial project, I get a lot of satisfaction.

Lets see what techniques we can apply to a giant, ugly heap of poo code that I’ve been working with. You’ll recognize it as the code base that combines an intense security requirement with occasional embarrassing vulnerabilities. OpenSSL is the name.

Now, I want to make it clear that I’m not dissing the OpenSSL developers (except maybe Eric Young for including a self-advertising clause in the license that still sticks to this day). I’ve written my share of what I call “superman code”.

How does superman code arise? You get a call from a frantic customer: “Hey, we need to write X software and we need it in 2 days”. You put on your cape and fly out there immediately. With plenty of caffeine and snacks, you hack together something with super-human speed that solves their imminent problem. You fly back home tired and they throw a party while crediting you (or themselves occasionally) for being a genius. 6 months later you revisit the superman code and scratch your head wondering just what the heck did the undocumented X509_REVOKED_add1_ext_i2d function do again? You end up rewriting half of it.

Our example is an OpenSSL function called SSL_CTX_set_verify. Give that manpage a quick read to get a idea what that function does. My task was to make a preexisting OpenSSL client verify that the server’s certificate was valid upon connection. The code below shows the lines of code I added:

asio::ssl::context context( io_service
                          , asio::ssl::context::tlsv1_client
                          );
//2 New Lines
context.set_verify_mode(asio::ssl::context::verify_peer);
context.load_verify_file("ca.pem");
//...

Note that I’m using the boost.asio library which includes a thin wrapper on OpenSSL. Unfortunately, my small change didn’t work when I ran it. Can you spot the bug?

I hope you didn’t spend as much time as I did looking for a bug in either the boost.asio or OpenSSL code bases. My bug was in the “//…” part. Lets expand a little bit:

asio::ssl::context context( io_service
                          , asio::ssl::context::tlsv1_client
                          );
//2 New Lines
context.set_verify_mode(asio::ssl::context::verify_peer);
context.load_verify_file("ca.pem");
//...
context.set_verify_mode(asio::ssl::context::verify_none);
//...

Oops! I changed the verify mode twice. What a bummer! This is where a functional programming principle, called purity, comes into play.

“set_verify_mode” is really a misnomer because what we are actually doing is changing the verify mode “state” to something else. The type of that function, in Haskell notation, would be something like:

set_verify_mode :: Context -> Int -> Context

We can do better. What we really want to do is define a context with a specified verify mode [declarative style], not create an arbitrary default context and change it [imperative style].

Consider the following code:

data ContextParams = CP { verifyMode :: Int
                        -- ...
                        }
context :: ContextParams -> Context

What we’re doing is moving all the imperative set_ functions (that really modify a context) into the “constructor” of Context. This being the case, we’re disallowing, at compile time, the changing of the context verify mode. The bug I introduced would never have made it to run time if Context was designed in this way.

Moving on, lets see if we can stop passing Ints around. I want to disallow the following type of code from compiling:

let c = context $ CP { verifyMode = 3 + 22
                     , --...
                     }

Setting a verifyMode to a sum of numbers really doesn’t make sense, does it? The essence of the verify mode is not an Integer, but something else. Looking at the manual page, we see that there are different sets of verify modes that make sense depending whether or not the context is a client or server. That indicates to me two distinct data types.

data ClientVerifyMode = -- ...
data ServerVerifyMode = -- ...

Lets set up a simple client mode definition:

data ClientVerifyMode = ClientVerifyPeer
                      | ClientVerifyNone

But going further, we know that if we’re verifying the peer we’ll be needing certificate authority keys to verify with (this is set with the SSL_CTX_use_certificate_file function). Also required would be the maximum certificate depth (SSL_CTX_set_verify_depth). On the other hand the SSL_CTX_set_verify function allows for a function to be passed to override the other parameters. Further “out there”, one could bypass all this stuff by writing his own verification function with SSL_CTX_set_cert_verify_callback.

Confusing? I found it confusing anyway. How can we simplify this? What is the essence of what we are trying to do here? The answer can be found by acting like a buddhist monk. Go take an unstructured walk. Exhale your desires and aversions. Inhale nature. Feel the oneness of all things. Notice the feeling of being touched by your clothing or the taste in your mouth. This is living. This is the field of inspiration. This is where the answer lies if it falls upon the path of your destiny.

Welcome back. What our function and its relatives boils down to is verification of the peer’s credentials, which is a certificate chain. Either the credentials are acceptable or they are not by whatever means you check them. So, the essence we’ve been looking for is:

data ClientPeerVerifier = -- Credentials -> Bool

That little comment is there to document our intended semantics or meaning. We derived this while doing hippie things. I plan on talking more about meanings and the subject of denotational semantics in a later post. Now we can give appropriate names to the specializations available in OpenSSL

data ClientPeerVerifier = -- Credentials -> Bool
                        | F (Credentials->Bool)

The F constructor, standing for function, represents the most general SSL_CTX_set_cert_verify_callback style verifier. Now some more

data ClientPeerVerifier = -- Credentials -> Bool
                        | F (Credentials->Bool)
                        | ConstTrue
                        | SimpleVerify TrustedCertificates Int

ConstTrue will represent the SSL_VERIFY_NONE parameter. Notice how our semantics imply a nice name for this (”const True” is a function that returns True for every input). SimpleVerify merges SSL_CTX_use_certificate_file, SSL_CTX_set_verify_depth, and SSL_VERIFY_PEER.

There is something missing still, what about that “further verification process” controlled by the verify_callback parameter of the SSL_CTX_set_verify function? If we tried to implement this in our semantics, and call it z, we’d have:

z :: TrustedCertificates -> Int -> (Credentials -> Bool -> Bool) -> (Credentials -> Bool)
z ts depth g c = g (simpleVerify ts depth c) c

The first two parameters are the same as SimpleVerify above. The third parameter is a function taking in credentials and the result of the simple verify procedure.

Lacking a good name for Z, lets call it verifyWithSimpleVerifyResult. SimpleVerify is really a specialization of this, but we’ll leave it in case there is some optimization for a NULL verify_func argument to SSL_CTX_set_verify.

data ClientPeerVerifier = -- Credentials -> Bool
                        | F (Credentials->Bool)
                        | ConstTrue
                        | SimpleVerify TrustedCertificates Int
                        | VerifyWithSimpleVerifyResult TrustedCertificates Int (Credentials -> Bool -> Bool)

Now we have all our cases covered. The only thing I might add to the code would be a comment explaining the meaning of VerifyWithSimpleVerifyResult, for example the definition of z above.

We could, if we wanted, write functions that have a user description (as opposed to semantic name) to help a user document his own code:

alwaysAccept :: ClientPeerVerifier
alwaysAccept = ConstTrue

For the ServerPeerVerifier, we’ll need a different meaning, or essence, as a client doesn’t always supply a certificate.

data ServerPeerVerifier = -- Maybe Credentials -> Bool

Concluding Thoughts

Using semantics, in many ways, obviates the need for a large portion of documentation. For example, knowing the semantics of ClientPeerVerifier allows me to understand completely ConstTrue by only reading its name. Compare this approach to the wordy, and incomplete, manual pages of OpenSSL. Thinking in semantics has a whole lot of other advantages as well which I’ll cover in another post.

Judiciously using purity and specialized data types (like we did when removing the use of Int for verifyMode) assists a developer in writing bug-free programs by disallowing a slew of bugs to get past the compilation stage.

For the actual project, I would likely continue using C++ but make the data types match what they would be if I were to transfer the Haskell code above. It turns out this isn’t as hard as one might think. The real use of Haskell on this problem was to construct a framework to understand the code that was there and design a new meaningful wrapper.

Excercises

Feel free to post your answers as comments.

(*) Figure out what to call the SSL_VERIFY_FAIL_IF_NO_PEER_CERT style ServerPeerVerifier.

(*) How would the semantics (meanings) need to change if we were handling the SSL_VERIFY_CLIENT_ONCE parameter?

(**) The SSL_CTX_set_cert_verify_callback function actually expects the callback to modify one of its arguments. If we wanted to include this functionality, how would we change the return value our ClientPeerVerifier semantics?

(**) Using the meaning style presented above or another functional style, write an OpenSSL wrapper in Haskell and submit it to Hackage. (Thanks!)

The event transformers we’re interested in ( : Event a -> Event b) semantically have the following property.

where

pfst = map fst

In other words, synchronous event transformers do not change the number of occurrences nor the times of occurrences of the argument. Most of Reactive’s event transformers have this property. Lets make a simple wrapper for Synchronous transformers:

type EventT a b = Event a -> Event b
newtype Synchronous a b = S {toEventT :: (EventT a b)}

There may be a better representation. Conal Elliott on #haskell suggested using MutantBots, but they aren’t expressive enough to encapsulate transformers like withNextE. For the purpose of this discussion, we’ll use the above representation and invite the reader to come up with a better one.

Some helper functions will come in handy. By the way, we’ll be using the style of Semantic Editor Combinators.

inS :: ((EventT a b) -> (EventT c d)) -> (Synchronous a b -> Synchronous c d)
inS f =  S . f . toEventT
 
inS2 :: ((EventT a b) -> (EventT c d) -> (EventT e f)) ->
        (Synchronous a b -> Synchronous c d -> Synchronous e f)
inS2 f (S a) (S b) = S (f a b)

An easy thing to see is that our Synchronous Event Transformers (SET’s) are Functors. The definition of fmap simply applies the function to the resultant event.

instance Functor (Synchronous a) where
  fmap = inS . fmap . fmap

One interesting thing about synchronous events is that we can apply one to another in parallel. In other words, if we have an event of functions and an event of values, we can apply each function event to each value event if they are synchronous.

-- Only works on events that are synchronous
apSync ::  EventG t (a->b) -> EventG t a -> EventG t b
apSync = inEvent2 f
  where
    f = inFuture2 (\(ta,a) (_, b) -> (ta, g a b))
    g (Stepper a ae) (Stepper b be) = (Stepper (a b) (apSync ae be))

If we have two synchronous event transformers, how can we combine them? One way would be to use apSync on their results:

apSyncT :: Synchronous e (d -> f) -> Synchronous e d -> Synchronous e f
apSyncT = inS2 (\f g e -> apSync (f e) (g e))

Hey, that looks mighty familiar:

instance Applicative (Synchronous a) where
  pure = S . pure . pure
  (<*>) = apSyncT

Interesting. Now we have an Applicative instance for synchronous event transformers. Later on, we’ll see how this is useful. As it turns out we can declare Category and Arrow instances as well:

instance Category Synchronous where
  id = S id
  (.) = inS2 (.)
 
instance Arrow Synchronous where
  arr = S . fmap
  (&&&) = liftA2 (,)
  -- Defined in terms of (&&&)
  first f = (f . arr fst) &&& arr snd

As with any applicative functor, we can define forwarded Num instances

-- Boilerplate taken from Reactive
noOv :: String -> String -> a
noOv ty meth = error $ meth ++ ": No overloading for " ++ ty
 
noFun :: String -> a
noFun = noOv "behavior"
 
-- Eq & Show are prerequisites for Num, so they need to be faked here
instance Eq (Synchronous a b) where
  (==) = noFun "(==)"
  (/=) = noFun "(/=)"
 
instance Show (Synchronous a b) where
  show      = noFun "show"
  showsPrec = noFun "showsPrec"
  showList  = noFun "showList"
 
instance Num b => Num (Synchronous a b) where
  negate      = fmap negate
  (+)         = liftA2 (+)
  (*)         = liftA2 (*)
  fromInteger = pure . fromInteger
  abs         = fmap abs
  signum      = fmap signum

Uses

Now that we have all these properties of synchronous events, how can we use them? Lets consider the types of a couple functions in reactive

withTimeE :: Ord t => EventG (Improving t) d -> EventG (Improving t) (d, t)
withTimeE_ :: Ord t => EventG (Improving t) d -> EventG (Improving t) t

Several Synchronous event functions come in pairs like this. The more general version passes along the data of the originating event and the convenient underscore variant doesn’t. The latter is implemented in terms of the former. With Synchronous, we can implement the more complex version in terms of the simpler version:

timeE :: Synchronous a TimeT
timeE = S withTimeE_
 
timeE' ::  Synchronous a (a, TimeT)
timeE' = liftA2 (,) id timeE
-- or, using Beelsebob's Applicative infix library
-- timeE' = id <^(,)^> timeE
-- or, if we make a default instance (for AFs) for Zip in Conal's TypeCompose
-- timeE' = zip id timeE

Synchronous eliminates the need to have two versions of these functions and saves us the strain of having implement the more complex variants.

More Synchronous Fun

Lets pull some more synchronous event transformers into our Synchronous data type:

prevE, nextE :: Synchronous a a
prevE = S withPrevE_
  where
    withPrevE_ = (fmap.fmap) snd withPrevE
nextE = S withNextE_
  where
    withNextE_ = (fmap.fmap) snd withNextE
 
mealyE ::  b -> (b -> b) -> Synchronous a b
mealyE a b = S (mealy_ a b)
 
splitE' ::  Event b -> Synchronous a (Event b)
splitE' = S . splitE_
  where
    splitE_ :: (Ord t) => EventG t b -> EventG t a -> EventG t (EventG t b)
    splitE_ = (fmap.fmap.fmap) snd splitE

Recall our elapsedFirstTry function from the event tutorial.

elapsedFirstTry :: Event () -> Event TimeT
elapsedFirstTry e = fmap f (withPrevE (withTimeE_ e))
  where
    f (tCur, tPrev) = tCur - tPrev

Since elapsed is a synchronous event transformer, we no longer need to implement a more complex variant of it. Thinking in terms of synchronous event transformers, we can further simplify the above definition:

elapsed ::  Synchronous a TimeT
elapsed = timeE - (prevE . timeE)

This can be read as “the time minus the previous time” for each occurrence. Our metronome implementation also sheds some complexity.

-- Old definition
metronome :: BellMachine
metronome = switchE . fmap f . withTimeE . mealy Idle next . withElapsed_
  where
    f ((dt,PlayingCycle), t) = period dt t
    f _ = mempty

to

metronome :: BellMachine
metronome = switchE . toEventT e'
  where
    e' = f <$> mealyE Idle next <*> timeE <*> elapsed
      where
        f PlayingCycle t dt = period dt t
        f _ _ _ = mempty

Using applicative in this case relieves us from tuple juggling and allows us to express more directly what we’d like. Note that toEventT was required here because switchE is not a synchronous transformer.

Arrows

I’m not certain it is all that useful, but arrows allow us to use the special arrow syntax. We can rewrite e' this way:

e' ::  Synchronous a (Event ())
e' = proc e -> do
  m <- mealyE Idle next -< e
  t <- timeE -< e
  dt <- elapsed -< e
  returnA -< if m == PlayingCycle then period t dt
                                  else mempty

– David Sankel @ Anygma.

Semantically, Behaviors can be thought of as functions of time:

Note that, unlike Events, behaviors do not include times at and .

Behaviors have a value at all times. The position of a computer mouse is a good example. At any time, there is exactly one position for the mouse. Other behaviors include the data on a hard drive, the color of a pixel, and the sound from speakers.

We’ll be exploring behaviors through various implementations of a dot machine. This machine consists of a display that has the ability to show any number of dots at arbitrary locations as well as a mouse with one button used for input.

type Dot = (Double,Double)
 
data Input = I { mouse :: Behavior (Double,Double)
               , button :: Event ()
               , integral :: (VectorSpace v, Scalar v ~ TimeT) => Behavior v -> Behavior v
               }
type DotMachine = Input -> Behavior [Dot]

Note that our Input data type also includes an integral function. We’ll assume that this performs some method of integration over time.

Simple Examples

For some basic examples, we’ll also consider machines that always display one dot.

type SingleDotMachine = Input -> Behavior Dot
toDotMachine :: SingleDotMachine -> DotMachine
toDotMachine = (fmap.fmap) pure
-- Alt. Def
-- toDotMachine s i = fmap (\a -> [a]) (s i)

Note that fmap applies to behaviors just as it applies to events.

A machine that displays a dot at the mouse location is quite simple:

atMouse :: SingleDotMachine
atMouse = mouse

Now, consider a machine that displays a dot at the origin of the screen.

originBA :: SingleDotMachine
originBA = const (pure (0.0,0.0))
-- Alt. Def.
-- originBA = (pure.pure) zeroV

pure produces a Behavior that is constant with respect to time. In our case pure (0.0,0.0) creates a Behavior of \t -> (0.0,0.0).

In the alternate definition, we use zeroV which is a function from the vector-space library and, in our case, is a synonym for (0.0,0.0). pure, when applied to functions, is equivalent to const.

Animation

One useful built in behavior is one that simply returns the current time as a Double.

time :: Behavior Double

time allows us to build simple animations.

Lets implement a machine that orbits the origin.

-- Simple Polar to Cartesian conversion
p2c :: (Floating a) => a -> a -> (a,a)
p2c mag phase = (mag*cos phase, mag*sin phase)
 
-- Orbit around the origin with a radius of 10.0
orbit :: Behavior (Double,Double)
orbit = fmap (p2c 10.0) time

Behaviors go beyond fmap in that a normal function can be “lifted” to apply to behaviors.

p2cB :: (Floating a) => Behavior a -> Behavior a -> Behavior (a,a)
p2cB = liftA2 p2c

The 2 in liftA2 specifies the number of parameters that should be converted to Behaviors. liftA3, and liftA4 are also available. These lift functions are defined in terms of a more general <*> operator. To learn more about this mechanism, see Applicative Functors on Wikibook.

Now we can define a machine with a spiral path:

spiral :: Behavior (Double,Double)
spiral = p2cB (fmap (\t -> 10.0*sin t) time) time

Integration

Reactive’s integration functions provide us with a straightforward way to incorporate simple physics into our programs. Recall from calculus how to find the position of an object with an initial position , an initial velocity , and a constant acceleration of .

In Reactive, this would be implemented as follows:

a = pure a0
v = pure v0 ^+^ integral a
p = pure p0 ^+^ integral v

There is a trick going on here. Recall that the expression pure v0 creates a constant function of time behavior. The plus (^+^) in this case actually adds two behaviors together. The definition of v could also have been written as:

v = liftA2 (^+^) (pure v0) (integral a)
-- or even simpler
v = fmap (^+^ v0) (integral a)

Reactive provides a vector space instance for behaviors of vectors space instances. Instances are also supplied for the various Num classes so you can feel free to use the normal + operator on two behaviors of Doubles, for example.

Consider a dot machine where the dot starts at the origin and is attracted towards the mouse. The further away the dot is, the faster it moves towards the mouse position.

First, we’ll use a general attractor function:

attract :: (Behavior Dot->Behavior Dot) -> -- The integral function
           Dot ->                          -- The initial position
           Behavior Dot ->                 -- The behavior to attract towards
           Behavior Dot
attract int pos0 attractor = pos
  where
    pos :: Behavior Dot
    pos = pure pos0 ^+^ int vel
    vel :: Behavior Dot
    vel = pos ^-^ attractor

Now the dot machine implementation is quite simple.

followMouse :: SingleDotMachine
followMouse i = attract (integral i) zeroV (mouse i)

Behaviors with Events

Reactive includes several functions involving both Behaviors and Events, the most primitive being stepper and snapshot.

-- | Discretely changing behavior, based on an initial value and a
-- new-value event.
stepper ::  a -> Event a -> Behavior a
 
-- Snapshot a behavior whenever an event occurs.
snapshot :: Behavior b -> Event a -> Event (a, b)
snapshot_ :: Behavior b -> Event a -> Event b

Using the above functions, we can make a machine that shows a dot at the origin until the button is pressed, in which case it will appear at the mouse position.

mouseAtPress :: Input -> Event Dot
mouseAtPress i = snapshot_ (mouse i) (button i)
-- Alt. Def.
-- mouseAtPress = liftA2 snapshot_ mouse button
 
wherePressed :: SingleDotMachine
wherePressed = stepper zeroV . mouseAtPress

If we instead want a dot to continue being displayed, we’ll collect the events,

collectE :: Event a -> Event [a]
collectE = monoidE . fmap pure
-- Alt def.
-- collectE = scanlE (++) [] . fmap (\a -> [a])

, make them into a behavior,

collectEB :: Event a -> Behavior [a]
collectEB = stepper mempty . collectE
-- Alt def.
-- collectEB = stepper [] . collectE

, and put it together:

atCursor :: DotMachine
atCursor = collectEB . mouseAtPress

Dynamic Collections

The atCursor example included a dynamically changing collection, a list of dots. What if instead we wanted a list of interactive behaviors instead? It turns out that this is difficult to implement in reactive as it is now. At the time of this writing reactive is being revamped for this purpose.

What’s Next

In the next article, I’ll conclude this series by taking a look at legacy adapters which enable our reactive programs to connect with the IO monad.

Acknowledgments

This tutorial was created by David Sankel with help from Thomas Davie and was sponsored by Anygma.

-- |At every event occurrence, produce a behavior that is a combination of the
-- first and second where it acts like the first up to the event occurrence
-- and then acts like the second.
splitB :: Behavior a ->
          Behavior a ->
          Event b    -> 
          Event (b,Behavior a)

This post describes how this function was implemented. In doing so, we’ll explore internals of the Reactive library and come into contact with the tricky laziness issues that often come up when working with Reactive.

Some of this code will be using (fmap.fmap) style. If that’s unfamiliar, see Peter Verswyvelen’s great mini tutorial on it.

Motivation

The following graph shows a mouse’s x axis position information over a period of time with time 0 representing when the program starts. The y axis represents the x position and the x axis represents time. If you look close, you’ll notice that the graph consists of dots representing samples of the mouse position. The position of the mouse between these samples is unknown by the computer.

In Reactive, we like to think of such things as continuous. In reactive-glut, for example, the mouse’s x position is represented as a continuous line, as in the following graph. At times before the program begins, all the way to , the position is .

Several useful reactive programs involve dynamic collections where a responsive entity comes to life at a certain time. In this case, we would like the entity’s knowledge of the universe to begin only after it’s creation. Aside from modeling the domain well, it sidesteps the possibility of a memory leak.

In the following graph we show what an entity might see of the x mouse position after its creation at time t.

splitB

Our solution to the above issues is a general function called splitB:

-- |At every event occurrence, produce a behavior that is a combination of the
-- first and second where it acts like the first up to the event occurrence
-- and then acts like the second.
splitB :: Behavior a ->
          Behavior a ->
          Event b    -> 
          Event (b,Behavior a)

To do the splitting as mentioned in the mouse example, we can specialize splitB to:

splitBBot :: Behavior a -> Event b -> Event (b, Behavior a)
splitBBot = splitB (pure (error "splitBBot: no data"))

A naive implementation

Lets start with a naive implementation:

splitB :: Behavior a -> Behavior a -> Event b -> Event (b, Behavior a)
splitB bLeft bRight e = fmap f (withTimeE e)
  where
    f (b,ot) = (b, iffB (fmap (ot >=) time) bLeft bRight)
 
iffB :: Behavior Bool -> Behavior a -> Behavior a -> Behavior a
iffB = liftA3 iff
 
iff a b c = if a then b else c

Semantically, the above splitB implementation is correct. Unfortunately, there is a rather large operational issue: whenever the resultant events are evaluated, a traversal of the entire bRight behavior occurs. This CPU and memory leak amounts to a reactive head explosion.

Something Better

What we need is a decent forgetter mechanism. For our first try we’ll reduce the behavior problem into a reactive problem.

unb :: BehaviorG tr tf a -> ReactiveG tr (Fun tf a)
beh :: ReactiveG tr (Fun tf a) -> BehaviorG tr tf a

The above functions convert a behavior into a reactive of time functions and vice-versa. It’s important to note that unb doesn’t have a semantic meaning and wouldn’t be used in normal code. The G’s in these signatures represent “General” in the aspect that the time types (tr and tf) are not fixed to any specific data type. The typical Event and Behavior types have tr and tf set to Double.

Now we can reduce our splitB implementation into an equivalent splitR implementation.

splitB l r e = fmap (second beh) (splitR (unb l) (unb r) e)
 
splitR :: Ord t => ReactiveG t a -> -- left
                   ReactiveG t a -> -- right
                   EventG t b -> -- Split locations
                   EventG t (b, ReactiveG t a) -- results

Lets assume we have a glueR for reactive that chops the right side of its first argument at time t, chops the left side of its second argument at time t, and glues the two pieces together:

glueR :: Ord t => ReactiveG t a ->  -- left
                  ReactiveG t a ->  -- right
                  Time t ->
                  ReactiveG t a -- combination of left and right with time t in the middle

We may now implement splitR:

splitR :: Ord t => ReactiveG t a -> -- left
                   ReactiveG t a -> -- right
                   EventG t b -> -- Split locations
                   EventG t (b, ReactiveG t a) -- results
splitR l r s = fmap snd (scanlE f (r,error "splitR, shouldn't see it") (withTimeGE s))
  where
    f (r,_) (b,t) = (c, (b,c))
      where
        c = glueR l r t

The above implementation uses scanlE to pass along the previous occurrence’s result to serve as a condensed version of the “right” reactive. We’ll deconstruct the Reactive data type to implement glueR in terms of glueE:

glueR :: Ord t => ReactiveG t a ->  ReactiveG t a -> Time t -> ReactiveG t a
glueR _ r (Max MinBound) = r
glueR l r (Max MaxBound) = l
glueR (Stepper al el) (Stepper ar er) t = Stepper al (glueE t el er)

In the above function, we see that a Reactive internally consists of an initial value and an event who’s occurrences represent possible changes.

Implementation of glueE is straightforward:

glueE :: Ord t => Time t -> EventG t a -> EventG t a -> EventG t a
glueE k = (fmap.fmap) (join . fmap (f k) . withTimeGE) eitherE
  where
    f k (e,t) | t < k     = either pure (pure mempty) e
              | otherwise = either (pure mempty) pure e

Thoughts

Our implementation of splitB certainly helps with our naive implementation’s memory and CPU leak. Unfortunately, when an occurrence is evaluated, all the behavior’s steps since the previous occurrence must still be traversed.

Much Better, but Very Tricky

Ideally, we would like each our occurrences to do no traversal when evaluated. If the prior event’s evaluation of the behavior caused concurrent evaluation of the current behavior, before it occurred, we can get this.

Lets look at a different implementation (note the different type signature) of glueE

glueE :: Ord t =>   Time t  ->
                 EventG t a ->  -- left
                 EventG t a ->  -- right
                 (EventG t a,   -- right event
                  EventG t a)   -- combination of left and right
glueE k l r = if k < min lt rt
               then (r,r)
               else if lt < rt
                      then second (mappend (once l)) (glueE k (restE l) r)
                      else first  (mappend (once r)) (glueE k l (restE r))
  where
    lt = firstETime l
    rt = firstETime r
 
-- If there is an occurrence, return the time of the first occurrence,
-- otherwise return +infty
firstETime :: Ord t => EventG t a -> Time t
firstETime = futTime . eFuture

glueE returns a copy of its right event and is completely identical semantically. However, the right event that is returned is now is written in terms of the combination. If one incrementally starts evaluating the returned right event, they are also evaluating the combination event at the same time. Think about it.

We can expand this to our glueR implementation:

glueR :: Ord t => ReactiveG t a ->  -- left
                  ReactiveG t a ->  -- right
                  Time t ->
                  ( ReactiveG t a   -- right
                  , ReactiveG t a ) -- combination of left and right
glueR _ r (Max MinBound) = (r, r)
glueR l r (Max MaxBound) = (r, l)
glueR (Stepper al el) (Stepper ar er) t = (Stepper ar *** Stepper al) (glueE t el er)

Finally, we put this together for our fully optimized splitR

splitR :: Ord t => ReactiveG t a -> -- left
                   ReactiveG t a -> -- right
                   EventG t b -> -- Split locations
                   EventG t (b, ReactiveG t a) -- results
splitR l r s = fmap g (withNextE (fmap snd (scanlE f (l,error "splitR, shouldn't see it") (withTimeGE s))))
  where
    f (cPrev,_) (b,t) = (c, (b,c,cPrev'))
      where
        (cPrev',c) = glueR l cPrev t
    g ((b,c,_), (_,_,c')) = (b,c')

The (fmap snd (scanlE f... part returns a triple (b,c,cPrev) where b is the value at the event splitter, c is the combination of the reactives at that event, and cPrev is the combination of the reactives at the previous event. cPrev is identical to c in the prior occurrence, however it has gone through that special transformation in glueR.

fmap g (withNextE... replaces the c in the triples with the cPrev in the subsequent event. The resulting 2-tuple is the answer.

Conclusion

If one has a widget of type UI -> Geometry3 we can now take a simple UI type:

data UI = UI {
  mousePosition      :: Behavior (Double,Double),
  leftButtonPressed  :: Event (),
  rightButtonPressed :: Event (),
  keyPressed         :: Event Key,
  framePass          :: Event ()
}

And define a function that will allow for new widgets to be created on command without worry of memory leak.

splitUiBot :: Ui -> Event b -> Event (b,Ui)

Hint: We’ll also need the use of a more general version of splitE.

Alright, now I can get back to writing that Behavior tutorial!

A basic knowledge of Haskell and the prelude functions, especially higher order functions like id and const, is all that is required.

We’ll start our journey by taking a look at events. Semantically, Events can be thought of as lists of time/value pairs where the times are non-decreasing:

Some varied examples:

• • [(1.0, 'h'), (2.0, 'e'), (3.0, 'l'), (3.1,'l'), (4.0,'o')] could be a keyboard event (Event Char) where the user typed “hello” pressing the keys at those times.
• • [(50.0,FSharp), (50.0,ASharp), (50.0,CSharp)] could refer to three notes being plucked on a guitar at time 50.
• • [(, ()), (0, ()), (5, ())] is an event that has an occurrence that happens before time. Note that events stretch time to include values at and . This is what the carot (^) signifies in the definition of above.
• • [ (1,()), (0,()) ] would not be an event since the times are decreasing.

Although we think of Events as lists, they are not implemented directly as them. Also, Events are abstract in that the representation itself isn’t manipulated directly. We’ll be using many Event functions that also apply to lists, and some that are specific to Events.

Some simple examples

Our examples are going to model various machines that have one button and a speaker that emits one sound. The button event is going to be of type Event (). We’re using the () type since these events don’t carry any extra information, unlike a keypress event. Our sound event is going to be similarly represented as Event (). So, quite simply our machines are all going to have the following type:

type BellMachine = Event () -> Event ()

For our first example, lets implement a simple machine that emits the bell event whenever the button event occurs.

doorBell :: BellMachine
doorBell = id

Using reactive, we can implement machines much more complex than a doorbell while retaining the same high-level of simplicity demonstrated in the above code.

Consider another simple machine. This one sounds a bell 3 minutes after it is turned on. Before we implement it, lets take a look at what functions Reactive includes for generating new events:

-- Converts a list of time/value pairs into an event. Note that the times _must_ be non-decreasing.
listE :: [(TimeT,a)] -> Event a
atTimes :: [TimeT] -> Event ()
atTime :: TimeT -> Event ()

Assuming that time 0 is when the machine turns on, the bell event could be implemented like this:

-- Convert minutes to seconds
mToS :: Double -> Double
mToS = (*) 60
 
-- The appropriate time to cook a soft-boiled egg is 3 minutes (see wikipedia)
eggTimer :: Event ()
eggTimer = atTime (mToS 3)

Note that eggTimer isn’t a machine of our initial type; It lacks any mention of an attached button. We make it into a machine of the appropriate type by ignoring all button presses using const.

eggTimerM :: BellMachine
eggTimerM = const eggTimer
-- Alternative Definition
-- eggTimerM = pure eggTimer

mempty/mappend (Monoid)

Lets look at a machine that sounds the bell at 10 seconds and when the user presses the button. Reflect, for a moment, on how this would be implemented imperatively. Timers? Signals? Event Loops? Compare that sketch to the simplicity of, and code-reuse within, the following reactive definition.

nifty :: BellMachine
nifty button = eggTimer `mappend` button
-- alternate definition
-- nifty = mappend eggTimer

We can think of mappend as merging events. Note that this function is part of the monoid concept and that mempty, mappend’s counterpart, represents an event that never occurs. Taking this into consideration, we can implement a completely silent machine like this:

silent :: BellMachine
silent = const mempty
-- Alternative Definition
-- silent = pure mempty

(Note: To use mappend and mempty, you’ll need to import Data.Monoid)

A more difficult example (fmap/switchE) (Functor/Monad)

Now lets implement a tricky machine. When the user presses the button twice, the machine begins pulsing the bell with a period equivalent to the time between the button presses. Another press of the button will stop the ringing at which point the process may be repeated.

Lets try to break the implementation into pieces. We know that we’ll need to calculate the difference of time between two event occurrences. For this sub-problem we’ll combine two of reactive’s functions, the first being withTimeE

-- Combine an event instance's data with its corresponding time.
withTimeE ::  Event a -> Event (a, TimeT)

withTimeE is typical of reactive’s built-in functions in that it carries along the input Event’s data in the first element of the resultant tuple, while the computed value gets inserted into the second element of the tuple. If we instead wanted to ignore the initial event’s data, we could define a new function, withTimeE_, as follows:

withTimeE_ :: Event a -> Event TimeT
withTimeE_ e = fmap snd (withTimeE e)
-- Alternative definition
-- withTimeE_ = (fmap.fmap) snd withTimeE

fmap allows us to apply a function to all the values of an event. fmap, like mappend/mempty, works similarly on other data types including functions (see the Functor class defined in Control.Monad).

The function we’ll be using in conjunction with withTimeE is withPrevE. withPrevE couples each value in an event with the previous occurrence’s value.

withPrevE ::  Event a -> Event (a, a)

Similar to withTimeE, it adds the computed value (in this case, the previous value) to the snd part of the tuple.

Combining these two functions, we can transform an Event () into an Event TimeT that represents the time passed since the previous event.

elapsedFirstTry :: Event () -> Event TimeT
elapsedFirstTry e = fmap f (withPrevE (withTimeE_ e))
  where
    f (tCur, tPrev) = tCur - tPrev
-- alt. def.
-- elapsedFirstTry = fmap (uncurry (-)) . withPrevE . withTimeE_

The above definition is all right, but in the spirit of reactive’s composability, we’ll define a more generally useful version that carries along the input event’s data and one that ignores it.

withElapsed :: Event a -> Event (a, TimeT)
withElapsed = fmap f . withPrevE . withTimeE
  where
    f ((aCur, tCur), (aPrev, tPrev)) = (aCur, tCur-tPrev)
 
withElapsed_ :: Event a -> Event TimeT
withElapsed_ = (fmap.fmap) snd withElapsed

withElapsed gets is pretty far along the way of implementing the proposed machine, but we still have a ways to go. Observe that we only care about the elapsed time every 3rd time the button is pressed. To ease identification of these particular presses, we’ll label the event occurrences with a state. First, we’ll define our state data type and a method to cycle them.

data State = Idle
           | WaitingForPeriodEnd
           | PlayingCycle
 
-- Given a state returns the next in sequence
next :: State -> State
next Idle                = WaitingForPeriodEnd
next WaitingForPeriodEnd = PlayingCycle
next PlayingCycle        = Idle

Reactive includes a simple function that will do the Event labeling for us.

-- | State machine, given initial value and transition function.  Carries
-- along event data.
mealy :: s -> (s -> s) -> Event b -> Event (b,s)
mealy_ :: s -> (s -> s) -> Event b -> Event s

Here is what we have so far . . . we’re getting pretty close.

soFar ::  Event () -> Event (TimeT, State)
soFar = mealy Idle next . withElapsed_

How do we generate the pulse events for the PlayingCycle state? For this type of situation, reactive has a few functions that have the signature Event (Event a) -> Event a. The most general of these is called join which applies to all Monads. In our case we’ll be using the switchE.

-- | Switch from one event to another, as they occur.
switchE :: Event (Event a) -> Event a

period :: TimeT -> TimeT -> Event ()
period delta t0 = atTimes (iterate ((+) delta) t0)

metronome :: BellMachine
metronome = switchE . fmap f . withTimeE . mealy Idle next . withElapsed_
  where
    f ((dt,PlayingCycle), t) = period dt t
    f _ = mempty

Install mingw & msys

Mingw and msys are required for the compiler and configure scripts. It has been reported to me that cygwin, which provides similar functionality, will not work.

MinGW. First, download the MinGW 5.1.4 installer and save it in a new folder. Execute the file and, when prompted, choose a minimal installation (it is important that you don’t install MinGW make).

MSYS. Download and run the msys 1.0.10 installer. You’ll be prompted with a console. Say yes to post install, reply yes to having MinGW installed, and type in your mingw location (default is C:/MinGW).

To check everything installed correctly, use Start->Programs->MinGW->MSYS->msys to open a prompt. At the prompt, typing gcc --version should show you the version of gcc you have installed.

Compile and Install freeglut

Download freeglut 2.4.0 source distribution and save it to C:\msys\1.0\home\<Your Username> (This is your default msys home directory. If you have your HOME environment variable set for another program, like emacs, your msys home directory is the value of that variable.).

Start the msys window, if you don’t already have one opened, and type the following commands at the prompt. You can paste into the msys window using SHIFT+INSERT or middle click.:

tar -zxf freeglut-2.4.0.tar.gz
cd freeglut-2.4.0/src/
gcc -O2 -c -DFREEGLUT_EXPORTS *.c -I../include
gcc -shared -o glut32.dll *.o -Wl,--enable-stdcall-fixup,--out-implib,libglut32.a -lopengl32 -lglu32 -lgdi32 -lwinmm

Now you should be left with glut32.dll and libglut32.a in that directory. Now move glut32.dll into your windows system32 directory.

cp glut32.dll /c/WINDOWS/system32

libglut32.a needs to be copied to ghc’s gcc-lib directory.

cp libglut32.a /c/ghc/ghc-6.10.1/gcc-lib/

Haskell OpenGL Binding

Download the haskell OpenGL binding from hackage here. At the time of this writing, the latest version was 2.2.1.1. Save it to your msys home directory, then type:

tar -zxf OpenGL-2.2.1.1.tar.gz
cd OpenGL-2.2.1.1
runhaskell Setup configure
runhaskell Setup build
runhaskell Setup install

Haskell GLUT Binding

Download the haskell GLUT binding from hackage here. At the time of this writing, the latest version was 2.1.1.2. Save it to your msys home directory.

You’ll also need to download the glutwin2112 patch (glutwin2112.patch) and save this to the msys home directory.

Then from an msys prompt enter the following:

tar -zxf GLUT-2.1.1.2.tar.gz
cd GLUT-2.1.1.2
patch -p1 < ../glutWin2112.patch
C_INCLUDE_PATH="../freeglut-2.4.0/include/" LIBRARY_PATH="../freeglut-2.4.0/src/" runhaskell Setup configure
C_INCLUDE_PATH="../freeglut-2.4.0/include/" LIBRARY_PATH="../freeglut-2.4.0/src/" runhaskell Setup build
C_INCLUDE_PATH="../freeglut-2.4.0/include/" LIBRARY_PATH="../freeglut-2.4.0/src/" runhaskell Setup install

Testing

Try to save and run the following file (teapots.hs). You should see a shaded sphere when run.

{-
   Light.hs (adapted from light.c which is (c) Silicon Graphics, Inc.)
   Copyright (c) Sven Panne 2002-2005 <sven.panne@aedion.de>
   This file is part of HOpenGL and distributed under a BSD-style license
   See the file libraries/GLUT/LICENSE
 
   This program demonstrates the use of the OpenGL lighting model. A sphere
   is drawn using a grey material characteristic. A single light source
   illuminates the object.
-}
 
import System.Exit ( exitWith, ExitCode(ExitSuccess) )
import Graphics.UI.GLUT
 
myInit :: IO ()
myInit = do
   clearColor $= Color4 0 0 0 0
   shadeModel $= Smooth
 
   materialSpecular Front $= Color4 1 1 1 1
   materialShininess Front $= 50
   position (Light 0) $= Vertex4 1 1 1 0
 
   lighting $= Enabled
   light (Light 0) $= Enabled
   depthFunc $= Just Less
 
display :: DisplayCallback
display = do
   clear [ ColorBuffer, DepthBuffer ]
   renderObject Solid (Sphere' 1 20 16)
   flush
 
reshape :: ReshapeCallback
reshape size@(Size w h) = do
   viewport $= (Position 0 0, size)
   matrixMode $= Projection
   loadIdentity
   let wf = fromIntegral w
       hf = fromIntegral h
   if w <= h
      then ortho (-1.5) 1.5 (-1.5 * hf/wf) (1.5 * hf/wf) (-10) 10
      else ortho (-1.5 * wf/hf) (1.5 * wf/hf) (-1.5) 1.5 (-10) 10
   matrixMode $= Modelview 0
   loadIdentity
 
keyboard :: KeyboardMouseCallback
keyboard (Char '\27') Down _ _ = exitWith ExitSuccess
keyboard _            _    _ _ = return ()
 
main :: IO ()
main = do
   (progName, _args) <- getArgsAndInitialize
   initialDisplayMode $= [ SingleBuffered, RGBMode, WithDepthBuffer ]
   initialWindowSize $= Size 500 500
   initialWindowPosition $= Position 100 100
   createWindow progName
   myInit
   displayCallback $= display
   reshapeCallback $= Just reshape
   keyboardMouseCallback $= Just keyboard
   mainLoop

Troubleshooting

Linker Errors. Pay close attention to the output of the GLUT configure command, it should have a line that looks like:

checking for GLUT library... -lglut32 -lglu32 -lopengl32 

If not, it may have failed without telling you so.

More Resources. The haskell-cafe mailing list is a good place to ask for help. Also this site has some information on getting freeglut+windows working with an older version of ghc.

Acknowledgments

joelhough.com blog for getting me started. Peter Verswyvelen for information on the HOME variable and pasting into the msys window. RayNBow for noting that the libglut32.a must be copied to a ghc directory. newsham and Greg Fitzgerald for noting the issues prompting the need for a patch. And all others who I may have forgotten.

import Control.Monad.Instances
import Control.Arrow
 
a, b :: (Int->Int) -> (Int,Int) -> (Int,Int)
a = fmap
b = second

Can you figure it out? If not, here’s a hint

f ::  ((Int -> Int) -> Int -> (Int, Int)) -> Int -> Int
f sec a = case sec (+1) a of (x,y) -> 6

The two functions, a and b, are identical for every single input, except one. Did you figure it out?

*Main> f a undefined
*** Exception: Prelude.undefined
*Main> f b undefined
6

Undefined, also called bottom or , is a subtle value in lazy languages like haskell and for certain types of programs, this can make a big difference. The functions a and b apply to as follows:

We say a function is strict if and is non-strict otherwise. Looking at the definition of fmap for tuples, we can see why it is strict in its second argument:

instance Functor ((,) a) where
	fmap f (x,y) = (x, f y)

Before evaluation even gets to the right hand side of the equal sign, it will return because it cannot pattern match (x,y) on undefined. We can make this non-strict in a couple ways, the first uses functions as an alternative to pattern matching:

instance Functor ((,) a) where
	fmap f t = (fst t, f (snd t))

The second uses the special tilde (~) symbol to delay the pattern matching until the result is actually used.

instance Functor ((,) a) where
	fmap f ~(x,y) = (x, f y)

And we see, the non-strict second function, is implemented as follows, using the tilde approach.

instance Arrow (->) where
-- ...
	first f = f *** id
	second f = id *** f
	(f *** g) ~(x,y) = (f x, g y)

Why non-strict?

At first glance, it might seem silly to implement functions non-strictly. After all, the earlier these functions fail out with bottom, the more efficient the program is in these cases. However, one particular point of interest is lazy streams.

Recall that the getContents :: IO [Char] function returns a lazy list of input characters. Lets create a couple functions that motivate extra laziness.

import IO
 
withNext :: [Char] -> [(Char,Char)]
withNext (a:a':as) = (a,a'):withNext (a':as)
 
main = do
  hSetBuffering stdout NoBuffering
  hSetBuffering stdin NoBuffering
  fmap withNext getContents >>= putStr . map fst

When I run this program (sorry windows users, this won’t work for you), and type “Hello World!”, here is what I get.

runhaskell test HeHlellol oW oWrolrdl!d

The underlined letters are the ones I typed. How did this happen? Note the following about withNext:

It is strict in the second half of its argument. Lets modify our function to be more lazy in this respect.

withNext' :: [Char] -> [(Char,Char)]
withNext' (a:as) = (a, head as):withNext as
-- Or, the tilde version
-- withNext' (a:(~(a':as))) = (a,a'):withNext (a':as)

As was the case with withNext, withNext' is strict in its argument.

Using this, we can see that withNext' is not strict in the second half of its argument.

When we run our more lazy version of this program, we get what we’d expect:

runhaskell test HHeelllloo WWoorrlldd!!

Connecting Strictness to Streams

As can be seen above, strictness and streams are tightly coupled. Here we present a theoretical evaluation () of a function at a given point in time. Here we introduce a new symbol we’ll call partial, , that represents a value that we have no information about at the given moment. represents a symbol where everything is known and all other variables could mean either. So, for our withNext' function above, we may write the following equations:

Note that our equations are the same as our strictness equations. Thus we may use these functions to prove invariants on our stream-based code.

Example from Reactive

Take the following mappend code from reactive:

instance Ord t => Monoid (FutureG t a) where
  -- ...
  -- Pick the earlier future.
  Future (s,a) `mappend` Future (t,b) =
    Future (s `min` t, if s <= t then a else b)

Using strictness analysis, we can come up with the following equations.

This tells us that if we do not know anything about the tuples in the Future arguments to mappend, then we cannot know anything about the result. So a developer might want to maintain an invariant that implies that .

Continuing on…

If we add some more invariants, we can go even further. Lets say that if we have the invariant that implies that min ( :: t) (x :: t) x and (<=) ( :: t) (x :: t) False. Then we get a Future that allows us to mappend now with a past future and a future future.

Verifying the the code is sufficiently lazy is now just a matter of seeing that these invariants are met.