Testing HsColour. Here you go: fibonacci with iso-recursive types

> data Mu f = Mu {unMu :: f (Mu f)}
> type List a = Mu ((,) a)
> tl = snd . unMu
> hd = fst . unMu
> cns = (Mu .) . (,)
> ones = Mu (1,ones)
> fibs :: List Integer
> fibs = cns 1 . cns 1 $ go fibs (tl fibs)
>        where go (Mu (x,xs)) (Mu (y,ys)) = cns (x+y) $ go xs ys

(NB. planet readers, you can't see the colours)

Prelude

I attended a compilers course this spring. The final excercise was to implement from scratch a compiler for what was basically a very restricted subset of C. The compiler was to generate LLVM assembly that could then be optimized and compiled into native binaries with the (very high quality) LLVM tools. I recommend having a look at the various LLVM benchmarks: it's going to be a major player in programming language implementation in the future.

All this however is but a backdrop to what I'm going to write about. I implemented the compiler in Haskell and bumped into very interesting design questions. First of all, I decided to implement the AST (abstract syntax tree, generated by the parser) as a generalized algebraic datatype (GADT) because I had been itching to find some real use for GADTs and ASTs were the canonical example of their use. The following is a condensed version of what the finished compiler uses (preceded by some boilerplate to make this post work as literate haskell):

> {-# LANGUAGE KindSignatures, EmptyDataDecls, MultiParamTypeClasses,
>              FlexibleInstances, GADTs #-}
>
> import Control.Monad
> import Control.Monad.Fix
> import Control.Monad.Error
>
> data Expr
> data Stmt
> data Location
>
> data NoAnn a = NoAnn
> type Identifier = String
> type Op = String
>
> data AST (ann :: * -> *) t where
>     If      :: ann Stmt -> AST ann Expr -> AST ann Stmt -> AST ann Stmt
>     Block   :: ann Stmt -> [AST ann Stmt] -> AST ann Stmt
>     Assign  :: ann Stmt -> AST ann Location -> AST ann Expr -> AST ann Stmt
>
>     Var     :: ann Location -> Identifier -> AST ann Location
>     Ref     :: ann Expr -> AST ann Location -> AST ann Expr
>
>     Binary  :: ann Expr -> Op -> AST ann Expr -> AST ann Expr -> AST ann Expr
>     NumLit  :: ann Expr -> Integer -> AST ann Expr

In addition to this there were declarations, array types and more control structures, but I'm trying to keep things simple. As you can see the GADT is parametrised over an annotation type ann and a phantom type that indicates the type of the node (statement, expression, location). The annotation type, however, is of kind *->*: it takes the node type as an argument. This is useful because different node types need to have different annotations, for example expressions have a type while statements do not. All this could also be formulated as vanilla Haskell types as follows (with a simple annotation type for simplicity):

> data Stmt' ann = If' ann (Expr' ann) (Stmt' ann)
>                | Block' ann [Stmt' ann]
>                | Assign' ann (Location' ann) (Expr' ann)
>
> data Location' ann = Var' ann Identifier
>
> data Expr' ann = Binary' ann Op (Expr' ann) (Expr' ann)
>                | Ref' ann (Location' ann)
>                | NumLit' ann Integer

However getting the different annotation types to flow as smoothly would be a bit bothersome. (The primes are added in order to keep this blog post a working .lhs file.)

Attribute grammars and first solution

I had decided to implement the compiler with attribute grammars, a very elegant and powerful formalism for tree traversals (see Why attribute grammars matter for an introduction). There exist attribute grammar systems that generate Haskell code from a description of the grammar (UUAG being the most noteworthy), but I decided to go on with a hand-coded approach. UUAG compiles the attribute grammar into a bunch of haskell functions that mutually recurse to calculate the attributes. This however mixes up all the attributes into one traversal and is very obfuscated. A more straightforward way would be to actually annotate the tree with attribute fields.

More specifically, syntetic attributes (ones which can be computed from a node's childs' attributes) would be stored in the node's annotation field while inherited attributes (ones which propagate from a node down to it's leaves) would be just passed down as arguments to the traversal function. The basic structure of the traversal would be something like

