Strongly-typed ghci commands

The ghci documentation explains how to implement conditional breakpoints by conditionally generating ghci commands depending on the values of variables which are in scope at the breakpoint. The approach works, but is hard to implement correctly because ghci's commands are stringly-typed. In this post, I will present a strongly-typed DSL for writing such commands in a type safe way, and I will use it to reimplement conditional breakpoints and to implement data breakpoints.

Data breakpoint demo

For future reference, here is how to define data breakpoints in ghci.

:def databreak \checkData -> return (":set stop :cmd (" ++ checkData ++ ") >>= \\hasChanged -> if hasChanged then return \":set stop :list\\n:back\" else return \":step\"")

That was unreadable, but that's kind of the point: multi-stage ghci commands are complex, which is why we need a DSL to make sense of them. For now, here's how you can use :databreak to find the step at which foo writes 2 to the IORef.

initIORef :: IO (IORef Int)
initIORef = newIORef 0

hasWrittenTwo :: IORef Int -> IO Bool
hasWrittenTwo ref = do
    value <- readIORef ref
    return (value == 2)

foo :: IORef Int -> [Int] -> IO ()
foo ref = mapM_ $ \x -> do
    print x
    writeIORef ref x

> ref <- initIORef
> :databreak (hasWrittenTwo ref)
> :step (foo ref [5,4,3,2,1])
[lots of forward stepping...]
foo ref = mapM_ $ \x -> do
    print x
    writeIORef ref x
    ^^^^^^^^^^^^^^^^
> x
2

By the end of the post, we'll be able to reimplement :databreak in a less succinct, but much more understandable style.

The status quo: stringly-typed commands

If you search for "conditional breakpoints" in the ghci documentation, you will see the following magic incantation (which I have split into multiple lines for readability):

:{
:def cond \expr -> return (":cmd if (" ++ expr ++ ") \
                                \then return \"\" \
                                \else return \":continue\"")
:}
:set stop 0 :cond (x < 3)

The meaning of the above is a multi-stage computation:

1. When breakpoint 0 is encountered, execute the command :cond (x < 3).
2. (x < 3) looks like an expression, but is actually the string "(x < 3)", which is passed to the definition of cond above.
3. The body of cond is an IO String computation. It returns a string which represents a ghci command.
4. That ghci command is: :cmd if ((x < 3)) then return "" else return ":continue".
5. The argument to :cmd is an expression of type IO String involving the variable x, which is assumed to be in scope in the code where breakpoint 0 is.

6. The IO computation returns one of two strings depending on the runtime value of x.

   If x is less than three,

   1. The condition for our conditional breakpoint has been triggered, so we should stop. The empty string is returned.
   2. This empty string is interpreted as a ghci command which does nothing. The multi-stage computation stops, as desired.

   If x is greater than or equal to three,

   1. The condition for our conditional breakpoint has not yet been triggered, so we should continue. The string ":continue" is returned.
   2. This string is interpreted as the ghci command :continue, which continues the execution until the next breakpoint is encountered. Go to 1.

There is a good reason why ghci is using strings to represent commands: as some of those commands are executed, the program being debugged progresses, which causes variables like x to enter the scope and others to leave it. Thus, at the moment when a command is defined, we don't yet have enough information to verify whether its definition is well-scoped.

Creating these kinds of multi-stage computations is a bit of a pain, because everything is a string and as a Haskell programmer, I need more precise types than that in order to reason about my program. It would be too easy to forget a :cmd or a return, producing a computation whose first stage type-checks, but which fails at runtime during the later stages.

> :{
> :def cond \expr -> return $ ":cmd if (" ++ expr ++ ") \
>                                  \then \"\" \
>                                  \else \":continue\""
> :}
> :set stop 0 :cond (x < 3)

The two commands above are accepted by ghci, because the expression given to :def has the required type String -> IO String, but we get a type error the first time the breakpoint is hit, much later than we'd like.

Making strings type-safe using phantom types

I have encountered this situation before while working on Hawk, an awk-like tool for manipulating text from the command-line via Haskell expressions. In the --map mode, Hawk applies the user expression to each line of stdin. This is implemented by embedding the user expression expr in the larger expression interact (unlines . map expr . lines), except with more complications due to other interfering features. To avoid making mistakes in this more complicated code, we came up with the following trick: instead of representing an expression as a raw string, we represent an expression of type a as a value of type S a. This is still a string under the hood, with an extra phantom type a documenting the purpose of the string's expression and allowing the type-checker to make sure we are using the string in the way we intended to.

data S a = S { runS :: String } deriving Show

To make use of S, I first need to define a few primitives corresponding to the many functions I might want to use inside my custom ghci commands. I need to be careful to specify the correct types here, as the type checker is not able to verify that the string I give corresponds to a function of the correct type. If I manage not to make any mistakes here, this will allow the type checker to prevent me from making mistakes later on, when combining those primitives into larger expressions.

sFmap :: Functor f => S ((a -> b) -> f a -> f b)
sFmap = S "fmap"

sReturn :: Monad m => S (a -> m a)
sReturn = S "return"

sIf :: S (a -> a -> Bool -> a)
sIf = S "\\t f b -> if b then t else f"

To combine those primitives, I can apply a string representing a function to a string representing an argument. The semantics for this operation is exactly the same as (<*>), but I cannot give an Applicative instance because my version of pure isn't polymorphic enough.

pureS :: Show a => a -> S a
pureS = S . show

(<.>) :: S (a -> b) -> S a -> S b
S f <.> S x = S ("(" ++ f ++ ") (" ++ x ++ ")")

Thanks to the type indices, Haskell can verify that I am constructing type-safe expressions, even though in the end I am still just concatenating strings.

-- Couldn't match expected type 'IO String' with actual type 'String'
sIncorrectExample :: S (Bool -> IO String)
sIncorrectExample = sIf <.> pureS ""
                        <.> pureS ":continue"

sCorrectedExample :: S (Bool -> IO String)
sCorrectedExample = sIf <.> (sReturn <.> pureS "")
                        <.> (sReturn <.> pureS ":continue")

> putStrLn $ runS sCorrectedExample
(\t f b -> if b then t else f) (return "") (return ":continue")

As the if..then..else example above demonstrates, computations expressed in terms of S primitives and (<.>) don't have access to the syntactic sugar we're accustomed to use in ordinary Haskell expressions. For this reason, it's often much more readable to define a new named function and to wrap it as a new primitive.

 namedExample :: Bool -> IO String
 namedExample True  = return ""
 namedExample False = return ":continue"
 
 sNamedExample :: S (Bool -> IO String)
 sNamedExample = S "namedExample"

Making ghci commands type-safe

There is another layer of stringly-typed imprecision in the above code: ":continue" is a plain old string, but not every string describes a valid ghci command. Let's create a newtype for those strings which do.

newtype C = C { runC :: String } deriving Show

No phantom type this time, since I'm not aware of any situation in which some commands would be allowed but not others.

continue :: C
continue = C ":continue"

back :: C
back = C ":back"

forward :: C
forward = C ":forward"

list :: C
list = C ":list"

step :: C
step = C ":step"

steplocal :: C
steplocal = C ":steplocal"

The :cmd and :def commands both expect a string argument, but since we know that this string is supposed to represent an IO computation, we should use S to specify that.

rawCmd :: S (IO String) -> C
rawCmd body = C $ ":cmd " ++ runS body

type Name = String
rawDef :: Name -> S (String -> IO String) -> C
rawDef name body = C $ ":def " ++ name ++ " " ++ runS body

A precisely-typed version of :cmd

We can do better than this. The IO computation given to :cmd doesn't return any string, it returns a string which represents a newline-separated sequence of commands.

import Data.List

-- compile from [C], the high-level representation of a list
-- of commands, to String, the low-level representation.
compileCmds :: [C] -> String
compileCmds = intercalate "\n" . fmap runC

sCompileCmds :: S ([C] -> String)
sCompileCmds = S "compileCmds"

We can thus make a safer version of rawCmd which asks for a computation returning a list of commands instead of a computation returning a string. We'll still be compiling to a string under the hood, but our users will have a much clearer picture of what they're doing.

cmd :: S (IO [C]) -> C
cmd body = rawCmd (sFmap <.> sCompileCmds <.> body)

A precisely-typed version of :def

For :def, it's a bit more difficult, because we would also like to give a precise type to the input string. It's a string given by the user, like the "(x < 3)" in our running example, which represents some expression. In the case of :cond, this is a boolean expression, and in order to keep things concrete, for now let's assume that this is always the case. Since the argument is a string representing a boolean expression, we can make its type more precise by using S Bool instead of String. So instead of S (String -> ...), we should use S (S Bool -> ...).

Yes, that's two nested S constructors. No, I'm not intentionally making this more complicated than it needs to be, I'm merely using the type system to make sense of the complexity which is already there. It means that :def's argument is a string representing a function which takes in a string which represents a boolean.

It's much easier to reason about this doubly-nested S if we first implement a function which compiles the precise representation S Bool -> IO [C] down to the imprecise representation String -> IO String, and then wrap that named function in an S constructor; the same trick we have used to improve readability.

-- using 'S a' instead of 'S Bool', to support any type of argument
compileDef :: (S a -> IO [C]) -> (String -> IO String)
compileDef body s = do
    cmds <- body (S s)
    return (compileCmds cmds)

sCompileDef :: S ((S a -> IO [C]) -> (String -> IO String))
sCompileDef = S "compileDef"

def :: String -> S (S a -> IO [C]) -> C
def name body = rawDef name (sCompileDef <.> body)

A strongly-typed version of :cond

> :{
> :def cond \expr -> return ":cmd if (" ++ expr ++ ")"
>     "then return \" \" "
>     "else return \":continue \""
> :}

Now that we have a type-safe version of :def, we can use it to rewrite the above definition of conditional breakpoints in a type-safe way.

defineCond :: C
defineCond = def "cond" sCond

cond :: S Bool -> IO [C]
cond expr = return [cmd (sCondHelper <.> expr)]

