# Joachim Breitner's Homepage

## Blog

## The perils of live demonstrations

Yesterday, I was giving a talk at the The South SF Bay Haskell User Group about how implementing lock-step simulation is trivial in Haskell and how Chris Smith and me are using this to make CodeWorld even more attractive to students. I gave the talk before, at Compose::Conference in New York City earlier this year, so I felt well prepared. On the flight to the West Coast I slightly extended the slides, and as I was too cheap to buy in-flight WiFi, I tested them only locally.

So I arrived at the offices of Target^{1} in Sunnyvale, got on the WiFi, uploaded my slides, which are in fact one large interactive CodeWorld program, and tried to run it. But I got a type error…

Turns out that the API of CodeWorld was changed just the day before:

```
commit 054c811b494746ec7304c3d495675046727ab114
Author: Chris Smith <cdsmith@gmail.com>
Date: Wed Jun 21 23:53:53 2017 +0000
Change dilated to take one parameter.
Function is nearly unused, so I'm not concerned about breakage.
This new version better aligns with standard educational usage,
in which "dilation" means uniform scaling. Taken as a separate
operation, it commutes with rotation, and preserves similarity
of shapes, neither of which is true of scaling in general.
```

Ok, that was quick to fix, and the CodeWorld server started to compile my code, and compiled, and aborted. It turned out that my program, presumably the larges CodeWorld interaction out there, hit the time limit of the compiler.

Luckily, Chris Smith just arrived at the venue, and he emergency-bumped the compiler time limit. The program compiled and I could start my presentation.

Unfortunately, the biggest blunder was still awaiting for me. I came to the slide where two instances of pong are played over a simulated network, and my point was that the two instances are perfectly in sync. Unfortunately, they were not. I guess it did support my point that lock-step simulation can easily go wrong, but it really left me out in the rain there, and I could not explain it – I did not modify this code since New York, and there it worked flawless^{2}. In the end, I could save my face a bit by running the real pong game against an attendee over the network, and no desynchronisation could be observed there.

Today I dug into it and it took me a while, and it turned out that the problem was not in CodeWorld, or the lock-step simulation code discussed in our paper about it, but in the code in my presentation that simulated the delayed network messages; in some instances it would deliver the UI events in different order to the two simulated players, and hence cause them do something different. Phew.

## Farewall green cap

For the last two years, I was known among swing dancers for my green flat cap:

This cap was very special: It was a gift from a good friend who sewed it by hand from what used to be a table cloth of my deceased granny, and it has traveled with me to many corners of the world.

Just like last week, when I was in Paris where I attended the Charleston class of Romuald and Laura on Saturday (April 29). The following Tuesday I went to a Swing Social and wanted to put on the hat, and noticed that it was gone. The next day I bugged the manager and the caretaker of the venue of the class (Salles Sainte-Roche), and it seems that the hat was still there, that morning, im Salle Kurtz^{1}, but when I went there it was gone.

And that is sad.

How fitting, given that my granny’s maiden name is Kurz.↩

## Mütze Ade

Seit wohl etwa zwei Jahren ist eine grüne Mütze mein Markenzeichen beim Swing-Tanzen:

Diese Mütze war etwas besonderes, denn sie war ein Geschenk von einer guten Freundin, handgenäht aus einem Tischtuchstoff meiner verstorbenen Oma, und reiste mit mir schon in viele Ecken der Welt.

So auch letzte Woche nach Paris, wo ich am Samstag bei Romuald und Laura einen Charleston-Kurs besuchte – und als ich dann am Dienstag beim Social in Le Chalet du Parc die Mütze aufziehen wollte, war sie nicht mehr da. Ich habe zwar noch den Verwalter und den Hausmeister der Salles Saite-Roche, dem Veranstaltungsort des Kurses, aufgescheucht, und die Mütze wurde wohl noch am Vormittag im Salle Kurtz^{1} gesehen, aber ich war zu spät und die Mütze ist nun weg.

Und das ist schade.

Wie passend, meine Oma ist eine geborene Kurz.↩

## ghc-proofs rules more now