> class Traverse1 a inherited synthetic where
>     traverse1 :: AST NoAnn a -> inherited -> AST synthetic a
> -- and instances for Stmt, Expr and Location

This solution however has the problem that makes the traversal monolithic. I'd like to have the different phases of the compiler (e.g typecheck, code generation) define their own simple traversals and then simply compose these in the driver. One other solution I toyed with was:

> type M = Either String   -- for example, actually it was RWST on top of Error
>
> -- an action that we can mfix over (as long as M is an instance of MonadFix)
> type Result a = a -> M a 
>
> data AG a = AG { 
>       block   :: M [a Stmt]                     -> Result (a Stmt),
>       ifthen  :: M (a Expr) -> M (a Stmt)       -> Result (a Stmt),
>       assign  :: M (a Location) -> M (a Expr)   -> Result (a Stmt),
>       
>       var     :: Identifier                     -> Result (a Location),
> 
>       ref     :: M (a Location)                 -> Result (a Expr),
>       binary  :: Op -> M (a Expr) -> M (a Expr) -> Result (a Expr)
> }
>
> compose :: AG a -> AG a -> AG a
> compose (AG b' i' a' v' r' bin')
>         (AG b  i  a  v  r  bin ) =
>     AG (f1 b' b) (f2 i' i) (f2 a' a) (f1 v' v) (f1 r' r) (f3 bin' bin)
>     where f1 m n = \x -> m x >=> n x
>           f2 m n = \x y -> m x y >=> n x y
>           f3 m n = \x y z -> m x y z >=> n x y z
> 
> class TraverseFix attr t where
>     traverseFix :: AG attr -> AST NoAnn t -> M (attr t)
>
> -- All we do in these instances is define the recursion scheme
> instance TraverseFix attr Stmt where
>     traverseFix ag (Block _ ss)   = mfix $ (block ag) (mapM (traverseFix ag) ss)
>     traverseFix ag (If _ e s)     = mfix $
>         (ifthen  ag) (traverseFix ag e) (traverseFix ag s)
>     traverseFix ag (Assign _ l e) = mfix $
>         (assign  ag) (traverseFix ag l) (traverseFix ag e)
> instance TraverseFix attr Location where
>     traverseFix ag (Var _ i) = mfix $ (var ag) i
> instance TraverseFix attr Expr where
>     traverseFix ag (Ref _ l)          = mfix $ (ref ag) (traverseFix ag l)
>     traverseFix ag (Binary _ o e1 e2) = mfix $
>         (binary ag) o (traverseFix ag e1) (traverseFix ag e2)

This lets one compose multiple attribute grammars (AGs) and take their fixpoint over the AST: this makes the order of composition irrelevant and actually allows for more expressive AGs. Also, it evades actually storing the intermediate attributes in the tree quite elegantly. All this is very true to the spirit of attribute grammars but the requirement of knowing all attributes beforehand violates the modularity I needed.

Stand by for part 2...

A handy (and quite well-known) trick in haskell is to turn list concatenation (a O(n) operation) into function composition that avoids copying and is O(1):

> let list1 = [1,2,3] in list1 ++ list1
> let list2 = (1:).(2:).(3:) in list2 . list2 $ []  -- ta-dah! no copying

I benchmarked this ages ago when I first heard about the trick, but morrow publishing a a library that uses this made me rerun and publish my observations. Here's the test code, the classical quicksort:

> module Main
>     where
>     
> import Random
> import Control.Monad
> import Data.List
> 
> qsort1 :: [Int] -> [Int]
> qsort1 [] = []
> qsort1 (x:xs) = qsort1 [a | a<-xs, a<x] ++ [x] ++ qsort1 [a | a<-xs, a>=x]
> 
> qsort2 :: [Int] -> [Int]
> qsort2 xs = qsort xs []
>     where qsort [] = id
>           qsort (x:xs) = qsort [a | a<-xs, a<x] . (x:) . qsort [a | a<-xs, a>=x]
>           
> main = do
>   l <- replicateM 500000 $ randomRIO (1,500000)
>   let l1 = qsort1 l
>   let l2 = qsort2 l
>   print (and $ zipWith (==) l1 l2)