condHelper :: Bool -> IO [C]
condHelper True  = return []
condHelper False = return [continue]


sCond :: S (S Bool -> IO [C])
sCond = S "cond"

sCondHelper :: S (Bool -> IO [C])
sCondHelper = S "condHelper"

My version is more verbose because it is divided into several helper functions, which makes sense for a multi-stage computation.

1. There is the stage in which :def is called, with a string representing the second stage as an argument.
2. Then there is the cond stage, in which a custom command is constructed by concatenating two strings: one representing a computation expecting a boolean and one representing a boolean.
3. That computation is the next stage, condHelper, which uses the boolean to determine which commands to run next.
4. Those commands are the final stage.

Note that it would not have been correct to define those helpers in a where clause, because then the function names would no longer be in scope when ghci needs to interpret the code inside the strings. The trick we are using for readability is polluting the global namespace, which I think is a good tradeoff in the context of a blog post, but I wouldn't do that in a library.

Why not a monad?

To the eyes of a Haskeller, there is one more obvious API improvement which can be made: abstracting over the mechanism which separates the different stages and wrapping it up under a monadic interface, thereby allowing a multi-staged computation to be expressed as a single unified monadic computation. With such an API, instead of translating the definition of :cond to a bunch of helper functions like we did above, we would be able to express it via something like this:

defCond :: DSL ()
defCond = def "cond" $ \sBool -> do
    bool <- interpret sBool
    if bool
    then return ()
    else executeC continue

Unfortunately, it's not possible to implement such a monadic interface. Consider the type signatures for interpret and bind:

interpret :: S a -> DSL a
(>>=) :: DSL a -> (a -> DSL b) -> DSL b

Since S a is represented as a string, there is no way to obtain the underlying value of type a in order to pass it to bind's second argument. Instead, we would need to embed that argument, the monadic continuation, inside the string which we will eventually pass on to ghci. This leads to the following variant of bind:

bindDSL :: DSL a -> S (a -> DSL b) -> DSL b

With an appropriate representation for DSL, it is certainly possible to implement bindDSL. But then for readability purposes, we'd still be separating the implementation of the second argument into a separate function, so the end result would still be separated into approximately one function per stage. For this reason, I'll skip the details of this pseudo-monadic implementation.

Implementing data breakpoints.

A data breakpoint is a breakpoint which triggers not when the program reaches a particular line, but when a particular reference is assigned a new value. In a language in which each variable points to its own memory address, this can be implemented efficiently using a hardware breakpoint. Since GHC's garbage collector moves data around, changing their memory addresses, we'll have to use a much slower approach.

I plan to repeatedly use the :step command to advance the computation a tiny bit, checking between every step whether the reference I am interested is now pointing to a different value.

A strongly-typed version of :set stop

If we use :step when there is no computation is being debugged, there is nothing to step through, and ghci prints an error message. Unfortunately this message is visible to the user but not to our command, so we cannot use this error to determine when to stop stepping. So instead, I will use :set stop to specify that my command should be executed each time the execution is stopped, whether after stepping or after encountering a breakpoint.

setStop :: C -> C
setStop c = C (":set stop " ++ runC c)

Since there is only one stop hook, attaching my command will replace any other command which might have already been attached to it. I would like to restore that command once I'm done, but since there is no way to ask ghci which command is currently attached, I'll have no choice but to reset it to a convenient default instead. Most people use :set stop :list, which displays the source which is about to be executed.

resetStop :: C
resetStop = setStop list

A strongly-typed version of :databreak

Now that we have built all of the scaffolding, the definition of :databreak is straightforward. We hook up a stop command so that each time we stop, we check whether the data has changed. If it has, we detach the hook. Otherwise, we step forward and if the computation hasn't finished yet, our hook will trigger again. As a result, we keep stepping forward until either the data changes or the computation terminates.

defineDatabreak :: C
defineDatabreak = def "databreak" sSetDataBreakpoint

setDataBreakpoint :: S (IO Bool) -> IO [C]
setDataBreakpoint sCheckData = return [ setStop
                                      $ cmd
                                      $ sCheckAgain <.> sCheckData
                                      ]

checkAgain :: IO Bool -> IO [C]
checkAgain checkData = do
    hasChanged <- checkData
    if hasChanged
    then onDataChanged
    else return [step]

-- go back one step, since it's the previous step
-- which caused the data to change
onDataChanged :: IO [C]
onDataChanged = return [resetStop, back]


sSetDataBreakpoint :: S (S (IO Bool) -> IO [C])
sSetDataBreakpoint = S "setDataBreakpoint"

sCheckAgain :: S (IO Bool -> IO [C])
sCheckAgain = S "checkAgain"

sOnDataChanged :: S (IO [C])
sOnDataChanged = S "onDataChanged"

Let's try it out:

> putStrLn $ runC $ defineDatabreak
:def databreak (compileDef setDataBreakpoint)
> :def databreak (compileDef setDataBreakpoint)

> ref <- initIORef
> :databreak (hasWrittenTwo ref)
> :step (foo ref [5,4,3,2,1])
[lots of forward stepping...]
foo ref = mapM_ $ \x -> do
    print x
    writeIORef ref x
    ^^^^^^^^^^^^^^^^
> x
2

For convenience, I have expanded out and simplified the definition of defineDatabreak, thereby obtaining the easy-to-paste version from the top of the post.

Haxl anti-tutorial

It's time for another anti-tutorial! Whereas a tutorial is an advanced user giving step-by-step instructions to help newbies, an anti-tutorial is a new user describing their path to enlightenment. My approach is usually to follow the types, so my anti-tutorials are also examples of how to do that.

Previously in the series:

1. pipes anti-tutorial
2. reactive-banana anti-tutorial
3. netwire anti-tutorial

Today, inspired by a question from Syncopat3d, I'll try to learn how to use Simon Marlow's Haxl library. I think Haxl is supposed to improve the performance of complicated queries which use multiple data sources, such as databases and web services, by somehow figuring out which parts of the query should be executed in parallel and which ones should be batched together in one request. Since Syncopat3d is looking for a way to schedule the execution of a large computation which involves running several external processes in parallel, caching the results which are used more than once, and batching together the processes which use the same input, Haxl seemed like a good fit!

Black triangle

To understand the basics of the library, I'd like to create a black triangle, that is, a trivial program which nevertheless goes through the whole pipeline. So as a first step, I need to figure out what the stages of Haxl's pipeline are.

Since I'm using a type-directed approach, I need some type signature from which to begin my exploration. Hunting around Haxl's hackage page for something important-looking, I find GenHaxl, "the Haxl monad". Despite the recent complaints about the phrase "the <something> monad", finding that phrase here is quite reassuring, as it gives me a good idea of what to expect in this package: a bunch of commands which I can string together into a computation, and some function to run that computation.

Thus, to a first approximation, the Haxl pipeline has two stages: constructing a computation, and then running it.

A trivial computation

Since GenHaxl is a monad, I already know that return 42 is a suitably trivial and valid computation, so all I need now is a function to run a GenHaxl computation.

That function is typically right after the definition of the datatype, and indeed, that's where I find runHaxl. I see that in addition to my trivial GenHaxl computation, I'll need a value of type Env u. How do I make one?

Clicking through to the definition of Env, I see that emptyEnv can make an Env u out of a u. Since there are no constraints on u so far, I'll simply use (). I fully expect to revisit that decision once I figure out what the type u represents in the type GenHaxl u a.

>>> myEnv <- emptyEnv ()
>>> runHaxl myEnv (return 42)
42

(source)

Good, we now have a base on which to build! Let's now make our computation slightly less trivial.

What's a data source?

There are a bunch of GenHaxl commands listed after runHaxl, but most of them seem to be concerned with auxiliary matters such as exceptions and caching. Except for one:

dataFetch :: (DataSource u r, Request r a) => r a -> GenHaxl u a

That seems to be our link to another stage of Haxl's pipeline: data sources. So the first stage is a data source, then we describe a computation which fetches from the data source, then finally, we run the computation.

So, I want an r a satisfying DataSource u r. Is there something simple I could use for r? The documentation for DataSource doesn't list any instances, so I guess I'll have to define one myself. Let's see, there is only one method to implement, fetch, and it uses both u and r. The way in which they're used should give me a hint as to what those type variables represent.

fetch :: State r
      -> Flags
      -> u
      -> [BlockedFetch r]
      -> PerformFetch

I find it surprising that neither u nor r seem to constrain the output type. In particular, u is again completely unconstrained, so I'll keep using (). The description of the u parameter, "User environment", makes me think that indeed, I can probably get away with any concrete type of my choosing. As for r, which seems to be the interesting part here, we'll have to look at the definitions for State and BlockedFetch to figure out what it's about.

class Typeable1 r => StateKey r Source
    data State r

data BlockedFetch r
  = forall a . BlockedFetch (r a) (ResultVar a)

Okay, so State r is an associated type in an otherwise-empty typeclass, so I can again pick whatever I want. BlockedFetch r is much more interesting: it has an existential type a, which ties the r a to its ResultVar a. The documentation for BlockedFetch explains this link very clearly: r a is a request with result a, whose result must be placed inside the ResultVar a. This explains why r wasn't constraining fetch's output type: this ResultVar is the Haskell equivalent of an output parameter. So instead of being a pure function returning something related to r, this fetch method must be an imperative computation which fills in its output parameters before returning to the caller. The type of fetch's return type, PerformFetch, is probably some monad which has commands for filling in ResultVars.

data PerformFetch = SyncFetch (IO ()) | ...

At least in the simple case, PerformFetch is a simple wrapper around IO (), so I guess ResultVar must be a simple wrapper around MVar or IORef.

A trivial data source

Anyway, we now have a clear idea of what r a is: a request whose result has type a. Let's create a simple data source, Deep Thought, which only knows how to answer a single request.

data DeepThought a where
    AnswerToLifeTheUniverseAndEverything :: DeepThought Int