A few weeks ago I blogged about an experiment of mine, where I proved equalities of Haskell programs by (ab)using the GHC simplifier. For more details, please see that post, or the video of my talk at the Zürich Haskell User Group, but one reason why this approach has any chance of being useful is the compiler’s support for rewrite rules.

Rewrite rules are program equations that the programmer specifies in the source file, and which the compiler then applies, from left to right, whenever some intermediate code matches the left-hand side of the equation. One such rule, for example, is

`{-# RULES "foldr/nil" forall k z. foldr k z [] = z #-}`

taken right out of the standard library.

In my blog post I went through the algebraic laws that a small library of mine, successors, should fulfill, and sure enough, once I got to more interesting proofs, they would not go through just like that. At that point I had to add additional rules to the file I was editing, which helped the compiler to finish the proofs. Some of these rules were simple like

```
{-# RULES "mapFB/id" forall c. mapFB c (\x -> x) = c #-}
{-# RULES "foldr/nil" forall k n. GHC.Base.foldr k n [] = n #-}
{-# RULES "foldr/undo" forall xs. GHC.Base.foldr (:) [] xs = xs #-}
```

and some are more intricate like

```
{-# RULES "foldr/mapFB" forall c f g n1 n2 xs.
GHC.Base.foldr (mapFB c f) n1 (GHC.Base.foldr (mapFB (:) g) n2 xs)
= GHC.Base.foldr (mapFB c (f.g)) (GHC.Base.foldr (mapFB c f) n1 n2) xs
#-}
```

But there is something fishy going on here: The `foldr/nil`

rule is identical to a rule in the standard library! I should not have to add to my file that as I am proving things. So I knew that the GHC plugin, which I wrote to do these proofs, was doing something wrong, but I did not investigate for a while.

I returned to this problem recetly, and with the efficient and quick help of Simon Peyton Jones, I learned what I was doing wrong.^{1} After fixing it, I could remove all the simple rules from the files with my proofs. And to my surprise, I could remove the intricate rule as well!

So with this bug fixed, ghc-proofs is able to prove *all* the Functor, Applicative and Monad rules of the Succs functor without any additional rewrite rules, as you can see in the example file! (I still have to strategically place `seq`

s in a few places.)

