NbE With Effects

Usually when playing with dependent types we are tempted into creating pure languages. This may stem from a few different places, the sort of person who wants dependent types is more mathematically inclined and pure languages are closer to math (or are math), or maybe they feel (possibly correctly) that pure languages have nicer engineering properties. However there is one fundamental reason that I think trumps them all, dependent types require comparing arbitrary programs (even ones with free variables) and deciding if they are equivalent.

This is quite easy when the programs are pure, simply run them to their final state and then compare the results, maybe using a few tricks during the comparison, such as alpha and eta rules. Once we want to add in effects however, things get more complicated. With a pure program we have the sense that the final state of an expression, its normal form, encompasses everything there was to know about the expression. The expression (\x. x + 2) 2 doesn’t really convey more information than simply 4. However if we run print "Hello, World!" and get just (), it really does feel like some information is lost, information that we would probably want to use to decide program equivalence.

NbE Without Effects

Let’s take a quick detour and talk about how we usually normalize pure programs. The normal method is to use NbE (normalization by evaluation). There’s a two main reasons for this, it’s usually easier than other methods, and it’s usually faster than other methods. Depending on the day, the fact that this is the case either feels like we’re breaking some law of nature, or completely natural and the perfect embodiment of Rob Pike’s third rule of programming. In any case, the gist of it is this, we transform our expression into some other form where normalization is easier, then we transform back into an expression in such a way that we only produce normal forms. The domain where the forms we transform into live is called the value domain, the transformation from expression to the value domain is called eval, and the transformation back to expression is called quote. This leads us to a system that looks a bit like this.

             eval
            ------>
Expressions         Values
            <------
             quote

The key point to emphasize once again is that the composition of eval and quote always takes expressions to their normal form, even if they have free variables.

NbE With Algebraic Effects

Luckily for me there’s already some work on extending NbE to handle effectful programs, namely the paper by Ahman and Staton, Normalization by Evaluation and Algebraic Effects. Unfortunately for me there’s much to much math in the paper for my brain to parse currently, but I’m pretty sure the NbE algorithm in the paper looks something like this.

                   eval
Expression with   ------> Realm of
Algebraic Effects <------ Mathematics
                   quote

The problems here are that A. I don’t have the realm of mathematics installed on my machine, and B. the language I want to normalize isn’t explicitly one of algebraic effects. However, I think that inspiration can still be drawn from the paper to solve our problem using one key insight they bring up. That is that algebraic effects can be normalized by way of the equation defined for each effect.

Algebraic Effects Without NbE

Let’s take another small detour to quickly discuss what the heck is an algebraic effect. Imagine that we have some program with a single bit of global state. This bit could be thought of as some global boolean switch that we can turn on and off. We might use some function read to read the state, and write to write to it. This would let us have a program like the following:

do
x <- read
if x
then
  do
  write 1
  return "Hello!"
else
  do
  write 0
  return "Goodbye!"

If we were to transform this program into one which uses algebraic effects it would look like this:

read [\x.
  if x
  then write 1 [\(). return "Hello!"]
  else write 0 [\(). return "Goodbye!"]
]

I think the best way to think about this transformation is that each effectful function from before has been turned into the node of a tree where each node has as its child the continuation from the original program.

Now that we have an expression using algebraic effects, we can ask the question, what would it’s normal form look like? Notice in the program above that there’s some redundant writes going on. If the global state is 1 then we “change” it to a 1, and if it’s 0 we write a 0. We can write down an equation that maybe captures this intuition that some algebraic effect tree nodes can be reduced in some way.

read [\x. if x then write 1 [cont] else alt] = read [\x. if x then cont () else alt]
read [\x. if x then alt else write 0 [cont]] = read [\x. if x then alt else cont ()]

There are other equations we could write down, maybe if we write then immediately read we could just remove the read since we know what the state is, but these two will do for now. If we apply these equations to our program to try and get the smallest program possible, then we would get the following:

read [\x.
  if x
  then return "Hello!"
  else return "Goodbye!"
]

Transforming back into our original language we would get:

do
x <- read
if x
then return "Hello!"
else return "Goodbye!"

For a more detailed discussion, and to learn what’s so algebraic about algebraic effects, please see What is Algebraic about Algebraic Effects and Handlers? by Andrej Bauer.

NbE With Algebraic Effects, For Reals

Ok we’ve finally gotten to the good bit, how to do NbE on a program containing effects. In fact we’ve already seen it in the previous section. There we transformed a program into one with explicit algebraic effects, applied some effect equations, then transformed back into the original language. This is simply NbE where the value domain handles effects using algebraic effects. For fun, and for profit, let’s look at this process using an actual real life example that occurs in a project I’m working on. This project contains a language which sits somewhere after closure conversion, and is one where closure allocation has been made explicit. We have some form for allocating closures malloc-clo, and one for applying them app-clo. Let’s look at a simple example for the source program (\x. x) 10.

id env x = x

do
f <- malloc-clo id ()
app-clo f 10