I'm using a GADT so that each request can specify the type of its answer. For example, I could easily add a request whose answer is a string instead of a number:

data DeepThought a where
    AnswerToLifeTheUniverseAndEverything :: DeepThought Int
    QuestionOfLifeTheUniverseAndEverything :: DeepThought String

But of course, Deep Thought isn't powerful enough to answer that request.

We also know that fullfilling a request isn't done by returning an answer, but by assigning the answer to a ResultVar.

runDeepThought :: DeepThought a -> ResultVar a -> IO ()
runDeepThought AnswerToLifeTheUniverseAndEverything var
  = putSuccess var 42

Alright, let's try to make DeepThought an official data source by implementing the DataSource typeclass:

instance DataSource () DeepThought where
    fetch _ _ _ reqs = SyncFetch $
        forM_ reqs $ \(BlockedFetch req var) ->
          runDeepThought req var

There's also a bunch of other easy typeclasses to implement, see the next source link for details.

A trivial state

I now have everything I need for my dataFetch to compile...

>>> runHaxl myEnv (dataFetch AnswerToLifeTheUniverseAndEverything)
*** DataSourceError "data source not initialized: DeepThought"

...but the execution fails at runtime. Now that I think about it, it makes a lot of sense: even though I don't use it, fetch receives a value of type State DeepThought, but since this is a custom type and I haven't given any of its inhabitants to anything, there is no way for Haxl to conjure one up from thin air. There must be a way to initialize the state somehow.

I must say that I'm a bit disappointed by how imperative Haxl's API has been so far. Whether we're assigning values to result variables or initializing a state, correctness requires us to perform actions which aren't required by the types and thus can't be caught until runtime. This is unusual for a Haskell library, and if the rest of the API is like this, I'm afraid following the types won't be a very useful exploration technique.

Anyway, I couldn't find any function with "init" in the name, but by looking for occurences of State in the types, I figured out how to perform the initialization: via the environment u which I had left empty until now.

instance StateKey DeepThought where
    data State DeepThought = NoState

initialState :: StateStore
initialState = stateSet NoState stateEmpty

>>> myEnv <- initEnv initialState ()
>>> runHaxl myEnv (dataFetch AnswerToLifeTheUniverseAndEverything)
42

(source)

It worked! We have a trivial data source, we have a trivial expression which queries it, we can run our expression, and we obtain the right answer. That's our black triangle!

Multiple data sources, multiple requests

Next, I'd like to try a slightly more complicated computation. Syncopat3d gives the following example:

F_0(x, y, z) = E(F_1(x, y), F_2(y, z))

Here we clearly have two different data sources, E and F. Syncopat3d insists that E is computed by an external program, which is certainly possible since our data sources can run any IO code, but I don't think this implementation detail is particularly relevant to our exploration of Haxl, so I'll create two more trivial data sources.

data E a where
    E :: String -> String -> E String
  deriving Typeable

data F a where
    F_1 :: String -> String -> F String
    F_2 :: String -> String -> F String
  deriving Typeable

runE :: E a -> ResultVar a -> IO ()
runE (E x y) var = putSuccess var (printf "E(%s,%s)" x y)

runF :: F a -> ResultVar a -> IO ()
runF (F_1 x y) var = putSuccess var (printf "F_1(%s,%s)" x y)
runF (F_2 x y) var = putSuccess var (printf "F_2(%s,%s)" x y)

Since GenHaxl is a monad, assembling those three requests should be quite straightforward...

>>> runHaxl myEnv $ do
...     f1 <- dataFetch (F_1 "x" "y")
...     f2 <- dataFetch (F_2 "y" "z")
...     dataFetch (E f1 f2)
"E(F_1(x,y),F_2(y,z))"

(source)

Batching

...but if I add a bit of tracing to my DataSource instances, I see that this computation is performed in three phases: F_1, F_2, then E.

>>> runHaxl myEnv ...
Computing ["F_1(x,y)"]
Computing ["F_2(y,z)"]
Computing ["E(F_1(x,y),F_2(y,z))"]
"E(F_1(x,y),F_2(y,z))"

(source)

This is not the trace I was hoping to see. Since fetch is receiving a list of request/var pairs, I expected Haxl to send me multiple requests at once, in case my data source knows how to exploit commonalities in the requests. But it doesn't look like Haxl figured out that the F_1 and F_2 requests could be performed at the same time.

It turns out that this is a well-known problem with Haxl's monadic interface. I remember about it now, it was described in a presentation about Haxl (slide 45) when it came out. The solution is to use the Applicative syntax to group the parts which are independent of each other:

>>> runHaxl myEnv $ do
...     (f1,f2) <- liftA2 (,) (dataFetch (F_1 "x" "y"))
...                           (dataFetch (F_2 "y" "z"))
...     dataFetch (E f1 f2)
Computing ["F_2(y,z)","F_1(x,y)"]
Computing ["E(F_1(x,y),F_2(y,z))"]
"E(F_1(x,y),F_2(y,z))"

(source)

Good, the F_1 and F_2 requests are now being performed together.

Style

I don't like the way in which we have to write our computations. Consider a slightly more complicated example:

E(
  E(F_1(x,y), F_2(y,z)),
  E(F_1(x',y'), F_2(y',z'))
)

Since the four F_1 and F_2 requests at the leaves are all independent, it would make sense for Haxl to batch them all together. But in order to obtain this behaviour, I have to list their four subcomputations together.

>>> runHaxl myEnv $ do
...     (f1,f2,f1',f2') <- (,,,) <$> (dataFetch (F_1 "x" "y"))
...                              <*> (dataFetch (F_2 "y" "z"))
...                              <*> (dataFetch (F_1 "x'" "y'"))
...                              <*> (dataFetch (F_2 "y'" "z'"))
...     (e1,e2) <- (,) <$> (dataFetch (E f1 f2))
...                    <*> (dataFetch (E f1' f2'))
...     dataFetch (E e1 e2)
Computing ["F_2(y',z')","F_1(x',y')","F_2(y,z)","F_1(x,y)"]
Computing ["E(F_1(x',y'),F_2(y',z'))","E(F_1(x,y),F_2(y,z))"]
Computing ["E(E(F_1(x,y),F_2(y,z)),E(F_1(x',y'),F_2(y',z')))"]
"E(E(F_1(x,y),F_2(y,z)),E(F_1(x',y'),F_2(y',z')))"

(source)

I feel like I'm doing the compiler's job, manually converting from the nested calls I want to write to the leaves-to-root, layered style I have to write if I want batching to work.

So I stopped working on my anti-tutorial and wrote a toy library which converts from one style to the other :)

...and when I came back here to show it off, I discovered that GenHaxl already behaved exactly like my library did! You just have to know how to define your intermediate functions:

f_1 :: GenHaxl () String -> GenHaxl () String -> GenHaxl () String
f_1 x y = join (dataFetch <$> (F_1 <$> x <*> y))

f_2 :: GenHaxl () String -> GenHaxl () String -> GenHaxl () String
f_2 x y = join (dataFetch <$> (F_2 <$> x <*> y))

e :: GenHaxl () String -> GenHaxl () String -> GenHaxl () String
e x y = join (dataFetch <$> (E <$> x <*> y))

And with those, we can now describe the computation as nested function calls, as desired.

>>> x = pure "x"
>>> y = pure "y"
>>> z = pure "z"
>>> x' = pure "x'"
>>> y' = pure "y'"
>>> z' = pure "z'"
>>> runHaxl myEnv $ e (e (f_1 x y) (f_2 y z))
...                   (e (f_1 x' y') (f_2 y' z'))
Computing ["F_2(y',z')","F_1(x',y')","F_2(y,z)","F_1(x,y)"]
Computing ["E(F_1(x',y'),F_2(y',z'))","E(F_1(x,y),F_2(y,z))"]
Computing ["E(E(F_1(x,y),F_2(y,z)),E(F_1(x',y'),F_2(y',z')))"]
"E(E(F_1(x,y),F_2(y,z)),E(F_1(x',y'),F_2(y',z')))"

(source)

Conclusion

I now understand Haxl's purpose much better. With the appropriate intermediate functions, Haxl allows us to describe a computation very concisely, as nested function calls. Haxl executes this computation one layer at a time: all of the leaves, then all the requests which only depend on the leaves, and so on. Within a single layer, the requests are subdivided again, this time according to their respective data sources. Finally, for a given data source, it is fetch's responsibility to find and exploit opportunities for reusing work across the different requests belonging to the same batch. There are also some features related to caching and parallelism which I didn't explore.

I also understand Haxl's implementation much better, having reimplemented part of it myself. In fact, I'd be interested in writing a follow-up post named "Homemade Haxl", in the same vein as my "Homemade FRP" series. What do you think? Are you more interested in watching me learn some new libraries, watching me reimplement libraries, or watching me implement new stuff? I'll be doing all three anyway, I just want to know which of those activities I should blog about :)

Really, your feedback would be greatly appreciated, as the only reason I started this anti-tutorial series in the first place is that my first write-up on understanding Pipes was so surprisingly popular. I've streamlined the format a lot since that first post, and I want to make sure I haven't lost any of the magic in the process!

The "99 Bottles of Beers" of Type Systems

"Hello World" is a good first example program because it is small, but also because it encourages the reader to get into the driver's seat and take control of the program. Copy-paste the "Hello World" listing from a website, and you're just blindly following instructions. Change it to print "Hello Mom", and you're boldly taking your first step towards the unknown, into a world where it is now you who is giving the instructions.

New programmers need to take that step, because programming anything non-trivial requires taking your own decisions about how things are implemented. If your boss was taking all the decisions for you, you wouldn't be a programmer, you'd be a typist.

The "Hello World" of Type Systems

Once you become an experienced programmer, "Hello World" examples are still useful as an introduction to new languages and new systems. Once you have a working base, you can experiment by making small changes and verifying whether they work as you expect, or if you need to read more tutorials.

For type systems, I guess a "Hello World" program would be a small datatype/structure/class containing a few simple fields. The standard here isn't as well-established as with "Hello World", but describing a person is quite common:

data Person = Person
  { name :: String
  , age :: Int
  }

I've used Haskell here, but regardless of the language in which I would have written this, you could still easily infer how to add a field for the person's height.

99 Bottles of Beer

A little down the road, another introductory program is "99 bottles of beer on a wall". This one teaches budding programmers another important lesson: it's possible to write a program which prints out more text than what you've written in its source code. More specifically, the program shows how to use a variable to abstract over the part of the text which varies from one iteration to the other, and how to use a loop to determine how many iterations to make and which value the variable should take in each one.

For type systems, a "99 bottles of beer" program would teach the same lesson: it's possible to write a program which uses larger types than those you've written in the source code. This is rarely needed, but it's possible! Even in a large, complicated application, you might have a manager of pools of worker threads processing lists of person values, but Manager (Pool (WorkerThread (List Person))) is still a fixed type which you write down explicitly in your program. It's as if you had abstracted out the number of beers to print, but then wrote explicit calls with n = 99, n = 98 and so on, instead of using a loop to generate the calls at runtime. Our "99 bottles of beer" example should generate types at runtime.

The "99 Bottles of Beer" of Type Systems

The simplest such example I could think of is as follows:

1. Parse a non-negative integer n from standard input or from a command-line argument.
2. If n is 0, print 42.
3. Otherwise, print the pair (x,x), where x is the text which would have been printed if n was one unit smaller. For example, the output for n = 3 should be "(((42,42),(42,42)),((42,42),(42,42)))".

With the important restriction that the pair (x, x) must first be constructed before being printed, and its representation must not have the same type as x.

An incorrect solution

The reason the restriction is important is that otherwise, it would be possible to implement the program using a single type, that of integer trees:

-- *not* a valid solution
data Tree a = Leaf a | Branch (Tree a) (Tree a)

showTree :: Show a => Tree a -> String
showTree (Leaf x)       = show x
showTree (Branch t1 t2) = printf "(%s,%s)" (showTree t1)
                                           (showTree t2)

printTree :: Tree Int -> Int -> IO ()
printTree v 0 = putStrLn (showTree v)
printTree v n = printTree (Branch v v) (n-1)

main :: IO ()
main = readLn >>= printTree (Leaf 42)

That program does not demonstrate that it's possible to write a program which uses larger types than those you've written in the source code.

Haskell solution

Instead of using the same type Tree Int at every iteration, we want to construct a sequence of larger and larger types:

0. Int
1. (Int,Int)
2. ((Int,Int),(Int,Int))
3. (((Int,Int),(Int,Int)),((Int,Int),(Int,Int)))
4. ...

In Haskell, this can be achieved via polymorphic recursion, meaning that we recur at a different type than the one which the current call is being instantiated at. For example, the call printTree 42 1 instantiates the type variable a = Int, while the recursive call printTree (42,42) 0 instantiates the type variable a = (Int,Int).

printTree :: Show a => a -> Int -> IO ()
printTree v 0 = print v
printTree v n = printTree (v,v) (n-1)

main :: IO ()
main = readLn >>= printTree 42

Polymorphic recursion is often used to recur on a smaller type, but since in this function it is the Int argument which is getting smaller, we can recur on a larger type without risking an infinite loop.

C++ solution

Speaking of infinite loops, C++ uses compile-time templates to handle polymorphic recursion, and this implementation strategy causes the compiler to instantiate more and more templates when we recur on a larger type. Eventually, gcc gives up with "template instantiation depth exceeds maximum of 900".

We can work around the problem by specializing the template at one of the types encountered before that limit, and printing an error message instead of recurring further.

#include <stdio.h>

template<typename A>
struct Pair {
  A fst;
  A snd;
  
  Pair(A fst, A snd)
  : fst(fst), snd(snd)
  {}
};

void print(int n) {
  printf("%d", n);
}

template<typename A>
void print(Pair<A> pair) {
  printf("(");
  print(pair.fst);
  printf(",");
  print(pair.snd);
  printf(")");
}

template<typename A>
void println(A value) {
  print(value);
  printf("\n");
}


template<typename A>
struct PrintTree {
  static void call(int depth, A value) {
    if (depth == 0) {
      println(value);
    } else {
      PrintTree<Pair<A> >::call(depth - 1, Pair<A>(value, value));
    }
  }
};

template<>
struct PrintTree<
  Pair<Pair<Pair<Pair<Pair<Pair<Pair<Pair<int>
> > > > > > > >
{
  static void call(int, Pair<
                          Pair<Pair<Pair<Pair<Pair<Pair<Pair<int>
                        > > > > > > >
  ) {
    fprintf(stderr, "maximum depth exceeded.\n");
  }
};

int main() {
  int depth;
  scanf("%d", &depth);
  
  PrintTree<int>::call(depth, 42);
  
  return 0;
}

Java solution

Other implementation strategies, such as Java's type erasure, need no such artificial bounds.

class Pair<A> {
  private A fst;
  private A snd;
  
  public Pair(A fst, A snd) {
    this.fst = fst;
    this.snd = snd;
  }
  
  public String toString() {
    return "(" + fst.toString() + "," + snd.toString() + ")";
  }
}

public class Main {
  public static <A> void printTree(int depth, A value) {
    if (depth == 0) {
      System.out.println(value.toString());
    } else {
      printTree(depth - 1, new Pair<A>(value, value));
    }
  }
  
  public static void main(String[] args) {
    Integer n = Integer.valueOf(args[0]);
    Integer m = 42;
    printTree(n, m);
  }
}

Conclusion

Many programming languages have the ability to work with larger types than those which are known at compile time, but for some reason, the feature is rarely used.

Perhaps one of the reasons is that the feature is rarely covered in tutorials. I have presented a small example demonstrating the feature, and I have demonstrated that the example isn't specific to one particular type system by implementing it in a few different languages. If you're writing a tutorial for a language and you have already covered "Hello World", "99 bottles of beer" and the "Hello World" of type systems, please consider also covering the "99 bottles of beer" of type systems.

Although, if I want this example to catch on, I should probably give it a better name. Maybe "Complete trees whose leaves are 42", or simply "Complete 42" for short?

How to package up binaries for distribution

This weekend, I wrote a game (in Haskell of course!) for Ludum Dare, an event in which you have 48h or 72h to create a game matching an imposed theme. It was really challenging!

Once the event was over, it was time to package my game in a form which others could play. Since the packaging procedure wasn't obvious, I'm documenting it here for future reference. The procedure isn't specific to Haskell, but I'll mention that linking Haskell programs statically, as advised around the web, didn't work for me on any platform.

Windows

While your program is running, use Process Explorer to list the .dll files your program is currently using (There is also Dependency Walker, but on my program it missed glut32.dll). Copy those DLLs to the same folder as your executable, zip the folder, and ship it.

OS X

Use otool -L to list the .dylib files on which your executable depends, and copy them to the same folder as your executable (or a libs subfolder). Use install_name_tool to change all the dylib paths embedded in your executable to @executable_path/foo.dylib (or @executable_path/libs/foo.dylib). Zip the folder, and ship it.

Linux

Use ldd to list the .so files on which your executable depends, and copy all of them except libc.so.X to the same folder as your executable (or a libs subfolder). Add ld-options: -Wl,-rpath -Wl,$ORIGIN (or ld-options: -Wl,-rpath -Wl,$ORIGIN/libs) to your cabal file, pass those flags directly to gcc, or use chrpath to change the existing RPATH if there is one. Zip the folder, and ship it.

Understanding "Strongly-typed Bound", part 1

First, giving credits where credit is due. The Bound library is written by Edward Kmett, and so is the strongly-typed variant I want to explore in this series. I learned about the strongly-typed version via a comment by geezusfreeek, in response to a question by _skp.

I have a lot to say about this script, and since the first thing I want to say about it involves writing down some typing rules, I thought I'd write them on the whiteboard and publish a video! Please let me know what you think of this new format.

Prisms lead to typeclasses for subtractive types

In my last post, I identified some issues with subtractive types, namely that math identities such as ∀ a. a + -a = 0, once they are translated into Haskell, would not be valid for all a. More precisely, the existence of a function of type

cancelSub :: forall a. (a :+: Negative a) -> Zero

would make it easy to implement a contradiction, regardless of the way in which we represent Negative a:

type a :+: b = Either a b
type Zero = Void

contradiction :: Void
contradiction = cancelSub (Left ())

I concluded by blaming the unconstrained forall. That is, I was hoping that the identity could be saved by finding some typeclass C such that C a => (a :+: Negative a) -> Void would be inhabited, or something along those lines. But what should C look like?

Prisms

Earlier today, I was re-listening to Edward Kmett on Lenses, in the first Haskell Cast episode. While explaining Prisms at 38:30, Kmett explained that a Lens' s a splits an s into a product consisting of an a and of something else, and that correspondingly, a Prism' s a splits an s into a sum consisting of an a and of something else. It occurred to me that the first "something else" should be s :/: a, while the second "something else" should be s :-: a.

Since Prism' s a is only inhabited for some combinations of s and a but not others, I thought a good choice for my C typeclass might be a proof that there exists a prism from s to a.

cancelSub :: HasPrism a (Negative a)
          => (a :+: Negative a) -> Void

That is, instead of restricting which types can be negated, let's restrict which types are allowed to appear together on the left- and right-hand sides of a subtractive type.

Four typeclasses

All right, so what should the HasPrism typeclass look like? In the podcast, Kmett explains that we can "construct the whole thing out of the target of a prism", and that we can pattern-match on the whole thing to see if it contains the target. In other words:

class HasPrism s a where
    construct :: a -> s
    match :: s -> Maybe a

This Maybe a discards the case I am interested in, the s :-: a. Let's ask the typeclass to provide a representation for this type, so we can give a more precise type to match.

class HasPrism s a where
    type s :-: a
    constructLeft :: a -> s
    constructRight :: (s :-: a) -> s
    match :: s -> Either a (s :-: a)