That’s great, isn’t it! Yeah, sure. But having to introduce the rules at that point provided a very good narrative in my talk, so when I will give a similar talk next week in Pairs (actually, twice, first at the university and then at the Paris Haskell meetup, I will have to come up with a different example that calls for additional rewrite rules.

In related news: Since the last blog post, ghc-proofs learned to interpret proof specifications like

```
applicative_law4 :: Succs (a -> b) -> a -> Proof
applicative_law4 u y = u <*> pure y
=== pure ($ y) <*> u
```

where it previously only understood

```
applicative_law4 = (\ u (y::a) -> u <*> (pure y :: Succs a))
=== (\ u (y::a) -> pure ($ y) <*> u)
```

I am not sur if this should be uploaded to Hackage, but I invite you to play around with the GitHub version of ghc-proofs.

In short: I did not initialize the simplifier with the right

`InScopeSet`

, so RULES about functions defined in the current module were not always applied, and I did not feed the`eps_rules`

to the simplifier, which contains all the rules found in imported packages, such as`base`

.↩

## veggies: Haskell code generation from scratch

How hard it is to write a compiler for Haskell Core? Not too hard, actually!

I wish we had a formally verified compiler for Haskell, or at least for GHC’s intermediate language Core. Now formalizing that part of GHC itself seems to be far out of reach, with the many phases the code goes through (Core to STG to CMM to Assembly or LLVM) and optimizations happening at all of these phases and the many complicated details to the highly tuned GHC runtime (pointer tagging, support for concurrency and garbage collection).

### Introducing Veggies

So to make that goal of a formally verified compiler more feasible, I set out and implemented code generation from GHC’s intermediate language Core to LLVM IR, with simplicity as the main design driving factor.

You can find the result in the GitHub repository of **veggies** (the name derives from “verifiable GHC”). If you clone that and run `./boot.sh some-directory`

, you will find that you can use the program `some-directory/bin/veggies`

just like like you would use `ghc`

. It comes with the full `base`

library, so your favorite variant of HelloWorld might just compile and run.

As of now, the code generation handles all the Core constructs (which is easy when you simply ignore all the types). It supports a good number of primitive operations, including pointers and arrays – I implement these as need – and has support for FFI calls into C.

### Why you don't want to use Veggies

Since the code generator was written with simplicity in mind, performance of the resulting code is abysmal: Everything is boxed, i.e. represented as pointer to some heap-allocated data, including “unboxed” integer values and “unboxed” tuples. This is very uniform and simplifies the code, but it is also slow, and because there is no garbage collection (and probably never will be for this project), will fill up your memory quickly.

Also, the code is currently only supports 64bit architectures, and this is hard-coded in many places.

There is no support for concurrency.

### Why it might be interesting to you nevertheless

So if it is not really usable to run programs with, should you care about it? Probably not, but maybe you do for one of these reasons:

- You always wondered how a compiler for Haskell actually works, and reading through a little over a thousands lines of code is less daunting than reading through the 34k lines of code that is GHC’s backend.
- You have wacky ideas about Code generation for Haskell that you want to experiment with.
- You have wacky ideas about Haskell that require special support in the backend, and want to prototype that.
- You want to see how I use the GHC API to provide a
`ghc`

-like experience. (I copied GHC’s`Main.hs`

and inserted a few hooks, an approach I copied from GHCJS). - You want to learn about running Haskell programs efficiently, and starting from veggies, you can implement all the trick of the trade yourself and enjoy observing the speed-ups you get.
- You want to compile Haskell code to some weird platform that is supported by LLVM, but where you for some reason cannot run GHC’s runtime. (Because there are no threads and no garbage collection, the code generated by veggies does not require a runtime system.)
- You want to formally verify Haskell code generation. Note that the code generator targets the same AST for LLVM IR that the vellvm2 project uses, so eventually, veggies can become a verified arrow in the top right corner map of the DeepSpec project.

So feel free to play around with veggies, and report any issues you have on the GitHub repository.

## Birthday greetings communication behaviour

Randall Munroe recently mapped how he communicated with his social circle. As I got older recently, I had an opportunity to create a similar statistics that shows how people close to me chose to fulfil their social obligations (given the current geographic circumstances):

(Diagram created with the xkcd-font and using these two stackoverflow answers.)

In related news: Heating 3½ US cups of water to a boil takes 7 minutes and 40 seconds on one particular gas stove, but only 3 minutes and 50 seconds with an electric kettle, despite the 110V-induced limitation to 1.5kW.

(Diagram updated on March 30, as the actual mail is slower than the other channels.)

## Why prove programs equivalent when your compiler can do that for you?

Last week, while working on CodeWorld, via a sequence of yak shavings, I ended up creating a nicely small library that provides `Control.Applicative.Succs`

, a new applicative functor. And because I am trying to keep my Haskell karma good^{1}, I wanted to actually prove that my code fulfills the `Applicative`

and `Monad`

laws.

This led me to inserted writing long comments into my code, filled with lines like this:

```
The second Applicative law:
pure (.) <*> Succs u us <*> Succs v vs <*> Succs w ws
= Succs (.) [] <*> Succs u us <*> Succs v vs <*> Succs w ws
= Succs (u .) (map (.) us) <*> Succs v vs <*> Succs w ws
= Succs (u . v) (map ($v) (map (.) us) ++ map (u .) vs) <*> Succs w ws
= Succs (u . v) (map (($v).(.)) us ++ map (u .) vs) <*> Succs w ws
= Succs ((u . v) w) (map ($w) (map (($v).(.)) us ++ map (u .) vs) ++ map (u.v) ws)
= Succs ((u . v) w) (map (($w).($v).(.)) us ++ map (($w).(u.)) vs ++ map (u.v) ws)
= Succs (u (v w)) (map (\u -> u (v w)) us ++ map (\v -> u (v w)) vs ++ map (\w -> u (v w)) ws)
= Succs (u (v w)) (map ($(v w)) us ++ map u (map ($w) vs ++ map v ws))
= Succs u us <*> Succs (v w) (map ($w) vs ++ map v ws)
= Succs u us <*> (Succs v vs <*> Succs w ws)
```

Honk if you have done something like this before!

I proved all the laws, but I was very unhappy. I have a PhD on something about Haskell and theorem proving. I have worked with Isabelle, Agda and Coq. Both Haskell and theorem proving is decades old. And yet, I sit here, and tediously write manual proofs by hand. Is this really the best we can do?

Of course I could have taken my code, rewritten it in, say, Agda, and proved it correct there. But (right now) I don’t care about Agda code. I care about my Haskell code! I don’t want to write it twice, worry about copying mistakes and mismatchs in semantics, and have external proofs to maintain. Instead, I want to prove where I code, and have the proofs checked together with my code!

Then it dawned to me that this is, to some extent, possible. The Haskell compiler comes with a sophisticated program transformation machinery, which is meant to simplify and optimize code. But it can also be used to prove Haskell expressions to be equivalent! The idea is simple: Take two expressions, run both through the compiler’s simplifier, and check if the results are the same. If they are, then the expressions are, as far as the compiler is concerned, equivalent.

A handful of hours later, I was able to write proof tasks like

```
app_law_2 = (\ a b (c::Succs a) -> pure (.) <*> a <*> b <*> c)
=== (\ a b c -> a <*> (b <*> c))
```

and others into my source file, and the compiler would tell me happily:

```
[1 of 1] Compiling Successors ( Successors.hs, Successors.o )
GHC.Proof: Proving getCurrent_proof1 …
GHC.Proof: Proving getCurrent_proof2 …
GHC.Proof: Proving getCurrent_proof3 …
GHC.Proof: Proving ap_star …
GHC.Proof: Proving getSuccs_proof1 …
GHC.Proof: Proving getSuccs_proof2 …
GHC.Proof: Proving getSuccs_proof3 …
GHC.Proof: Proving app_law_1 …
GHC.Proof: Proving app_law_2 …
GHC.Proof: Proving app_law_3 …
GHC.Proof: Proving app_law_4 …
GHC.Proof: Proving monad_law_1 …
GHC.Proof: Proving monad_law_2 …
GHC.Proof: Proving monad_law_3 …
GHC.Proof: Proving return_pure …
GHC.Proof proved 15 equalities
```

This is how I want to prove stuff about my code!

Do you also want to prove stuff about your code? I packaged this up as a GHC plugin in the Haskell library `ghc-proofs`

(not yet on Hackage). The README of the repository has a bit more detail on how to use this plugin, how it works, what its limitations are and where this is heading.

This is still only a small step, but finally there is a step towards low threshold program equivalence proofs in Haskell.

Or rather recover my karma after such abominations such as ghc-dup, seal-module or ghc-heap-view.↩

## Trump is so mean

Vor zweieinhalb Monaten berichtete ich an dieser Stelle von meinen Eindrücken nach der Präsidentschaftswahl (Danke für die motivierenden Rückmeldungen!). Inzwischen ist Donald Trump Präsident, und nun geht es so richtig los.

Am Tag der Amtseinführung habe ich nicht viel mitbekommen. In Philadelphia gab wohl es Proteste, insbesondere am Tag drauf, als hier wie in vielen anderen Städten in und außerhalb der USA der „Women’s March“ statt fand. Über Facebook konnte ich mitverfolgen, welche meiner Bekannten teilnahmen, das war es aber auch erst mal.

Interessant wurden die nächsten Tage, als sich zeigte, dass Trump es ernst meint und mit einer Verfügung nach der anderen seine Vorstellungen in die Tag umsetzen wollte. Ich will hier nicht alles wiederholen, was schon ausführlichst in den Nachrichten, auch in Deutschland, behandelt wurde (die BBC hat eine gute Zusammenfassung der ersten Woche).

Für mich und mein akademisches Umfeld am relevantesten waren zwei Entwicklungen: Zum einen verfügte Trump einen Maulkorberlass für viele Behörden, und für das Umweltamt sogar einen kompletten Einstellungs- und Auftragstop, und von der Seite des Weißen Hauses verschwanden Abschnitte zum Klimawandel. Auch wenn sich ein paar Nationalparkranger dem Anfangs widersetzten – das ist nicht mehr ein Umfeld von freier Wissenschaft und Ratio-geleiteter Politik.

Noch heftiger war die Reaktion dann als Trump plötzlich und ohne Vorwarnung die Einreise von Bürgern sieben vorwiegend muslimischer Staaten, darunter dem Iran, stark einschränkte. Einige Reisende oder Wiederkehrende aus diesen Staaten wurden nun am Flughafen länger befragt, abgewiesen oder direkt zurückgeschickt. In meinem Freundeskreis hier sind auch Wissenschaftler aus dem Iran, deren Vertrauen in eine verlässliche Zukunft in den USA nun schwer beschädigt ist. Denn betroffen sind nicht etwa nur Bewerber um neue Visas, die sich nun auf längere Wartezeiten einstellen müssten, sondern auch solche, die schon längst ein Visum – oder gar eine permanente Aufenthaltsgenehmigung (*green card*)^{1} – haben und sich in den Staaten eine Existenz aufgebaut haben.

Über Facebook erfuhr ich dass einige meiner Freunde, insbesondere eben jene Iranerin, an einer spontanen Demonstration heute Nachmittag am Flughafen von Philadelphia teilnehmen wollten, und dem schloss ich mich an. Allerings nicht nur ich, so dass schon die Autobahn zum Flughafen von den Autos empörter Bürger verstopft war und zeiweise die Autobahnausfahrten gesperrt waren.

Die Empfangshalle des Flughafens, dem angedachten Ort für den Protest, war angesichts von über 5000 Teilnehmern schon längst voll. Die in großer Zahl (und mit Pferden) aufmaschierte Polizei sperrte den Zugang und verlegte den Protest vor das Gebäude.

Ich mischte mich also eine Weile unter das dort protestierende Volk, lauschte den Sprechchören („No hate, no fear – refugees are welcome here“, „Let them in“, „This is what democracy looks like“) und bewunderte die unzähligen Pappschilder. Die Bilder hier sind eine Auswahl der besten (und weitere gibt es auf meiner Bilderseite).

Hier wurde später zurückgerudert.↩

## Global almost-constants for Haskell

More than five years ago I blogged about the “configuration problem” and a proposed solution for Haskell, which turned into some Template Haskell hacks in the seal-module package.

With the new GHC proposal process in plase, I am suddenly much more inclined to write up my weird wishes for the Haskell language in proposal form, to make them more coherent, get feedback, and maybe (maybe) actually get them implemented. But even if the proposal is rejected it is still a nice forum to discuss these ideas.

So I turned my Template Haskell hack into a proposed new syntactic feature. The idea is shamelessly stolen from Isabelle, including some of the keywords, and would allow you to write

```
context fixes progName in
foo :: Maybe Int -> Either String Int
foo Nothing = Left $ progName ++ ": no number given"
foo (Just i) = bar i
bar :: Int -> Either String Int
bar 0 = Left $ progName ++ ": zero no good"
bar n = Right $ n + 1
```

instead of

```
foo :: String -> Maybe Int -> Either String Int
foo progName Nothing = Left $ progName ++ ": no number given"
foo progName (Just i) = bar progName i
bar :: String -> Int -> Either String Int
bar progName 0 = Left $ progName ++ ": zero no good"
bar progName n = Right $ n + 1
```

when you want to have an “almost constant” parameter.

I am happy to get feedback at the GitHub pull request.

## TikZ aesthetics

Every year since 2012, I typeset the problems and solutions for the German math event Tag der Mathematik, which is organized by the Zentrum für Mathematik and reaches 1600 students from various parts of Germany. For that, I often reach to the LaTeX drawing package TikZ, and I really like the sober aesthetics of a nicely done TikZ drawing. So mostly for my own enjoyment, I collect the prettiest here.

On a global scale they are still rather mundane, and for really impressive and educating examples, I recommend the TikZ Gallery.