Results with ghc -O0:

% for i in 1 2 3; do time ./qsort +RTS -P -K12000000; done
True
./qsort +RTS -P -K12000000  13.09s user 0.28s system 99% cpu 13.420 total
True
./qsort +RTS -P -K12000000  12.81s user 0.28s system 99% cpu 13.135 total
True
./qsort +RTS -P -K12000000  13.38s user 0.31s system 99% cpu 13.709 total

COST CENTRE                    MODULE               %time %alloc  ticks     bytes
qsort1                         Main                  35.4   46.2    109 143631183
qsort2                         Main                  32.5   34.3    100 106768654
main                           Main                  26.9   17.2     83  53500026
CAF                            Main                   5.2    2.3     16   7001237

and with ghc -O3:

% for i in 1 2 3; do time ./qsort +RTS -P -K12000000; done
True
./qsort +RTS -P -K12000000  9.40s user 0.30s system 99% cpu 9.720 total
True
./qsort +RTS -P -K12000000  10.58s user 0.40s system 99% cpu 11.021 total
True
./qsort +RTS -P -K12000000  10.10s user 0.36s system 99% cpu 10.501 total

COST CENTRE                    MODULE               %time %alloc  ticks     bytes
qsort1                         Main                  35.1   46.8     74 127559904
main                           Main                  33.6   19.1     71  52001182
qsort2                         Main                  31.3   34.1     66  93115220

So it seems the compositive version is a tad faster and notably less memory-hungry. Also, ghc optimizes the compositive version more efficiently, presumably because (.) enables all sorts of rewrites (++) doesn't.

As a sidenote, strangely enough replacing the list comprehensions in the above code with something like

> let (small,big) = partition (<x) xs in qsort small ++ [x] ++ qsort big

ended up in a performance decrease of some 3s with -O3 (didn't test w/o optimizations)...

Update: As folks on #haskell pointed out I should mention that this isn't a real quicksort. Quicksort refers to the exact in-place partitioning algorithm that the imperative version uses. This is of course immaterial to the benchmark.

Update 15:01: quicksilver noted that the profiling overheads for the two implementations might be different. I ran a quick test that showed the overheads to be roughly equal: unoptimized qsort2 was about 3% faster than unoptimized qsort1 both with and without profiling.

Today's small haskell satori: the least fixpoint operator

> fix f = let x = f x in x

(which seemed like dark magic when I first saw it) could be written a bit more intuitively as

> fix' f = let f' = f . f' in f' undefined

This captures the intuition that fix just applies a function iteratively to undefined (i.e. bottom, _|_). Actually we could use any value in the place of undefined but that would restrict the type of fix'. You see, the only reason f' really needs to be applied to anything is to appease the typechecker.

Of course the original (Haskell98) definition is more elegant and probably has better sharing characteristics too.

Update 2008-07-11: found some related musings on haskell-cafe. See also the reply

Sorry, somehow managed to forget about writing part 2 for multiple weeks

Okay, I'll pick up where part one ended. I've added booleans and declarations in order to make type checking non-trivial ;)