Our typeclass now has three methods, for converting back and forth between s and its two alternatives. We can combine those three methods into a single bijection, and with this final transformation, we obtain a form which is easily transferable to the other inverse types:

class Subtractable a b where
    type a :-: b
    asSub :: Iso a ((a :-: b) :+: b)

class Divisible a b where
    type a :/: b
    asDiv :: Iso a ((a :/: b) :*: b)

class Naperian b a where
    type Log b a
    asLog :: Iso a (Log b a -> b)

class Rootable n a where
    type Root n a
    asRoot :: Iso a (n -> Root n a)

Routing around the contradiction

The real test for these new definitions is whether they allow us to define constructive versions of the math identities for subtraction, division, logarithms and roots. Once annotated with the proper type class constraint, does cancelSub still lead to a contradiction? If not, can it be implemented?

It can!

type Negative a = Zero :-: a

cancelSub :: forall a. Subtractable Zero a
          => Iso (a :+: Negative a) Zero
         -- a :+: Negative a
cancelSub = swap
         -- Negative a :+: a
        >>> inverse iso
         -- Zero
  where
    iso :: Iso Zero (Negative a :+: a)
    iso = asSub

The math version of the constrained type is still ∀ a. a + -a = 0, but with a new proviso "whenever -a exists". It's still the same identity, it's just that with real numbers, -a always exists, so the proviso does not usually need to be spelled out.

In the world of types, Negative a does not always exist. If fact, there's only one possible instance of the form Subtractable Zero a:

instance Subtractable Zero Zero where
    type Zero :-: Zero = Zero
    
    asSub :: Iso Zero ((Zero :-: Zero) :+: Zero)
    asSub = Iso Right (either id id)

In other words, in the world of types, the proviso "whenever -a exists" simply means "when a = 0".

Other identities

I wish I could say that all the other identities become straightforward to implement once we add the appropriate typeclass constraints, but alas, this is not the case. I plan to discuss the remaining issues in a subsequent post.

For now, I am content to celebrate the fact that at least one contradiction has been slain :)

Edward Kmett likes my library :)

I have be re-listening to old episodes of the Haskell Cast, and it turns out I missed something really, shall we say, relevant to my interests.



In the very first episode, Edward Kmett talks about lens and a few of his other libraries. Then, near the end, he is asked about interesting Haskell stuff aside from his libraries. His answer, at 59:45:

"There was a really cool Commutativity monad [...] that really struck me as an interesting approach to things, I thought it was particularly neat toy."

— Edward Kmett

Yay, that's my library! And here are Wren's blog posts he mentions, about generalizing my approach.

Issues with subtractive types

I tried to expand on my earlier attempt at understanding root types, but I hit several obstacles. Here is a summary of those obstacles, in case future-me or someone else feels like trying again.

Goals

The conversation began with Naperian types, and the way in which they satisfy the same laws as mathematical logarithms, except at the type level. For example, the law log_b xy = log_b x + log_b y would translate to a function of type

logProduct :: Log b (a1, a2) -> Either (Log b a1) (Log b a2)

where, as usual, pairs represent multiplication and Either represents a sum. We would also expect a function with the converse type, and we would expect the two functions to form an isomorphism.

My goal would be to find implementations for Log and the other inverse types such that the corresponding isomorphisms exist and are useful. As the rest of the post will demonstrate, "exists" is already quite a strong requirement.

I should mention before moving on that yes, I am familiar with "The Two Dualities of Computation: Negative and Fractional Types", and I am intentionally using a different approach. Their non-deterministic invertible language in quite interesting, but ultimately too weird for me.

I would prefer to find a way to implement negative and fractional stuff as Haskell datatypes, or failing that, to understand why it can't be done. Today's post is about the latter: if negative and fractional types can exist in Haskell, then identities such as 0 ↔ x + -x wouldn't be valid for all types x, like they are in that paper.

Naïve definitions

Since subtraction is the inverse of addition, I tried to define a subtractive type and the other inverses types in term of the types we already have.

type a :+: b = Either a b
type a :*: b = (a, b)

data ab :-: b where
  MkSub :: a -> (a :+: b) :-: b

data ab :/: b where
  MkDiv :: a -> (a :*: b) :/: b

data Log b a where
  MkLog :: p -> Log b (p -> b)

data Root n a where
  MkRoot :: b -> Root n (n -> b)

One obvious problem with those definitions is that they don't support any of the math identities, except for the ones used in the definitions themselves: x + y - y = x, etc. For most types a, the type a :-: b isn't even inhabited, so while we might be able to implement absurd-style isomorphisms, the result would be completely useless.

Isomorphisms to the rescue

In the reddit comment linked at the top of this post, I worked around the problem via the hypothesis that maybe we shouldn't expect math identities to correspond to type isomorphisms so directly. Instead, I postulated an extra operator which would lift an isomorphism between a and a' to an isomorphism between a :-: b and a' :-: b, and similarly for the right-hand side and for the other type operators. It worked well enough, but since this transformation isn't constructive, we still don't get useful isomorphic functions at the end.

So, can we make the transformation constructive? Something like this:

data a :-: b where
  MkSub :: r -> Iso a (r :+: b) -> a :-: b

data a :/: b where
  MkDiv :: r -> Iso a (r :*: b) -> a :/: b

data Log b a where
  MkLog :: p -> Iso a (p -> b) -> Log b a

data Root n a where
  MkRoot :: b -> Iso a (n -> b) -> Root n a

By using id as the Iso, we can construct the same inhabitants as with the previous definitions. In addition, we can now constructively lift an isomorphism on the left- or right-hand side to an isomorphism on the whole type. The code for doing this is a bit longer than I'd like, but the idea is that since isomorphisms can already be lifted to either side of a (:+:), (:*:), or (->), we should therefore be able to concatenate an isomorphism for the left- or right-hand side with the existing Iso. For example:

liftRightAdd :: forall a b b'
              . Iso b b'
             -> Iso (a :+: b) (a :+: b')
liftRightAdd isoB = ...

liftRightSub :: forall a b b'
              . Iso b b'
             -> Iso (a :-: b) (a :-: b')
liftRightSub isoB = Iso fwdS bwdS
  where
    fwdS :: a :-: b -> a :-: b'
    fwdS (MkSub r iso) = MkSub r (liftIso iso)
      where
        liftIso :: Iso a (r :+: b) -> Iso a (r :+: b')
        liftIso iso = liftRightAdd isoB . iso
    
    bwdS :: a :-: b' -> a :-: b
    bwdS (MkSub r iso) = MkSub r (liftIso iso)
      where
        liftIso :: Iso a (r :+: b') -> Iso a (r :+: b)
        liftIso iso = liftRightAdd (inverse isoB) . iso)

With those tools, we should be able to take a non-constructive transformation like the one I wrote in my reddit comment:

log_b(a1) + log_b(a2) ~ Either (Log b a1) (Log b a2)
                     ≈≈ Either (Log b (p1 -> b))
                               (Log b (p2 -> b))
                      ≈ Either p1 p2
                      ≈ Log b (Either p1 p2 -> b)
                     ≈≈ Log b (p1 -> b, p2 -> b)
                     ≈≈ Log b (a1, a2)
                      ~ log_b(a1*a2)

And translate it into a constructive version:

addLogs :: forall a1 a2 b. Iso (Log b a1 :+: Log b a2)
                               (Log b (a1 :*: a2))
          -- Log b (a1 :*: a2)
addLogs = liftRightLog (liftBothMul (inverse asExp1)
                                    (inverse asExp2))
          -- Log b ((p1 -> b) :*: (p2 -> b))
        . liftRightLog expSum
          -- Log b (p1 :+: p2 -> b)
        . inverse logExp
          -- p1 :+: p2
        . liftBothAdd logExp logExp
          -- Log b (p1 -> b) :+: Log b (p2 -> b)
        . liftBothAdd (liftRightLog asExp1)
                      (liftRightLog asExp2)
          -- Log b a1 :+: Log b a2
  where
    asExp1 :: Iso a1 (P1 -> b)
    asExp2 :: Iso a2 (P2 -> b)

expSum :: Iso (a1 :+: a2 -> b)
              ((a1 -> b) :*: (a2 -> b))
logExp:: Iso (Log b (p -> b))
             p

Success? Not so fast.

Impossible isomorphisms

In order to execute the above constructive proof, we must of course implement all the smaller isomorphisms on which it is based. Two of them, asExp1 and asExp2, seem pretty silly: can we really expect any type a1 to be isomorphic to a function of the form p1 -> b, for any type b of our choosing?

I had originally postulated that I could do this because in my original definition for Log b a1, log types were only inhabited when a1 had the required form p1 -> b. With the new Iso-based definition, I'm no longer sure I can do this, and even with the old definition, it was only ever justified to transform Log b a1 into Log b (p1 -> b), not to transform a naked a1 into p1 -> b.

However, if we simply pick p1 = Log b a1, then the math identity b^{log_b x} = x justifies the principle. Can we write a constructive version of this identity?

One direction is easy:

mkExpLog :: a -> (Log b a -> b)
mkExpLog x (MkLog p (Iso fwd _)) = fwd x p

But the other direction direction is impossible. It would allow us to implement unsafeCoerce!

unExpLog :: (Log b a -> b) -> a

unsafeCoerce' :: b -> a
unsafeCoerce' = unExpLog . const

Similar issues occur with identities from the other inverse types. With a constructive version of the identity x - x = 0, for example, we can construct an inhabitant for the empty type:

unSubSelf :: a :-: a -> Void

subSelf :: [()] :-: [()]
subSelf = MkSub () (Iso fwdL bwdL)
  where
    fwdL :: [()] -> () :+: [()]
    fwdL []      = Left ()
    fwdL (():xs) = Right xs
    
    bwdL :: () :+: [()] -> [()]
    bwdL (Left  ()) = []
    bwdL (Right xs) = ():xs

bottom :: Void
bottom = unSubSelf subSelf

The fact that a recursive type is used in this counter-example hints at an explanation of the issue. The identity x - x = 0 is certainly true in math, for any number x. So at least for types with exactly x inhabitants, we would expect the isomorphism to hold. But in this case, the type [()] has infinitely-many inhabitants, and as we know from math, ∞ - ∞ is not zero, it's an indeterminate form.

Here is another implementation of the empty type, based on the identities x / x = 1 and x / y = x * (1/y):

mkDivSelf :: () -> a :/: a
mkTimesReciprocal :: a :/: b
                  -> a :*: (() :/: b)

divZero :: Void :/: Void
divZero = mkDivSelf ()

bottom' :: Void
bottom' = fst (mkTimesReciprocal divZero)

I haven't managed to derive a contradiction from any of the root identities, but they seem just as impossible to implement.

Restricted isomorphisms

Okay, so the indeterminate forms ∞ - ∞ and 0 / 0 both led to contradictions. In math, we work around the problem by saying that the division identities are only valid when the denominator is non-zero, and we don't even bother mentioning infinity because it's usually not a member of our universe of discourse, the real numbers for example.

In the world of types, instead of forbidding particular elements such as zero, it's much more common to require a witness proving that the types under consideration are valid for the current operation. In Agda, this would be a predicate on Set, while in Haskell, it would be a typeclass constraint. So, if future me is reading this and wants to continue exploring the world of inverse types, I leave him with the following recommendation: try looking for typeclass constraints under which the identities don't lead to contradictions, or even better, under which they can actually be implemented.

Homemade FRP: mystery leak

The mystery leak is back, and this time it's personal: the bug is clearly in my code somewhere.

My first hypothesis is that since I am emulating reactive-banana's API, and I now have the same kind of leak as I had with the real reactive-banana, maybe it's the same bug with the same solution? Nope, adding a <* stepper undefined events for each kind of event does not plug the leak.

My next attempt is to simplify: what is the simplest program I can write which reproduces the leak?

main :: IO ()
main = play (InWindow "Nice Window" (200, 200) (800, 200))
            white
            30
            (pure (Circle 10))
            currentValue
            (\_ -> handleEventB ())
            (\_ -> handleEventB ())

Obtained using the "-hy" flag; see Real World Haskell's chapter on profiling.
The rest of the profile information is useless: it says all the space is used by "MAIN".

That's as simple as main could get while still using gloss and my homemade FRP implementation. I already know that a pure (Circle 10) behaviour doesn't leak with gloss and the real reactive-banana, so clearly, the bug must be in my homemade version.

In order to simplify further, let's bring in the FRP primitives.

data Behavior t a = Behavior
  { currentValue :: a
  , runBehavior :: t -> Behavior t a
  }

pure :: a -> Behavior t a
pure x = Behavior x (\_ -> pure x)

handleEventB :: t -> Behavior t a -> Behavior t a
handleEventB = flip runBehavior

main :: IO ()
main = play (InWindow "Nice Window" (200, 200) (800, 200))
            white
            30
            (pure (Circle 10))
            currentValue
            (\_ -> handleEventB ())
            (\_ -> handleEventB ())

Still leaks; as expected, since I didn't really change anything yet.

I'm not using Behavior's ability to accept input events, so I can simplify further:

data Behavior t a = Behavior
  { currentValue :: a
  , runBehavior :: Behavior t a
  }

pure :: a -> Behavior t a
pure x = Behavior x (pure x)

main :: IO ()
main = play (InWindow "Nice Window" (200, 200) (800, 200))
            white
            30
            (pure (Circle 10))
            currentValue
            (\_ -> runBehavior)
            (\_ -> runBehavior)

I don't know why the colours have changed, but clearly, it's still leaking.
(spoiler alert: the colour change will turn out to be important)

Usually, space leaks are due to insufficient strictness. I waste a bit of time adding bangs and seqs here and there, but of course, the application is already strict: in order to display each Picture, gloss is forced to fully-evaluate each step.

Still, just to validate that gloss really is doing the simple iterative loop I think it is doing, I replace play with my own loop.

main :: IO ()
main = loop (pure (Circle 10))
  where
    loop b = do
        print (currentValue b)
        loop (runBehavior b)

Compared with the previous graph, it looks like the memory is now high all the time,
but look at the Y axis: the memory usage is now constant, and much smaller than before.

Interesting, the leak is gone! Could the leak be in gloss after all? To make absolutely sure, I go back to my full, unsimplified program, and I replace its top-level by a similar loop.

main :: IO ()
main = loop (reactiveMain floats inputs)
  where
    floats = inputEvents
    inputs = never
    
    loop b = do
        print (currentValue b)
        loop (handleEventB 1.0 b)

This time, the colour change is expected, because the program is completely different.
But did you expect the leak to be back?

Nope, it's not gloss. Or at least, it's not just gloss: I observe a leak when I use a gloss loop with a simple update function (G and ¬U), I also observe a leak when use a simple loop with a complex update function (¬G and U), but I don't see a leak when I use the simple loop with the simple update function (¬G and ¬U). Therefore, there is probably a leak in gloss (G), and a second leak in the complex update function (U). That's why the graph colours changed: the different programs are illustrating different leaks.

I begin with the complex update function; since I wrote all the code, I should be able to understand the problem better.

The update function leak

The profile data is very different this time, and also very useful. It's no longer Behavior which uses up all the space: it's lists, and the profiling report (obtained with "-p") even tells us where to look:

COST CENTRE     MODULE    %time %alloc

main.loop       Main       78.0   75.8
accumE.go.(...) PureFrp     5.9    8.2
filterE.go      PureFrp     2.1    4.3
fmap            PureFrp     2.0    2.6
accumE.go       PureFrp     1.5    2.7
mappend         PureFrp     1.3    1.3
accumE.go.xs    PureFrp     1.1    1.5

accumE is indeed manipulating lists: it uses scanl to produce a list of intermediate values, obtained by accumulating all the events occurring this frame. Let's add some strictness to that list:

accumE :: a -> Event t (a -> a) -> Event t a
accumE x e = Event go
  where
    go t = x' `seq` (xs', accumE x' e')
      where
        (fs, e') = runEvent e t
        xs = scanl (flip ($)) x fs
        x' = last xs
        xs' = tail xs  -- skip the initial unmodified x

Leak fixed. Next!

One leak down, one to go. Before we move on, though, I'd like to understand why strictness is needed in this particular function.

Let's see, each time a Float event comes in, reactiveMain is called and its current value is fully evaluated. Somewhere inside reactiveMain, there is a call to accumE, and without the extra strictness annotation, we know that accumeE's current value (the xs list and the x' it contains) doesn't get evaluated. Why not?

There is more than one use of accumE in reactiveMain, but the one in firstEvent looks particularly fishy:

firstEvent :: Event t a -> Event t a
firstEvent = fmap snd
           . filterE ((== 1) . fst)
           . numberEvents

numberEvents uses accumE to pair each event with an incrementing number. But for all events except the first one, we only evaluate the numeric half of the pair; could it be that the right-hand side is accumulating thunks?

Given the fact that a single seq was sufficient to solve the problem, that seems unlikely. After all, seq only forces x' to WHNF; depending on the implementation of numberEvents, that might either mean evaluating the outer pair or the incrementing number, but definitely not the inner members of the pair.

And indeed, if we revert the seq fix and remove firstEvent from the equation, the leak returns:

firstEvent is not the problem here.

There is another occurrence of numberEvents inside clickEvents. This location is interesting because I have noticed that clicking on a button causes a lot of extraneous memory to be released.

clickEvents :: Event t (Char, Int)
clickEvents = fmap swap
            $ numberEvents
            $ clickLabels

To explain the memory release, Float and click events must somehow be evaluated differently: one accumulates thunks, while the other evaluates them. And there is indeed a big difference: clickEvents ignores all the Float events, and only reacts to clicks. So how is ignoring events leading to thunk accumulation?

Well, ignoring events simply means filtering them out of the list of input events, which means that most of the time, clickEvents is going to be receiving an empty list as input and producing an empty list as output. This empty list gets fully-evaluated on every frame, in order to confirm that there is nothing to update on the screen, but that doesn't mean that all the thunks get forced: x', for example, is not a member of this empty list.

Let's look at the code for accumE again:

accumE :: a -> Event t (a -> a) -> Event t a
accumE x e = Event go
  where
    go t = (xs', accumE x' e')
      where
        (fs, e') = runEvent e t
        xs = scanl (flip ($)) x fs
        x' = last xs 
        xs' = tail xs  -- skip the initial unmodified x

scanl always returns a non-empty list starting with x, which is why we can call partial functions like last and tail without fear. Also, since x is passed through without being examined, any thunks accumulated to compute x will be passed through without being evaluated. In this case, it's the calls to last which will accumulate.

The reason the memory gets released when a button is clicked is that x is also involved in the computation of the elements of the output list, so as soon as this output list becomes non-empty and its elements get fully-evaluated, so does x. With the new strictness annotation, just evaluating the output list to WHNF is now sufficient to evaluate the next x to WHNF, thereby fixing the leak.

The gloss leak

Let's look into the second leak now, the one which occurs when I use gloss with a simple update function.

data Behavior t a = Behavior
  { currentValue :: a
  , runBehavior :: Behavior t a
  }

pure :: a -> Behavior t a
pure x = Behavior x (pure x)

main :: IO ()
main = play (InWindow "Nice Window" (200, 200) (800, 200))
            white
            30
            (pure (Circle 10))
            currentValue
            (\_ -> runBehavior)
            (\_ -> runBehavior)

If it's really a bug in gloss, then I should be able to reproduce it without any FRP-related stuff at all. Simplified as it is, a Behaviour t a is isomorphic to [a], and pure x isomorphic to repeat x. Can gloss handle infinite lists?

main :: IO ()
main = simulate (InWindow "Nice Window" (200, 200) (800, 200))
                white
                30
                [0..]
                (renderInt . head)
                (\_ _ -> tail)

Nope, it can't.

Okay, so this is an extremely simple gloss program exhibiting a clear memory leak, so even if I can't find the leak myself, I should be able to send this example program to the gloss developers as a bug report. Still, where does the profiler say that the issue is?

COST CENTRE   MODULE                                 %time %alloc

MAIN          MAIN                                    89.2  71.8
main          Main                                    6.7    0.0
CAF           Graphics.Rendering.(...).Functions      1.4    0.0
CAF           GHC.IO.Encoding                         1.2    0.0
callbackIdle  Graphics.Gloss.Internals.(...).Idle     0.6   13.7
drawComponent Graphics.Gloss.Internals.(...).Picture  0.3    9.5
fromList      Main                                    0.2    4.8

It looks like callbackIdle would be a good place to start. Looking at the code, this cost center is actually a function named callback_simulate_idle. Here is a slightly simplified version:

-- | Called when we're finished drawing
-- and it's time to do some computation.
callback_simulate_idle
 :: IORef SM.State  -- ^ the simulation state
 -> IORef world   -- ^ the current world
 -> world   -- ^ the initial world
 -> (Float -> world -> IO world) -- ^ advance the world
 -> IO ()
 
callback_simulate_idle simSR worldSR worldStart worldAdvance
 = {-# SCC "callbackIdle" #-}
   do simS <- readIORef simSR
 let result | SM.stateReset simS
            = simulate_reset simSR worldSR worldStart

            | SM.stateRun   simS
            = simulate_run   simSR worldSR worldAdvance
 
            | SM.stateStep  simS
            = simulate_step  simSR worldSR worldAdvance
 
            | otherwise
            = \_ -> return ()
 
 result

The memory is probably being allocated every time worldAdvance is called, but it's another value which catches my eye: worldStart? Why would the idle function need to remember the starting state? I see that it's being used when we want to "reset". I didn't know gloss allowed you to reset to the start state.

This reset feature explains the leak: in order to reset to the start state, gloss need to keep a pointer to the head of the infinite list, which prevents elements from being garbage-collected after being displayed.

Well, this is problematic. How to fix the leak while retaining the ability to reset the state? If the start state was obtained by calling a function, then the infinite lists returned by different invocations of this function would not be shared, thereby allowing the elements to be garbage-collected. But that's not the API gloss uses: play receive the start state directly, not as a wrapping function returning the start state. And creating our own function returning this constant state wouldn't help, because the function would hold a pointer to the head of the list, which would again prevent the garbage collection.

Anyway, I'm quite curious about this reset feature by now, so I look in the code for the key combination which triggers it, to no avail. In fact... it doesn't seem like the reset feature can be triggered at all? It's dead code! Along with plenty of other code which also looks dead. If fact, of the above four cases, only the simulate_run branch is ever taken.

This is weird, but it's actually great news for the memory leak. After removing all the dead code, the reference to worldStart is no longer kept alive after the first step, and the leak goes away.

The sweet plateau of fixed space leaks.

Conclusion

It can be hard to reason about a bug, be it a space leak or otherwise, when your assumptions are flawed. In this case, I had assumed that there was only one leak, when in fact there were two.

The key to uncovering incorrect assumptions is to run lots of sanity checks. In this case, after I had concluded that the leak had to be in gloss, I tested this hypothesis by removing gloss from the unsimplified version of my program, expecting the leak to disappear. When it didn't, I knew that one of my assumptions had to be flawed.

When that happens, one tedious but very effective weapon is to simplify the program: in a smaller program, there are fewer places for incorrect assumptions to hide. It also simplifies chains of reasoning, by not having lots of elements through which to chain.

Homemade FRP: a study in following the types

I wonder how FRP is implemented? Since I only know about a small part of reactive-banana so far, this is the interface I am currently thinking of when I think of FRP:

data Event t a
data Behavior t a

instance Functor (Event t)
instance Functor (Behavior t)
instance Monoid (Event t)
instance Applicative (Behavior t)

filterE :: (a -> Bool) -> Event t a -> Event t a
accumE :: a -> Event t (a -> a) -> Event t a
stepper :: a -> Event t a -> Behavior t a

I have omitted never and union, because they are just mempty and mappend from Monoid. I have also omitted accumB, because my understanding is that accumB x e is just a more efficient version of stepper x (accumE x e), and I am not concerned at all about efficiency yet.

Interactivity

So, how do I implement this interface? Could I represent Event as a map from timestamp to values, for example? It sounds like this representation would admit an implementation for all the required functions, but that would not allow me to handle events as they come, like I can do with gloss-banana. I would have to open the window, and let the user click around without being able to update the display. After accumulating all the mouse events, I would gather them into one big map, an Event t InputEvent, from which I could construct an Event t Picture. At this point, I would know exactly what I should have displayed after each of the mouse clicks, but it would be too late for that. Clearly, I need to find a way to obtain the early outputs before I learn about the later inputs...

With a list instead of a map, I can think of at least two laziness-based approaches for this kind of problem, but I'm not ready for a clever implementation yet. Let's keep things simple!

I said that a map-based representation would not allow me to handle events as they come. So clearly, being able to handle events as they come should be part of my API. What would a function for handling a new event look like?

handleInputEvent :: InputEvent -> Event t a -> IO (Maybe a)

I give the next InputEvent, the Event decides what it wants to do with it, and optionally triggers an event of type a based on it. But it's weird to have such a concrete type as InputEvent; surely reactive-banana isn't aware of the specifics of the event types supported by gloss. Event should have a type parameter indicating which type of input events it expects. Oh! Maybe that's what the t is for?

handleEvent :: t -> Event t a -> IO (Maybe a)

Much better. You might wonder why I am returning an IO action instead of a pure Maybe a: it's because of accumE. Accumulating the values of the events as they come requires storing an intermediate state somewhere, and a pure function would not be able to store its new state anywhere.

Well, I don't want to be stuck inside IO yet, so let's thread this state explicitly:

handleEvent :: t -> Event t a -> (Maybe a, Event t a)

I give the next t-valued input event, the Event decides what it wants to do with it, and optionally triggers an event of type a. The Event might have changed its internal state somehow, so it also returns a modified copy of itself, one which is ready to receive the next event.

Event

I now have a much clearer idea of the way in which I am going to use (or "eliminate", in type-theory-speak) values of type Event, but I'm no closer to figuring out how to represent those Event values. Or am I? When a type has a single (or a most general) eliminator, we can just use that eliminator as a representation:

data Event t a = Event
  { runEvent :: t -> (Maybe a, Event t a)
  } deriving Functor

handleEvent = flip runEvent

Is this representation good enough? Can the rest of the API be implemented on top of it? As I get stuck trying to implement union, I remember that one input event can cause more than one output event to be emitted at the same time. I make a small adjustment:

data Event t a = Event
  { runEvent :: t -> ([a], Event t a)
  } deriving Functor

With this representation, I can easily derive an implementation for the first few combinators, simply by following the types. A good sign!

instance Monoid (Event t a)
  where
    mempty = Event (const ([], mempty))
    e1 `mappend` e2 = Event go
      where
        go t = (xs1 ++ xs2, e1' <> e2')
          where
            (xs1, e1') = runEvent e1 t
            (xs2, e2') = runEvent e2 t

filterE :: (a -> Bool) -> Event t a -> Event t a
filterE p e = Event go
  where
    go t = (filter p xs, filterE p e')
      where
        (xs, e') = runEvent e t

Interlude: on the technique known as "follow the types"

Following the types is a technique which allows a function to be implemented very quickly, by taking decisions based on the types of the values involved instead of their meaning. Since it happens so quickly, it's a process which is a bit difficult to describe, as stopping in the middle of it in order to take notes will break the magic. Here is an attempt at reconstructing the magic after the fact.

First, let's dispel a possible misconception: I'm not a human version of djinn. That is, when I "follow the types", I do not blindly pick a random expression of the expected type, hoping it will be correct. Instead, I use the types as a shortcut when there is only one obvious way to go forward, and otherwise I pick an expression which fits the immediate context.

For example, in the code for filterE, I begin with the Event constructor, I pass it an intermediate function receiving a value of type t, and I eliminate the e argument using its only eliminator and the only value of type t I have on hand. I did not waste any time on those uninteresting details, because there are simply no alternatives to consider.

The call to filter p xs, on the other hand, is deliberate: a simple xs would have had the same type, but would have been incorrect. Yet the reason I used filter was not because I stopped to think about correctness; that would have involved reasoning based on the meaning of the values. Instead, I knew from the start that I wanted to filter out values of type a. It is the context of implementing an event-filtering function which guided me through the non-forced parts of the implementation: as I was following the types, I was on the lookout for values of type a or [a], ready to filter them on sight. This kind of context is also the reason why I used [] in the definition of mempty, versus (++) in the definition of mappend.

A very different example of context is that of the recursive call to filterE p e', where e and e' would have also type-checked. This part of the implementation is in a recursive position for Event t a, just like the tail is a recursive position for lists. In such a recursive context, I naturally picked a recursive expression, of the proper type of course, and using smaller arguments where possible.

Simplification

After a type-based implementation, I like to take a moment to go beyond the types and examine the meaning of all the values involved. Reading the code I just blindly wrote for never/mempty, the Event in which no event ever occurs, I see that the first input event is ignored, and that no output events are produced in response. Afterwards, recursively, no event ever occurs, and that's exactly what I want.

This reviewing phase is also a good opportunity for simplifications, such as replacing (\_ -> ...) with const or rearranging the pieces in a pointfree style. One simplification opportunity I notice is that [] is the mempty for lists, and (mempty, mempty) is the mempty for pairs, and const mempty is the mempty for functions. This, and a similar chain for mappend, allows the Monoid implementation to be simplified greatly:

instance Monoid (Event t a)
  where
    mempty = Event mempty
    Event e1 `mappend` Event e2 = Event (e1 `mappend` e2)

In this version, all the details are implicit, so much so that it's hard to follow the meaning of the values. But it's also a much more elegant implementation, and I've just read and understood the expanded-out version anyway, so I'm confident that the meaning is what I expect.

Behavior

The workflow for Behavior and its combinators is very similar to Event, so let's go through it quickly.

How do I represent/eliminate a Behavior? Probably the same way I eliminate events, except that behaviours have a value at every point in time, so I should receive exactly one a instead of a (potentially-empty) list of them.

data Behavior t a = Behavior
  { runBehavior :: t -> (a, Behavior t a)
  } deriving Functor

Trying to implement stepper, I realize that a behaviour is also supposed to hold a value before the very first event, and also between events. I need a second eliminator:

currentValue :: Behavior t a -> a

Now I have two eliminators. What would be a most general eliminator, from which the two others could be implemented?

generalEliminator :: Behavior t a -> (a, t -> Behavior t a)

I no longer need an a on the right-hand side of the (t -> ...), because currentValue can extract this a from the returned behaviour. I transform this most general eliminator into a representation for Behavior, giving convenient names to the pair's two components:

data Behavior t a = Behavior
  { currentValue :: a
  , runBehavior :: t -> Behavior t a
  } deriving Functor

Following the types is very straightforward this time.

instance Applicative (Behavior t)
  where
    pure x = Behavior x fx
      where
        fx _ = pure x
    Behavior f ff <*> Behavior x fx = Behavior (f x) fy
      where
        fy t = ff t <*> fx t

As before, this can be simplified: (\_ -> x) is the pure x for functions, and thus fx could be written as pure (pure x). Similarly, fy could be written by nesting two (<*>), whatever that means. This hints at a variant implementation of Behavior based on Compose, which will hide the details of the nesting:

data Behavior t a = Behavior
  { currentValue :: a
  , runBehavior :: Compose ((->) t) (Behavior t) a
  } deriving Functor

instance Applicative (Behavior t)
  where
    pure x = Behavior x (pure x)
    Behavior f cf <*> Behavior x cx = Behavior (f x) (cf <*> cx)

I'm not convinced that this variant is actually better, because the other combinators don't benefit from Compose: they just peel off the Compose layer, do their work, and put it back on. Speaking of the other combinators, I've skipped two of them in my exposition. I left them for the end, because...

When following the types leads nowhere

The last two combinators don't fit the mantra of following the types very well. Here is part of accumE:

accumE :: a -> Event t (a -> a) -> Event t a
accumE x e = Event go
  where
    go t = (_xs, ...)
      where
        (fs, e') = runEvent e t

The next step is to find an expression of type [a] for _xs. Unused values include fs, of type [a -> a], and x, of type a. One obvious and type-correct way to combine those two values is to apply all the functions in the list to x:

        _xs = fmap ($ x) fs

But we're in an accumulator context, so I'm expecting something like a fold instead. When something doesn't seem right, it's best to stop following the types and switch to "figure out what I'm trying to do" mode.

In this case, what I am trying to do is to thread the x through all the functions, returning all the intermediate values. It turns out there is a standard library function for that, scanl:

accumE :: a -> Event t (a -> a) -> Event t a
accumE x e = Event go
  where
    go t = (xs', accumE x' e')
      where
        (fs, e') = runEvent e t
        xs = scanl (flip ($)) x fs
        x' = last xs
        xs' = tail xs  -- skip the initial unmodified x

If I was more familiar with scanl, I could have used it without thinking, remaining in follow-the-types mode. But then I wouldn't have thought to skip scanl's initial copy of x, I might have recurred with x instead of last xs, and everything would have been completely wrong.

My implementation for the last combinator is also quite wrong:

stepper :: a -> Event t a -> Behavior t a
stepper x e = Behavior x (Compose go)
  where
    go t = stepper x e'
      where
        (xs, e') = runEvent e t

I did not use xs, and as a result, I recur on the wrong x. Here is what I should have written instead:

stepper :: a -> Event t a -> Behavior t a
stepper x e = Behavior x (Compose go)
  where
    go t = stepper (last (x:xs)) e'
      where
        (xs, e') = runEvent e t

The only trick here is that I prepend x to xs in order to ensure that the argument to last is non-empty.

Conclusion

Following the types didn't work for every single combinator, but when it did work, it quickly produced a correct implementation on the first attempt.

Yup, it's working!
It even has the same leak-until-clicked behaviour as the original :)

When it didn't work, following the types did not lead to any wasted work. For ease of presentation, I have shown an incorrect type-based version followed by a corrected meaning-based version, but during my original implementation, there wasn't a sharp break between the two phases. Like I said, it all happens very quickly, so it's hard to describe exactly what is going on inside my head when I code. I think I always focus on the correctness of what I write. It's just that over time, I have learned that when the types which are in scope are sufficiently distinct, it's okay for "correct" to mean simply "type-correct". Whereas at other times, perhaps mere seconds later, it becomes important to understand what the values actually mean.

If you came here to learn how to follow the types yourself, and you're disappointed by my vague explanations, don't be. I did not set out to learn to follow the types; I just wrote lots of Haskell code, and my brain learned to focus on the types when appropriate. You'll get there, don't worry.

reactive-banana mystery leak

So I accidentally let my reactive-banana toy app opened all night, and in the morning the computer was horribly unresponsive until I killed it. After starting a new instance, I noticed that the CPU goes up from ~5% to 100%, during which the memory usage also grows uncontrollably. What is causing this?

The first thing I try is to lower the refresh rate at which gloss recomputes its frames, in case the problem is that the computer can't keep up with the work it has to do. The resource usage still increases, but much more slowly. Next, I try to isolate the commit in which the problem was introduced. Did the problem exist when I was using gloss, but not reactive-banana? No. Git-bisecting, I find that the problem was introduced by commit 66f4e7, "accumulating clicks":

@@ -27,13 +28,31 @@ reactiveMain :: forall t. Frameworks t
              => Event t Float
              -> Event t InputEvent
              -> Moment t (Behavior t Picture)
-reactiveMain floats _ = return pictures
+reactiveMain floats events = return pictures
   where
-    partialSums :: Behavior t Float
-    partialSums = accumB 0 (fmap (+) floats)
+    buttonClicks :: [Event t ()]
+    buttonClicks = map (flip buttonClick events) buttons
+    
+    countA,countB,countC :: Behavior t Int
+    [countA,countB,countC] = map countEventsB buttonClicks
+    
+    clickCounts :: Behavior t (Int,Int,Int)
+    clickCounts = liftA3 (,,) countA countB countC
     
     pictures :: Behavior t Picture
-    pictures = fmap renderFloat partialSums
+    pictures = fmap render clickCounts
+
+countEventsB :: Num a => Event t b -> Behavior t a
+countEventsB = accumB 0 . fmap (+) . fmap (const 1)
+
+buttons :: [Extent]
+buttons = [extentA, extentB, extentC]
+
+buttonClick :: Extent -> Event t InputEvent -> Event t ()
+buttonClick ex = fmap (const ()) . filterE isInside
+  where
+    isInside (EventKey (MouseButton LeftButton) Down _ p) = pointInExtent ex p
+    isInside _                                            = False
 
 renderFloat :: Float -> Picture
 renderFloat = uscale 0.2 . text . show

This is the commit in which I switched from displaying the accumulated time to displaying the number of accumulating clicks on three buttons.

After a little more experimentation, I notice that the CPU and memory get released whenever I click on one of the buttons. Weird! Which special thing happens when I click one of the buttons? Well, one thing is that the graphics change. What if I force the graphics to change all the time by displaying the running elapsed time? The problem disappears. That's good, but I don't want to display the running elapsed time. Can I instead compute the running time, but display a fixed string? Embarrassingly, the first time I tested this I forgot to force the computed value, so the problem reappeared. When I do force the value, the problem remains hidden.

Ok, so I don't understand why the CPU usage would go up, but the memory increase seems to be due to a laziness issue.

I wish I could use ghci to step through the code, but the app hangs when I do. Seems to be an issue with gloss, not reactive-banana. Maybe if I disable the timed updates by setting the refresh rate to zero? Still hangs, but the leak disappears. Which is not a surprise, really: the fact that the leak grew more slowly when the refresh rate was lower clearly indicates that the leak is caused by the Float events.

Or it is that clear? With the refresh rate set to zero, there are no Float events, and at first the leak doesn't seem present. But if I click outside the buttons or move the mouse a lot, this generates a bunch of ignored events, which causes the memory to rise. Since this is not how I have previously been testing the leaks, I re-perform the git-bisect with a refresh rate of zero, and discover that the problem was actually introduced by commit 1386bf, "accumulating time":

@@ -18,7 +21,19 @@ main :: IO ()
 main = playBanana (InWindow "Nice Window" (200, 200) (800, 200))
                   white
                   30
-                  (\floats _ -> return $ fmap renderFloat $ stepper 0 floats)
+                  reactiveMain
+
+reactiveMain :: forall t. Frameworks t
+             => Event t Float
+             -> Event t InputEvent
+             -> Moment t (Behavior t Picture)
+reactiveMain floats _ = return pictures
+  where
+    partialSums :: Behavior t Float
+    partialSums = accumB 0 (fmap (+) floats)
+    
+    pictures :: Behavior t Picture
+    pictures = fmap renderFloat partialSums

This is the commit in which I switched from displaying the Float values to displaying the sum of all Float values so far. Interestingly, I am not even using the mouse events in my FRP computation, so the problem can't possibly be that my code is doing something it shouldn't. Maybe there is something it should do which it isn't doing? Perhaps I should be actively consuming and ignoring the events, instead of simply not using them?

reactiveMain floats events = return pictures
  where
    pictures :: Behavior t Picture
    pictures = fmap renderFloat partialSums <* stepper undefined events

It works! In the most recent commit, which handles mouse events but filters out most time events, it is the floats which must be ignored. And in general, just to be safe, both kinds of events should be actively ignored:

pictures :: Behavior t Picture
pictures = fmap render buttonTexts
        <* stepper undefined floats
        <* stepper undefined events

Or, better yet, let's hide this inside gloss-banana, so that nobody has to think about this again.