Monday, September 07, 2015

Two kinds of backtracking

I sometimes write my own parser combinators. I sometimes make mistakes while implementing my own parser combinators. In this post, I describe a mistake I made a few times: using the wrong kind of backtracking effect.

2015-08-11 update: it turns out everything in this post is already well-known in the litterature, see the Reddit discussion for links.

Two ways to order effects

So, like I said, I sometimes write my own parser combinators. It's not that hard: a parser can either succeed and consume some characters from a String, or it can fail, causing the computation to backtrack. Those two effects are already implemented separately by the State and Maybe monads, so we can create our custom Parser monad as a combination of the two, using monad transformers.

The one aspect of monad transformers about which I always need to think twice is the order in which I need to place the layers in order to get the side-effects to interact in the way I expect. With State and Maybe, depending on the order in which the layers are placed, we can either get a permanent state which survives backtracking:

import Control.Applicative
import Control.Monad
import Control.Monad.Trans.Class
import Control.Monad.Trans.Maybe
import Control.Monad.Trans.State

type PermanentState a = MaybeT (State String) a
runPermanent :: PermanentState a -> String -> (Maybe a, String)
runPermanent = runState . runMaybeT

-- |
-- >>> runPermanent writeThenBacktrack "initial state"
-- (Just "secret state!","secret state")
writeThenBacktrack :: PermanentState String
writeThenBacktrack = writeSecret <|> appendBang
    writeSecret :: PermanentState a
    writeSecret = do
        lift $ put "secret state"
        fail "backtracking"
    appendBang :: PermanentState String
    appendBang = do
        s <- lift get
        return $ s ++ "!"

Or we can get what we want for parsers, a path-specific state which gets reset along with the computation when we backtrack:

type Parser a = StateT String Maybe a

runParser :: Parser a -> String -> Maybe (a, String)
runParser = runStateT

-- |
-- >>> runParser writeThenBacktrack' "initial state"
-- Just ("initial state!","initial state")
writeThenBacktrack' :: Parser String
writeThenBacktrack' = writeSecret <|> appendBang
    writeSecret :: Parser a
    writeSecret = do
        put "secret state"
        fail "backtracking"
    appendBang :: Parser String
    appendBang = do
        s <- get
        return $ s ++ "!"

This way, if we start consuming characters and we discover that we need to backtrack, we start the next alternative from the state we were at the beginning as if the characters were never consumed.

char :: Char -> Parser ()
char expected = do
  (c:cs) <- get
  guard (c == expected)
  put cs

-- |
-- >>> runParser twoAlternatives "aab"
-- Just (1,"")
-- >>> runParser twoAlternatives "ab"
-- Just (2,"")
twoAlternatives :: Parser Int
twoAlternatives = (pure 1 <* char 'a' <* char 'a' <* char 'b')
              <|> (pure 2 <* char 'a' <* char 'b')
Two kinds of backtracking

The kind of backtracking we have seen so far consists of abandoning the current alternative and trying the next one. This behavior can be summarized by the following equation:

(f1 <|> f2) <*> x = if succeeds f1
                    then f1 <*> x
                    else f2 <*> x

I'll call that kind "if-then-else backtracking". There is another, more general kind of backtracking which Maybe does not support, which I'll call "distributive backtracking" after the following equation:

(f1 <|> f2) <*> x = (f1 <*> x)
                <|> (f2 <*> x)

The difference between the two behaviors is that if x fails in f1 <*> x, if-then-else backtracking will give up on the entire (f1 <|> f2) <*> x expression, whereas distributive backtracking will also try f2 <*> x before giving up. If the fact that x failed in f1 <*> x is sufficient to determine that it will also fail in f2 <*> x, then failing early is a good performance improvement. Otherwise, it makes the parser fail more often than it should.


For a concrete case in which this makes a difference, consider this alternate implementation of twoAlternatives:

-- |
-- >>> runParser twoAlternatives' "aab"
-- Just (1,"")
-- >>> runParser twoAlternatives' "ab"
-- Nothing
twoAlternatives' :: Parser Int
twoAlternatives' = optionalPrefix <* char 'a' <* char 'b'
    optionalPrefix :: Parser Int
    optionalPrefix = (pure 1 <* char 'a')
                 <|> (pure 2)