> {-# LANGUAGE KindSignatures, EmptyDataDecls, MultiParamTypeClasses,
>              FlexibleInstances, GADTs #-}
>
> import Control.Monad
> import Control.Monad.Error
> import Control.Monad.RWS
> import Control.Monad.Reader
>
> data Expr
> data Stmt
> data Location
> data Decl
>
> type Identifier = String
> type Op = String
> type Symbol = String
> data Type = BoolType | IntegerType
>
> -- the empty annotation
> data NoAnn a = NoAnn
>
>
> data AST (ann :: * -> *) t where
>     If      :: ann Stmt -> AST ann Expr -> AST ann Stmt -> AST ann Stmt
>     -- note the added declaration list
>     Block   :: ann Stmt -> [AST ann Decl] -> [AST ann Stmt] -> AST ann Stmt
>     Assign  :: ann Stmt -> AST ann Location -> AST ann Expr -> AST ann Stmt
>
>     Var     :: ann Location -> Identifier -> AST ann Location
>     Ref     :: ann Expr -> AST ann Location -> AST ann Expr
>
>     Binary  :: ann Expr -> Op -> AST ann Expr -> AST ann Expr -> AST ann Expr
>     NumLit  :: ann Expr -> Integer -> AST ann Expr
>
>     -- these are new
>     BoolLit :: ann Expr -> Bool -> AST ann Expr
>     Decl    :: Identifier -> Type -> AST ann Decl

Descending from the Tower o' Ivory

I decided to partly break the attribute grammar abstraction by performing different phases inside different suitable monads. This increased coding pleasure and clarity in comparison to the generalized versions presented in the previous post.

> type M = Either String    -- aka Error, used for inter-phase communication
> type TypeM = ReaderT TEnv (Either String)   -- typecheck monad
> type CodeM = RWST SEnv () SState (Either String) -- codegen monad

The Reader monad is used for passing down symbol tables, and, in the case of code generation, the label of the current loop for use in breaking. These are the inherited attributes of the respective attribute grammars.

> data SEnv = SEnv { symbols :: [Symbol], loopend :: Maybe String}
> data TEnv = TEnv { decls :: [AST NoAnn Decl]}

Additionally code generation needs to keep counters for disambiguating variables and scopes (labels). The State monad corresponds to a top-down left-to-right flowing attribute.

> data SState = SState { var :: Integer, scope :: Integer }

Synthetic attributes are embedded in the form of the recursive traversal, no fancy tricks are needed to represent them.

As another step down the abstraction ladder I differentiated the type signatures of different phases to enforce and clarify the flow of information between the phases.

Typechecking generates an annotated AST from an unannotated one:

> data Attr a where
>     EAttr {etyp :: AST Attr Type} :: Attr Expr
>     LAttr {ltyp :: AST Attr Type} :: Attr Location
>     Empty :: Attr a
>
> class Typecheck a where
>    typecheck :: AST NoAnn a -> TypeM (AST Attr a)
>
> do_typecheck :: AST NoAnn Stmt -> M (AST Attr Stmt)
> do_typecheck ast = runReaderT (typecheck ast) (TEnv [])

Code generation takes an annotated AST and transforms it into code:

> data Code a where 
>     -- code is the body, out is the register the result is in
>     ECode {code :: String, out :: String} :: Code Expr
>     -- code fetches the reference, which is then available in ptr
>     LCode {lcode :: String, ptr :: String} :: Code Location
>     -- statement code is just a body
>     SCode :: String -> Code Stmt
>
> class Codegen a where
>    codegen :: AST Attr a -> CodeM (Code a)
>
> do_codegen :: AST Attr Stmt -> Either String String
> do_codegen ast = do 
>   (SCode code,_) <- evalRWST (codegen ast) (SEnv [] Nothing) (SState 0 0)
>   return code

Now our glorious two phase compiler (still missing the instances ;) could be written as \s -> parser s >>= do_typecheck >>= do_codegen. The do_ functions are restricted to statements on purpose: we know that the root node of the AST will be a statement.

Notice how the Code and Attr types are parametrized with the same phantom types as nodes in the AST. This is what we had in mind when designing the GADT.

Now we have managed to present different phases modularily while not straying too much from the original attribute grammar approach.

Okay, this has been sitting in my draft directory for long enough, better "realease early, release often"

Coming next: the implementation.

Update 23:35

Update 2008-08-25: The do_ functions

Prequel: lazy evaluation

The book The Implementation of Functional Programming Languages discusses at length the graph reduction implementation of a non-strict functional language (see esp. chapters 10-12). This technique is what is usually called lazy evaluation.

The point about lazy evaluation is that each function argument is evaluated at most once (when it is first needed). This also applies to names bound with lets as lets are (in the book) transformed into function applications.

The picture is a bit more complicated for GHC, but in essence: lazy evaluation guarantees that a monomorphic (non-polymorphic) expression with a name is evaluated only once.

The beef: fix

Now I'll continue where I left off in a previous posting about fix. We are dissecting the standard definition of fix:

> fix f = let x = f x in x

I previously explored one alternative definition, and now I'll use another as a springboard. So: why is fix not defined as

> myfix f = f (myfix f)

which is obviously equivalent to the previous one? The oft-heard answer is that the former definition has "better sharing characteristics".

Let's have a look at an infinite list of ones.

> ones = 1:ones :: [Integer]
> ones_myfix = myfix (1:) :: [Integer]
> ones_fix = fix (1:) :: [Integer] 

The typesigs are here to keep us monomorphic.

First up, ones. The name ones gets bound to a cons-cell (constructed by (:)), that has 1 as its head and ones as its tail. Only one cons-cell is ever allocated. Now let's have a look at what ones_myfix does.

ones_myfix ==> myfix (1:) ==> 1:myfix (1:) ==> 1:1:myfix (1:) ==> ...

This equivalent to ones_myfix = 1:ones_myfix, but only up to naming, and naming is crucial when dealing with lazy evaluation. The call myfix (1:) is not memoised so it is re-evaluated when we progress through the list, and each call allocates a new cons cell. The solution is to add an intermediate name, which is exactly what (the real) fix does:

ones_fix ==> fix (1:) ==> let x = 1:x in x

Which creates one cons cell exactly like ones, except the cell is called x. This is why the standard definition of fix has those "better sharing characteristics".

Afterword

The Implementation of Functional Programming Languages takes an approach where fix (AKA the Y combinator) is taken as a built-in and recursive lets are implemented with it. In GHC, recursive lets are elementary and thus fix can be defined without any special tricks.

The book actually mentions that there are two distinct ways for implementing the built-in Y: either cyclically (by sharing) or non-cyclically (re-evaluating at each step). This is exactly the same design decision we encounter with haskell's fix.

Updated 01:40

The CS Dept. at Helsinki University mostly does machine learning, data analysis and bioinformatics nowadays with some oldschool algorithmics for the fogies. There has been a demand for hard theory (complexity theory, type theory, adv theory of computation) among the students and we've finally gotten the wheels rolling.

This fall a bunch of us got together and held a course (site in Finnish, includes lecture material and excercises) on lambda calculus here at Helsinki University. Over 120 people participated and about 80 held with us to the end. The course focused on practical aspects of λ-calculus instead of grinding through parametricity and other mathematical properties.

This spring the same group is lecturing Introduction to Functional Programming, a course whose teacher left our university a few years ago. Again we have over 120 participants. Lectures are held in the second largest auditorium here in Exactum and we're enjoying full support of the administration. The course is about the basics of functional programming as a software design paradigm with Haskell as main language.

What's fabulous is that both of these courses were in the top three in participant numbers for respectively the fall and spring semesters. Also, the department (of CS) has arranged a possibility for undergraduates to hold free-form workshops for extra credit. We have a bunch of people interested in going through post-TaPL type theory and another group that wants to do cool practical Haskell.

I've heard that the department is overjoyed by the activity students are exhibiting but is afraid that we'll want thesis advisors and postgraduate positions from these hot fields nobody is researching here. Let's see what happens in a few years ;)

Trying to overcome my writer's block by jotting down some random thoughts.

1

My life is a cyberpunk novel. I rise tired after minimal sleep, slam stimulants into my system and run through a DDR-esque concrete ghetto to the tram stop. I only wake up properly at work where I juggle abstractions and try to teach robot hands to pick up cubes in a virtual reality.

2

The Haskell project course is chugging along nicely. People are encountering frustrating and sometimes even interesting real-world problems like FFI, installing libraries and handling exceptions in pure code. I plan to blog on the exception issue soon.

Also, we've been thinking about the future teaching of functional programming at Univ Helsinki. There's a course on formal type theory (with Coq!) coming up this fall.

3

At work we've moved to Roundup, a pretty pleasant issue tracker that is easy to customize. The default templates could be a bit cleaner tho. (E.g., there's support for storing different queries in the db but the menu uses hard-coded GET parameters).

