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.

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.

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

Went to Ruka for some downhill skiing with my folks over easter and had a great time. I retried telemark style after many years of concentrating on polishing my alpine technique and found it very invigorating. The kind of joy I hadn't for years experienced on Finnish slopes (preferring the Alps) was there as sharp as ever. Also, the naturalness of the free-heel turn caught me by surprise. I'm sold, I have to buy a set.

The thing that kept me occupied after a hard day of sliding down the fell was D. B. Weiss's debut novel Lucky Wander Boy, a book that left my head spinning for hours. LWB is a nerd book that doesn't glorify nerds but also a prime example of postmodern fiction that starts off very innocently and ends somewhere out there. Outwardly a straightforward story in three acts, the bulk of the book is just a well-disguised buildup to an out-of-the-box conclusion. Read it, please.

Off-the-record is a crypto protocol implemented as a quite mature open source (LGPL) library. Its purpose is to enable trusted one-to-one instant messaging (etc.) that can be trusted at the moment it is said but can be later plausibly denied. Also, the protocol is built so that there are no long-term keys that when compromised would reveal all past communications. (This is a problem with for example PGP-type encrypted email solutions.) There are OTR plugins for irssi and xchat as well as other IM clients. If asymmetric cryptography and D-H give you that warm fuzzy feeling, this is the coolest toy since ssh.

New chiptune finds: Nullsleep and Pulselooper, both producing authentic Nintendo (NES & Game Boy) beats. Great stuff. Sadly the other releases under the new 56kbps netlabel aren't as good as Pulselooper...

Just found two wicked indie shoot-em-ups.Check them out:

• White Butterfly
• Garden of Coloured Lights

Both work fine under wine and offer some smooth minimalist eye candy and great game mechanics. Check out especially the weapon system of Garden.

Some older findings in the field of shmup minimalism are the games of Kenta Cho, some ported to linux. Rrootage and Noiz2sa are my favourites.

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

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

I'm not sure whether it's actually worthwile to pollute the internets with yet another VCS rant but here goes...

1

Pearls of wisdom on #haskell:

<int-e> Saizan: what advantage does darcs have, over git, for purposes of tracking the history of a wiki? darcs is all about ignoring the history.

Disregarding the wiki context (comment from a discussion about gitit, a haskell wiki engine that uses git as a storage backend), this quote sums up exactly what has been my problem with darcs. Background: I use darcs for managing my config files and for small one-man projects but for everything bigger I just fall back to git.

I'm irked by having to have a separate working copy for each branch. Firstly, this sucks because pushing all branches to a public repo needs additional effort. Also, combined with not-caring-about-history this makes forking from the past or tagging a past revision very ugly. I want my VCS to store everything and not force me to bookkeep on branches. Darcs takes branches back to the SVN age.

Git can be adapted to any sort of workflow and it'll mostly do the right thing. Darcs doesn't have any thing to adapt, and instead of doing the right thing it does nothing on most issues. I appreciate the minimalism, but just don't like the way darcs forces me to act with a large project.

2

Interface-wise, I love the interactive approach of darcs, but git is getting close with those -i flags. rebase -i is great for cleaning up history, commit -i and add -i are almost as nice as darcs's record. gitk is an essential tool for the non-linear development style git encourages (and darcs discourages IMO). After the initial learning curve, git is a great and consistent tool.

As I mentioned earlier, Zendroid uses git. After I started as the third developer at the startup, we needed to establish real (scalable) development practices. I started looking at different open source issue trackers. Two systems that are implemented as git plugins are ticgit and git-issues, the latter being a python clone of the former ruby program.

Both projects are still in their infancy and quite unpolished, but still managed to seem promising. They track tickets that can be assigned, prioritized, commented and solved. However, they do this by using something akin to git-shelve to store ticket information in a separate branch.

This just doesn't work. Git can only operate on one branch at a time. Pushing and pulling changes to the issues branch require checking it out (involving much copying and losing changes made to the working tree (unless git-stash is used)). Also, a single commit can not both fix a bug and mark it as fixed. Of course one could keep a separate working copy with the issues branch checked, which is again not at the level of integration we would want. The tools could (quite easily) provide an interface for syncing the issue branches but although git-issues has such a thing documented, neither project implements it.

This leads to the other gripe I have with these two pieces of software. Both were inadequately documented and often threw backtraces instead of error messages. Somehow both have gotten stuck at the proof-of-concept stage, possibly because of the cumbersome separate branch model. We started looking at alternatives, briefly considering the all-so-trendy Lighthouse and totally not considering trac.

Ditz to the rescue. I had heard of the project previously but had thought it as something simple like devtodo. Not so. Ditz offers all the features git-issues and ticgit do and more. One can group tickets into bundles (releases) and annotate, comment and query them in all thinkable ways. Additionally the tickets are stored in a separate directory in the same branch as the code they refer to, and are formatted as YAML (yay!), making merging very easy and pleasant. Ditz is also well-documented and actively developed. The only problem we have bumped into is that a ticket that someone has claimed can not be "stolen" without hand-editing the ticket files.

So, that sorts out the technology side. On the human side of things we schedule tasks with dated releases. All the issues grouped into a certain release are meant to be cleared before the set date. In addition we have larger releases that roughly correspond to milestones. Ideally, all work done should be related to a ticket claimed by the developer and marked as "started". Changes to tickets are propagated in sync with code changes.

Update 2008-10-06: Git actually uses hardlinks when changing branches, so performance isn't the problem. In any case the semantic load (and ugliness) remains.

Also: I forgot to mention that we have a separate review project that contains code-review tickets.