Instead of repeating the char 'a' <* char 'b' suffix twice, I have refactored the code so that only the optional 'a' prefix is included in the disjunction. By doing so, I have accidentally changed the meaning of the parser: instead of accepting "aab" and "ab", it now only accepts "aab". That's because by the time the parser encounters the mismatched 'b', it has already made its decision to use the extra 'a' in the prefix, so it's too late to go back and use an empty prefix instead.

In this simple contrieved example, it would be straightforward to reorganize the definition of twoAlternatives' to both avoid the repetition and retain the original meaning. In the more complicated real-world circumstances in which I encountered this limitation, however, refactoring was not a solution.

I was trying to debug a parser in the same way I debug some programs: by commenting out portions of it in order to isolate the problem to a smaller amount of code. Unfortunately, the different portions of the parser were tightly coupled: the commented-out portion was supposed to parse a few characters, the next portion was supposed to parse the next few characters, and commenting out the first parser caused the second parser to fail, as it was presented with the characters which were intended for the first parser. So after commenting out the first parser, I replaced it with a dummy parser which accepts any string of characters whatsoever.

Unfortunately, this dummy parser consumed the entire input, and then the second parser was again presented with the wrong part of the input, namely the end-of-file marker. I expected the dummy parser to backtrack and to try consuming slightly fewer characters, but it couldn't, because the parsing framework I was using was based on if-then-else backtracking. After the dummy parser consumed everything, no backtracking was allowed, just like what happened after we parsed the extra 'a' prefix above.

In order to make my dummy parser stop at the correct spot, I'd have to know what character the second parser was expecting to start at, so I could tell my dummy parser to accept everything but that character. Except that the first parser might have been supposed to parse some copies of that character as well, in which case that strategy would cause us to stop too early. So I'd have to reimplement much of the logic of the parser I was commenting out, which defeated the purpose of commenting it out. I was stuck.

Implementing distributive backtracking using the list monad

The easiest way to switch from if-then-else backtracking to distributive backtracking is to implement our backtracking using a list instead of a Maybe.

type Parser a = StateT String [] a

runParser :: Parser a -> String -> [(a, String)]
runParser = runStateT

With this simple change (I did not have to change any other definition nor type signature), twoAlternatives' now succeeds at parsing its input.

-- |
-- >>> runParser twoAlternatives' "aab"
-- [(1,"")]
-- >>> runParser twoAlternatives' "ab"
-- [(2,"")]
twoAlternatives' :: Parser Int
twoAlternatives' = optionalPrefix <* char 'a' <* char 'b'
    optionalPrefix :: Parser Int
    optionalPrefix = (pure 1 <* char 'a')
                 <|> (pure 2)

The reason it works is because optionalPrefix is no longer returning the first result which works, instead it returns a lazy list containing both results. This way, once the mismatched 'b' is encountered, there is enough information to go back and try another element from the list.

Implementing distributive backtracking in terms of if-then-else backtracking

If, like me, you're stuck with a parser based on if-then-else backtracking and you can't change the implementation, do not despair! As the title of this section indicates, it is possible to implement distributive backtracking on top of it.

Notice that the difference between the two kinds of backtracking is only apparent when a disjunction is followed by sequential composition, i.e., the case (f1 <|> f2) <*> x. If the parser was already written in the canonical form (f1 <*> x) <|> (f2 <*> x), where x can contain more disjunctions but f1 and f2 cannot, the kind of backtracking involved would make no difference. So, can we somehow put expressions into canonical form before executing our parser?

To turn (f1 <|> f2) <*> x into (f1 <*> x) <|> (f2 <*> x), we must apply the continuation (<*> x) to both sides of the (<|>). So I guessed that my wrapper's representation ought to receive a continuation, and the rest of the implementation followed naturally from following the types:

newtype DistributiveParser a = DistributiveParser
  { unDistributiveParser :: forall r. (a -> Parser r) -> Parser r
  } deriving Functor