I've been working on compiling our stream computation DSL to jvm bytecode that just loops over a bunch of arrays. It's been sweet so far.

5

Foundations for Programming Languages is a great book. Tackles some type theory but mainly other cool stuff such as algebras (as featured in algebraic datatypes), different models of lambda calculus and logical relations. A good complement for TaPL.

7

Have travelling to do this summer:

• The IMC competition in Bulgaria
• A trip to Austria, including hiking in Hohe Tauern national park and some Vienna
• Cottage and boating trips with parents & grandparents

Random links

for your browsing pleasure

• http://multigrainknackebrod.blogspot.com/ -- a somewhat interesting blog
• http://kdice.com -- nice simple risk-like game
• http://www.lawfulpath.com/ref/sw4qw/index.shtml -- a conspiracy theory
• http://jpatokal.iki.fi/music/mp3/gnosis_at_inkvisitio3.mp3 -- some nice gabber

Parallel or

Every (imperative) programmer knows the usefulness of a shortcircuiting or operation, that is, a binary operation that doesn't evaluate it's second argument if the first one is True. To a functional programmer this is only natural: the function or is lazy in it's second argument.

> or True  _ = True
> or False x = x

Wouldn't it be nice to have a parallel or that evaluates to True if either of it's arguments is True. That is, a function por satisfying