Here the lambda in the source program has been hoisted up to the global level and been named id. If we turn this program into one using algebraic effects, we would get.

id env x = return x

malloc-clo id () [\f.
  app-clo f 10 [\res. return res]
]

Just like we did for the global state example, we can write down some equations to capture our intuition that some effects are redundant.

malloc-clo l env [\f. B(app-clo f a [cont])]   
=
malloc-clo l env [\f B(cont (l env a))]

where B(c) denotes some expression B containing c

malloc-clo l env [\f. B]
=
B
where f does not appear free in B

Now applying this first equation to our example gives us:

id env x = return x

malloc-clo id () [\f.
  return (id () 10)
]

and applying our second equation, and the definition of id gives:

id env x = return x

return 10

This is great considering our intuition that (\x. x) 10 normalizes to 10. It’s also great since we never even really had to simulate heap allocation or the like, even though that’s sort of the effect that we would want from malloc-clo.

It remains to be seen whether or not this approach will pan out, but at least it’s interesting.

Unix is a live programming language.

Files can be thought of as objects which only respond to two messages, read and write.

Plan 9 and FUSE both add the ability for read and write to do more than just do disk i/o.

This makes Linux sort of like a Smalltalk where objects are programmed through FUSE.

The file system provides the “live” part.

Because files can be updated during execution (while the operating system is running), and because there is a level of indirection to refer to them (file paths are pointers, not the contents of the file), changing how a files responds to read and write messages will change how other parts of the system function.

For example, imagine changing /bin/echo to point to a program which is like normal echo but prints a space between each character. How would this change the behaviour of other programs which use it?

The genius of Plan 9 is that it is a distributed object-oriented language which restricts messages to simple byte streams.

In this view, however, executing files is a bit weird.

We can think of exec as a message which causes the object to treat the output of a read message sent to itself as machine code and run it on the cpu.

Hashbangs let us override this behaviour.

The analogy between object orientation (in the original sense) and Unix is more than a novelty, it can bear fruit.

If exec is weird, is it truly needed? Smalltalk itself has no exec.

Imagine a Unix where exec is removed and FUSE is made easy to program.

Imagine a Unix where use defined messages are allowed, files being able to respond to more than just read and write.

Maybe even a Unix where more data types are allowed than the humble byte stream? (Gasp)

I have no idea if any of these ideas would be good, but at least they would be interesting and novel.

They seem, at least to me, to be a genuine mutation of the Unix formula (would a Unix without exec even be a Unix?).

I hope I’m smart and dedicated enough to at least try them out.

And if not me, someone else.

Good software is not only a pleasure to use, but is well written. Unfortunately most software is rarely a pleasure to use, let alone well written.

Window Managers

• dwm

Terminal Emulators

This class of software shouldn’t still be so important by now, finding a better solution for creating interfaces to things is a top priority.

• st

Web Browsers

There are no known web browsers which even approach being good. Use something open source, a free browser might be a contradiction in terms.

Text Editors

Text is the most extensible data format at the moment. Being able to edit it will be of vital importance while this is true.

• vis
• kakoune

Programming Languages

To what degree we should ignore the underlying execution of the code and in what way is unclear. Therefore languages such as Haskell cannot be considered good software at the present time.

• C
• Go

User Interface Tools

• dmenu
• wjt
• xmenu

Today we will be looking at 2 lines of shell script. While they may look quite unassuming, when bound to a shortcut (super-v in my case) they will give you a nice and elegant interface for changing the volume on your system. A demonstration can be found here.

The pre-requisite programs for today are the following

• pamixer
• wjt
• xargs

Without further ado here is the script.

wjt -x $(pamixer --get-volume) \
| xargs -I? pamixer --set-volume ?

The best place to start explaining this is probably wjt.

wjt is a very simple program, when you run it it gives the user a slider bar at the top of their screen. Whenever the user changes the value of the slider (by clicking or using one of the shortcuts, see man wjt) the new value is printed to stdout. An initial value can be provided though the -x flag as we do in our script.

Next we use pamixer to interface with pulseaudio. On the first line pamixer --get-volume does exactly what you would expect, it prints the current volume. Say the current volume is 20. When we run wjt -x $(pamixer --get-volume) the code inside the $() is run first. This code is then replaced by its output, which we established is 20, giving us wjt -x 20. When this is then executed a slider pops up with an initial value of 20.

Finally we will cover xargs. When the first line is executed its output (the new values of the slider) is put into the input of the second using the pipe (|) operator. xargs then takes each line of this output and runs the given command with the ? replaced with the input on that line. Say we run the whole script and then change the slider to 21, xargs will receive a line of input containing 21. It will then take its given command pamixer --set-volume ? and replace the wildcard given by the -I flag (in this case ?) with that line of input and then run the new command. This results in xargs running the command pamixer --set-volume 21 which has exactly the effect you would expect, the system volume is set to 21. xargs then repeats this process for every new line of input, giving us a simple, elegant volume widget.

This is my new website! I’m not quite sure about the colour scheme yet, it’s a bit special…