runDistributiveParser :: DistributiveParser a
                      -> String -> Maybe (a, String)
runDistributiveParser p = runParser (unDistributiveParser p return)

instance Alternative DistributiveParser where
    empty = DistributiveParser $ \cc -> fail "backtracking"
    f1 <|> f2 = DistributiveParser $ \cc -> unDistributiveParser f1 cc
                                        <|> unDistributiveParser f2 cc

instance Applicative DistributiveParser where
    pure x = DistributiveParser $ \cc -> cc x
    df <*> dx = DistributiveParser $ \cc ->
                unDistributiveParser df $ \f ->
                unDistributiveParser dx $ \x ->
                cc (f x)

distributiveParser :: Parser a -> DistributiveParser a
distributiveParser px = DistributiveParser $ \cc -> do
    x <- px
    cc x

char' :: Char -> DistributiveParser ()
char' = distributiveParser . char

By reimplementing twoAlternatives' using our new wrapper, we obtain a version which succeeds at parsing its input, even though the underlying backtracking implementation is still if-then-else backtracking.

-- |
-- >>> runDistributiveParser twoAlternatives'' "aab"
-- Just (1,"")
-- >>> runDistributiveParser twoAlternatives'' "ab"
-- Just (2,"")
twoAlternatives'' :: DistributiveParser Int
twoAlternatives'' = optionalPrefix <* char' 'a' <* char' 'b'
    optionalPrefix :: DistributiveParser Int
    optionalPrefix = (pure 1 <* char' 'a')
                 <|> (pure 2)

I guess the conclusion is: make sure to use the appropriate implementation of backtracking if you can, and also when you can't :)

Thursday, June 18, 2015

Will it memoize?

In this post, I will try several variants of a simple memoizing Haskell program and test whether the program actually memoizes or not. This will give us a better grasp on sharing.
If you've been studying Haskell for any length of time, you have probably already stumbled upon the following unusual definition of the Fibonacci sequence.
fibs = 1 : 1 : zipWith (+) fibs (tail fibs)
If I print the fourth element of this list, how many additions will be evaluated? What if I then print the fifth element? Would you believe me if I told you that the answer depends on whether the NoMonomorphismRestriction extension is enabled or not? The answer also depends on various other details, which we will explore in this post.
In order to observe the additions as they are being evaluated, let's create a variant which prints a message to the console when it is called.
import Debug.Trace
noisyAdd x y = trace "adding" (x + y)

fibs = 1 : 1 : zipWith noisyAdd fibs (tail fibs)
fib n = fibs !! n
So, how many additions when I print the fourth element?
> fib 4
Three, because that's the number of entries in [2..4], and at each of those indices a single addition is performed to compute the next number out of the two previous numbers.

How many additions when I then print the fifth?
> fib 5
Only one! There are four entries in [2..5], but entries 2 through 4 have already been evaluated during our previous query. Implementing fib via a list of all possible results has effectively memoized our function.

Inside a where clause
The fact that fib is using a list for memoization purposes is an implementation detail. Let's hide the list inside the function's where clause.
fib n = fibs !! n
    fibs = 1 : 1 : zipWith noisyAdd fibs (tail fibs)
Will it memoize?
> fib 4
> fib 5
It did not! The definitions in the where clause are local to the body of the function, which itself only exists once the argument n has been given. For this reason, each time fib is called, a new copy of fibs is allocated and the previously-memoized values are forgotten.

Consider the following variant:
fib = \n -> fibs !! n
    fibs = 1 : 1 : zipWith noisyAdd fibs (tail fibs)
Will it memoize?
> fib 4
> fib 5
It did! This time, the where block does not have access to the n argument, so it does not need to be instantiated on every call. As a result, all the calls to fib are backed by the same list, and memoization succeeds.

Let's enable the NoMonomorphismRestriction extension.
{-# LANGUAGE NoMonomorphismRestriction #-}

fib = \n -> fibs !! n
    fibs = 1 : 1 : zipWith noisyAdd fibs (tail fibs)
Adding GHC extensions allows extra non-standard features, but our existing standards-conforming code should work the same as before, shouldn't it? In particular, it should still memoize, right?
> fib 4
*Main> fib 5
It did not! Enabling NoMonomorphismRestriction changed the type which GHC inferred for our definitions. With the extension turned on, GHC infers polymorphic types:
{-# LANGUAGE ScopedTypeVariables #-}

fib :: forall a. Num a => Int -> a
fib = \n -> fibs !! n
    fibs :: [a]
    fibs = 1 : 1 : zipWith noisyAdd fibs (tail fibs)
The Num a constraint is implemented via an implicit dictionary argument, which leads to the same non-memoizing behavior we had earlier when the n argument was in scope inside the where block. Here, Num a is clearly in scope as well, otherwise fibs would not be able to add its elements together.

Without NoMonomorphismRestriction, GHC infers monomorphic types:
fib :: Int -> Integer
fib = \n -> fibs !! n
    fibs :: [Integer]
    fibs = 1 : 1 : zipWith noisyAdd fibs (tail fibs)
This time the global Num Integer instance is used, not an abstract Num a which could change from call to call. This allows the same fibs to be used on each call, which in turn allows the memoized values to be retained from call to call.

Universal quantifiers

In the type signature fib :: forall a. Num a => Int -> a, there are three arguments of different kinds: the a is an implicit type argument, the Num a is an implicit dictionary argument, and the Int is an ordinary argument. We have seen that dictionary arguments and ordinary arguments both introduce a new scope and thereby hinder memoization. Is it also the case for type arguments?

To figure out the answer, let's construct a variant of fib which always adds integers and therefore doesn't need a dictionary argument, and also carries around a spurious polymorphic value on which no additions are performed. This way, we'll have a type argument but no dictionary argument.

fib :: forall a. Int -> a -> (Integer, a)
fib = pairWithFib
    pairWithFib :: Int -> a -> (Integer, a)
    pairWithFib n x = (fibs !! n, x)
    fibs :: [Integer]
    fibs = 1 : 1 : zipWith noisyAdd fibs (tail fibs)
Will it memoize?
> fib 4 "foo"
adding things
adding things
adding things
*Main> fib 5 [42.0]
adding things

It did! Types get erased, they do not exist at runtime. In particular, instantiating a to String and later to [Double] does not involve passing around some runtime representation of String or [Double], and it does not create a new copy of the where block.

It's a bit surprising, because this is a situation in which the evaluation semantics do not match up with the typing semantics. According to the type system, the pairWithFib in which a has been instantiated to String is not the same pairWithFib as the one in which a has been instantiated to [Double], as those two pairWithFib instances have different types and thus cannot be interchanged. Yet at runtime, those two instances of pairWithFib are represented by the same identical value. The trick is that in the absence of any type class constraint, pairWithFib has no way to distinguish between the different types it is supposed to be instantiated at, so it is allowed to behave the same in all cases. In particular, it is allowed to be the same identical value in all cases.


In the previous paragraph, I was careful to use the phrase "same identical value" as opposed to simply "the same value". By "identical", I mean that the two values have the same identity, which in turn means that they occupy the same space in memory.

In object-oriented languages, the concept of identity is very important. Suppose you hold references to two objects which happen to be equal to each other, in the sense that their corresponding fields are pairwise equal. Despite the fact that the objects are ostensibly equal, which of those two references you pass to a third party method matters because that third party might mutate one of the object's fields. If that happens, all the other references to this same identity, throughout your program, will also see the mutated field, while the references to other identities will not. And if you had passed the other reference, a different set of references, those which point to the other identity, will see their fields mutated. It's just normal pointer indirection, but it's something you always have to keep in mind in those languages, in order to avoid a family of problems known as aliasing issues.

In Haskell's immutable fragment, there are no aliasing issues, in the sense that calling a pure function on equal values will always yield equal results, regardless of the identity of those values. Nevertheless, the identity of those values does have its importance: identities do not impact correctness, but they do impact performance. Under some circumstances, excessive sharing can lead to poor performance, whereas in the case of memoization, sharing can increase performance by minimizing duplicated work.

The general rule explaining our results in all the previous sections is that memoization only happens if the data structure which holds the memoized values is shared between calls. To demonstrate this, our last example plays with sharing by specifying which copy of the fibs data structure is used to memoize which copy of the fib function.

mkFibs :: forall a. Num a => [a]
mkFibs = fibs
    fibs :: [a]
    fibs = 1 : 1 : zipWith noisyAdd fibs (tail fibs)

mkFib :: forall a. Num a => [a] -> Int -> a
mkFib = (!!)
Let's begin by constructing two copies of the fibs data structure:
fibsA :: [Integer]
fibsA = mkFibs

fibsB :: [Integer]
fibsB = mkFibs
And then two fib functions for each of the two copies of fibs:
fibA1 :: Int -> Integer
fibA1 = mkFib fibsA

fibA2 :: Int -> Integer
fibA2 = mkFib fibsA

fibB1 :: Int -> Integer
fibB1 = mkFib fibsB

fibB2 :: Int -> Integer
fibB2 = mkFib fibsB
"Will it memoize" is now the wrong question to ask. Each function memoizes its own results, but which functions share their memoized results with each other?
> fibA1 4
adding things
adding things
adding things
> fibA2 5
adding things
> fibB1 4
adding things
adding things
adding things
> fibB2 5
adding things

As expected, functions which were created from the same copy of fibs share their results with each other.

I hope that this last example makes it clear that sharing is something you can control. You can write most of your Haskell code without worrying about sharing, and then in the few places in which sharing affects the performance, you can explicitly thread your shared data structures to the places where you need them.

2015-06-20 update: as /u/pycube correctly points out, the above technique only works when you want to make sure that something is shared. Preventing sharing is much harder, because optimizations tend to increase sharing. With -O2, for example, all the examples in this post memoize.

Sunday, June 14, 2015

Querying type specializations

Obtaining the most general type of a Haskell expression is easy. But how do you figure out the more specialized types which your expression also has?


Let's draw a simple balloon using the diagrams library.

import Diagrams.Prelude
import Diagrams.Backend.Cairo.CmdLine

diagram :: Diagram B
diagram = circle 1
          vrule 1

I want to make the length of the string configurable.

{-# LANGUAGE FlexibleContexts, TypeFamilies #-}

balloon n = circle 1
        === vrule n

diagram :: Diagram B
diagram = balloon 2

That was easy, but I don't feel comfortable leaving balloon without a type signature. I'm a Haskell programmer, I need types in order to reason about my programs!

The most general type

With the proper flags, GHC warns about the fact that my top-level binding doesn't have a type signature and shows me which type it has inferred for it. I can also easily obtain this information via ghci:

> :type balloon
  :: (RealFloat (N a), Semigroup a, Transformable a, Juxtaposable a,
      TrailLike a, V a ~ V2)
  => N a -> a

Oh my, that's a large context! At least I can see why GHC wanted me to add FlexibleContexts (there is a constraint on N a, which isn't a type variable) and TypeFamilies (V a can evaluate to V2, which means V is probably a type-level function, also known as a type family).

I'd like to use a simpler type if possible. Maybe I can instantiate a to a concrete type?

Type defaulting

Since GHC 7.8, one easy way to figure out the concrete type at which an expression is instantiated is to pass it as an argument to a type-hole.

-- Found hole ‘_typeof’ with type: Integer -> Double
diagram :: Diagram B
diagram = balloon (_typeof 2)

The most general type of 2 is Num a => a, which can get specialized to Integer or Double or any of a large number of types having a Num instance. The _typeof type hole does not further constrain its argument's type, but the type defaulting rules cause a to be specialized to Integer. Then, balloon's complicated type does constrain its argument's type, and when combined with the requirement to produce a Diagram B, balloon's argument must apparently be a Double. At least, that's what the type-hole's inferred type Integer -> Double seems to be telling us.

Or could it be that balloon accepts a more general type than Double, but the defaulting rules simplify this type to Double before we have the chance to observe this more general type? For example, consider the following silly definition:

ignoreFractional :: Fractional a => a -> ()
ignoreFractional x = ()

If we use a type hole to query the type of ignoreFractional's argument, we get Double, even though the type of ignoreFractional is more general than that.

-- Found hole ‘_typeof’ with type: Integer -> Double
main :: IO ()
main = print $ ignoreFractional (_typeof 42)

Let's disable type defaulting, so that it stops skewing our results.

default ()

Note that the syntax for default is default (type1, type2, ...), not default type, type2, ..., so the above is disabling type defaulting, not configuring the unit type to be the new default instead of Integer.

Without type defaulting, our type hole is no longer concluding that ignoreFractional's argument must be a Double. It also complains that some type variables are ambiguous, which is fine for now.

-- Found hole ‘_typeof’ with type: a1 -> a0
-- Where: ‘a0’ is an ambiguous type variable
--        ‘a1’ is an ambiguous type variable
main :: IO ()
main = print $ ignoreFractional (_typeof 42)

More importantly, our type hole still says that balloon's argument must be a Double, so type defaulting did not skew our earlier results after all.

-- Found hole ‘_typeof’ with type: a0 -> Double
-- Where: ‘a0’ is an ambiguous type variable
diagram :: Diagram B
diagram = balloon (_typeof 2)
Evaluating type-level functions

Looking at the most general type of balloon more closely, I think I can figure out how Double was chosen. Ignoring the constraints, the type of balloon is N a -> a. We're imposing a ~ Diagram B, and we've already seen that diagrams likes to use type-level functions. Perhaps N is a type-level function which returns Double when given the input Diagram B?

> :kind! N (Diagram B)
N (Diagram B) :: *
= Double

Indeed it is. Note the exclamation mark in the :kind! command: that's how I am telling ghci that I want to see the result of the type-level function application, not just the kind of this result.

> :help
:kind[!] <type>             show the kind of <type>
                            (!: also print the normalised type)
The fully-specialized type

We now know that instantiating a ~ Diagram B specializes N a -> a to Double -> Diagrams B, and that this choice for a satisfies all the constraints. I can finally give a short type for balloon:

balloon :: Double -> Diagram B
balloon n = circle 1
        === vrule n

I could have obtained this answer more easily by using the type hole to query the type of balloon directly.

-- Found hole ‘_typeof’
--   with type: (Double -> Diagram B) -> a0 -> Diagram B
-- Where: ‘a0’ is an ambiguous type variable
diagram :: Diagram B
diagram = (_typeof balloon) 2
Intermediate types

So far, we have seen two extremes: the most general, most abstract type of an expression, and its fully-specialized, most concrete type. There are other types in between those two extremes, obtained by fixing some parts of the type signature but not others.

For example, I now know what the type of balloon specializes to when I force the return type to be the fully-specialized type Diagram B. In diagrams, the B identifies the backend I have imported at the top of the file. Which part of the specialization is due to the fact that the result is forced to be a Diagram, and which part is due to the fact that I am using the Cairo backend?

An answer to this question would be a type signature of the following form:

balloon :: _constraint => _input -> Diagram _backend

In which _constraint, _input and _backend would be instantiated so that the resulting type signature would be the most general type which is both a valid type signature for balloon's definition and matches the above form. For example, we know from our previous experiments that _constraint ~ (), _input ~ Double and _backend ~ B would be valid instantiations. Is there a solution which involves more type variables and fewer concrete datatypes?

Proxies and identities

Let's ignore the constraints for now. The problem is now much simpler: we have the most general type N a -> a, we have a shape input -> Diagram backend, and we want to unify those two types. Type unification is GHC's bread and butter, we just need to construct a program whose types will require GHC to unify those two types as part of its ordinary type checking phase.

For example, consider the following restricted identity function:

myId :: (input -> Diagram backend)
     -> (input -> Diagram backend)
myId = id

If we apply myId to balloon, GHC will have to find an instantiation for input and backend or otherwise complain that the call doesn't typecheck.

In order to ask GHC which instantiations it has chosen, we can add an extra parameter whose only purpose is to give us a place to put a type hole.

import Data.Proxy

typeof :: Proxy (input -> Diagram backend)
       -> (input -> Diagram backend)
       -> (input -> Diagram backend)
typeof Proxy = id

-- Found hole ‘_proxy’ with type:
--   Proxy (N backend -> Diagram backend)
query = typeof _proxy balloon

So there you go, a type signature of the form _input -> Diagram _backend involving type variables instead of concrete types:

balloon :: _constraint => N backend -> Diagram backend

We still don't know what those constraints should be, and I don't know how the technique could be generalized to obtain it.

Interestingly, the argument type N a got specialized to N backend, the same type-level function but applied to a different type variable. This makes me think that when N is applied to Diagram backend, the Diagram part is probably stripped off and the result is obtained via the recursive call N backend.

> :set -XRankNTypes
> :kind! forall backend. N (Diagram backend)
forall backend. N (Diagram backend) :: *
= N backend

Indeed it is.

Partial type signatures

With the new support for partial type signatures in GHC 7.10, there is now an easier way for us to discover what _constraint, _input and _backend should be instantiated at. I cannot give the name _constraint to the extra constraint wildcard, but as long as the other wildcards can be named, it's still easy to distinguish which is which.

{-# LANGUAGE NamedWildCards #-}

-- Found hole ‘_’ with inferred constraints:
--   (RealFloat (N w_backend),
--    TrailLike (QDiagram w_backend (V w_backend) (N w_backend) Any),
--    Metric (V w_backend),
--    V w_backend ~ V2)
-- Found hole ‘_input’ with type: N w_backend
-- Found hole ‘_backend’ with type: w_backend
balloon :: _ => _input -> Diagram _backend

I'm guessing that QDiagram is probably related to Diagram in some way. Is Diagram a type synonym for a more complicated QDiagram type?

> :info Diagram
type Diagram b = QDiagram b (V b) (N b) Any


Analyzing the contribution of the backend

Substituting what GHC found for each hole, alpha-renaming, and unexpanding the QDiagram expression back into its Diagram type synonym, I can now give balloon the following type signature.

balloon :: ( RealFloat (N b)
           , Metric (V b)
           , TrailLike (Diagram b)
           , V b ~ V2
        => N b -> Diagram b

That's still quite a mouthful, but compare with the most general type signature we had inferred for balloon earlier:

balloon :: ( RealFloat (N a)
           , Juxtaposable a
           , Semigroup a
           , TrailLike a
           , Transformable a
           , V a ~ V2
        => N a -> a

We can see that specializing a to Diagram b has had quite an impact on the constraint. The Juxtaposable constraint has been removed, presumably because there is an instance Juxtaposable (Diagram b) somewhere. The same goes for Semigroup and Transformable. The TrailLike constraint remains, presumably because the instances for that involve a concrete backend, something like instance TrailLike (Diagram B). The RealFloat and ~ V2 constraints remain as well, but apply to a different type variable, because N (Diagram b) and V (Diagram b) reduce to N b and V b. Finally, the Metric constraint was added, presumably because one of the instances has it as a context, something like instance Metric b => Juxtaposable (Diagram b).

We now have a better idea of which constraints are satisfied by the fact that a is a Diagram, and which parts of the constraint depend on the particular choice of backend. More importantly, we have learned about many techniques for querying the various types of an expression, which is very useful when you are relying on types as much as I am to understand an existing Haskell codebase.

Saturday, May 02, 2015

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

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

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.

Wednesday, January 28, 2015

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)


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)


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)



...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))"]


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))"]


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


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

  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')))"]


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_1 <$> 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_1(y',z')","F_1(x',y')","F_1(y,z)","F_1(x,y)"]
Computing ["E(F_1(x',y'),F_1(y',z'))","E(F_1(x,y),F_1(y,z))"]
Computing ["E(E(F_1(x,y),F_1(y,z)),E(F_1(x',y'),F_1(y',z')))"]



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!

Sunday, December 21, 2014

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:

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

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) {

template<typename A>
void println(A value) {

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

struct PrintTree<
> > > > > > > >
  static void call(int, Pair<
                        > > > > > > >
  ) {
    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) {
    } 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);

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?

Monday, December 08, 2014

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.


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.


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.


Use ldd to list the .so files on which your executable depends, and copy all of them except 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.