> por :: Bool -> Bool -> Bool
> por True  _    === True
> por _     True === True

even if _ were undefined or a non-halting computation. As it turns out, a function like this cannot be implemented in lambda calculus. Let's prove this.

We will restrict our selves to simply-typed lambda calculus with three constants, True, False :: Bool and if :: Bool -> a -> a obeying the following reduction rules:

> if True  M N ==> M
> if False M N ==> N

Recall that the basic reduction rule of lambda calculus was beta-reduction, that is, function application.

We will additionally allow for fixpoints, as otherwise we wil not be able to define most functions at all. (Strictly speaking, we will need one fixpoint operator per type, but type annotations will be ommitted in the future for brevity.) The definition of fix (if you don't understand it, just take for granted that fix let's us do recursion or see these posts):

> fix_a :: (a -> a) -> a
> fix_a ==> \f -> f (fix f)

Our evaluation order will be normal order, that is: we apply beta-reduction (function application) and our custom reduction rules at the lefternmost possible part of the expression. (This evaluation scheme is confluent, i.e. it always produces a unique normal form if such exists)

Now, because of it's type, por must have form

> por = \x -> \y -> E

for some E. Let us assume that E is in normal form (if it is not, it can be reduced without changing the semantics of por). We will also assume that both x and y appear in E as this is only natural.

Now then, buried in E there must be some reduction opportunities that can only be taken when something is substituted for x and y. Because x and y are variables, they must be distinct parts of E. That is, when we substitute something for x and y, these somethings will not overlap. By symmetry we can assume that x is left of y in E. Let E[A,B] denote E with A replaced for y and B for x. Now then if A reduces to A' in one step, E[A,B] reduces to E[A',B] in one step because A was our lefternmost reduction opportunity.

Now we note that fix (\x -> x) reduces to itself in two steps:

> fix (\x -> x) ==> (\f -> f (fix f)) (\x -> x) ==> (\x -> x) (fix (\x -> x))
>   ==> fix (\x -> x)

And thus

> por (fix (\x -> x)) B === E[fix (\x -> x),B]

can have no normal form regardless of B. Especially por (fix (\x -> x)) True =/= False.

A taste of domain theory

Scott models, also known as domains, are a way of obtaining denotational semantics for lambda calculi. Denotational semantics mean a mapping of the structures of the language to mathematical objects (functions, sets) of some sort.

Long story short, we consider a more-defined-than ordering of values. For simple types such as Bool and Nat (the natural numbers), there are just two levels to this ordering: the completely undefined value _|_ (pronounced "bottom"), and the defined values (1,2,True,...). The intuistic reason for using these orders is that a (computable) function must map a more-defined argument to a more-defined result. That is, functions must be monotonic wrt. the orderings of it's argument and result types.

An example is in place. Consider a function f :: Nat -> Bool with

> f undefined === True

now clearly f 4 must be True as well because f couldn't have inspected it's argument. Similarily, if

> f 4 === undefined

f undefined must be undefined also.

To be exact, for simple types (here Bool and Nat) the ordering is defined by

1. _|_ <= x for all x
2. x and y are not comparable if neither is _|_

The monotonicity requirement can now be formulated as: if a <= x then f a <= f x.

The cliff hanger

If we expand the definition of monotonicity to two arguments in the most natural way, that is

> a <= x && b <= y ==> f a b <= f x y

we find out that partial or is monotonic: this can be easily ascertained by either checking all cases or reasoning that making either argument to por less defined will never make the result more defined. So, por cannot be told apart from the defineable functions in our semantic model.

In the next post we will investigate what happens when we introduce por as a constant into our lambda calculus. Be warned, it might take a while as there's a lot to handle and I'm leaving for the alps after the weekend.

Preliminaries:

> module Data.Function.Stack where
> import Data.Function
> import Control.Monad
> import Control.Monad.Instances

Let's pretend that Haskell functions receive their arguments neatly on a stack. Now suppose our arguments were given in the wrong order and we needed to shuffle them around a bit before actually making the function call. In the Haskell world this is equivalent to applying some sort of permuting combinator to the function. Here are some basic stack operations implemented as combinators:

Swap the first two arguments:

> swap :: (a -> b -> rest) -> (b -> a -> rest)
> swap = flip

Duplicate the first argument:

> dup :: (a -> a -> rest) -> (a -> rest)
> dup = join  -- in the (r->) monad, sorry

Apply a literal argument:

> push :: a -> (a -> rest) -> rest
> push = flip id

Discard an argument:

> pop :: rest -> (a -> rest)
> pop = const

The type signatures can be interpreted as stack effects (which are used in stack-based languages to describe the stack effects of functions, or words as they are called) simply by reading them backwards. The top of a stack is to the left (a -> b -> rest is a stack with a on top) and the signature x -> y means that the stack state y is turned into state x.

First example:

(\a -> f 3 a a) = dup . push 3 $ f

As you can see, the stack combinators are written left-to-right in execution order. Nice.

Some additional combinators:

> dup2 :: (a -> b -> a -> rest) -> (a -> b -> rest)
> dup2 f a b = f a b a

> dup3 :: (a -> b -> c -> a -> rest) -> (a -> b -> c -> rest)
> dup3 f a b c = f a b c a

> rot :: (b -> c -> a -> rest) -> (a -> b -> c -> rest)
> rot = dup3 . pop

> rot' :: (c -> a -> b -> rest) -> (a -> b -> c -> rest)
> rot' = rot . rot

And a second example:

(\a b c -> f b c a 3) = (push 3) . dup3 . pop . rot $ f

Shuffling arguments with just these combinators can be very laboursome. To facilitate deep transformations we introduce the meta-combinator deep:

> deep :: (x -> y) -> ((c -> x) -> (c -> y))
> deep = (.)

Which takes a stack combinator and applies it one level down:

deep (push True) :: (c -> Bool -> rest) -> c -> rest

Now we can rewrite example 2 as:

(\a b c -> f b c a 3) = rot . (deep . deep . deep $ push 3) $ f

We can also describe complicated function compositions in this language of ours by mapping Haskell functions into "words" that manipulate our ephemeral stack:

> apply :: (a -> b) -> (b -> rest) -> (a -> rest)
> apply = flip (.)

> apply2 :: (a -> b -> c) -> (c -> rest) -> (a -> b -> rest)
> apply2 f g = (g .) . f

Example:

(\a b c -> f a (a+b) (g c)) = dup . deep (apply2 (+) . deep (apply g)) $ f

Oh the pointfree fun!

Thanks to ski on #haskell who gave a link to his earlier work in the same vein.