# Joachim Breitner's Homepage

## Blog

## Compose Conference talk video online

Three months ago, I gave a talk at the Compose::Conference in New York about how Chris Smith and I added the ability to create networked multi-user programs to the educational Haskell programming environment CodeWorld, and finally the recording of the talk is available on YouTube (and is being discussed on reddit):

It was the talk where I got the most positive feedback afterwards, and I think this is partly due to how I created the presentation: Instead of showing static slides, I programmed the complete visual display from scratch as an “interaction” within the CodeWorld environment, including all transitions, an working embedded game of Pong and a simulated multi-player environments with adjustable message delays. I have put the code for the presentation online.

Chris and I have written about this for ICFP'17, and thanks to open access I can actually share the paper freely with you and under a CC license. If you come to Oxford you can see me perform a shorter version of this talk again.

## Communication Failure

I am still far from being a professor, but I recently got a glimpse of what awaits you in that role…

From:Sebastian R. <…@gmail.com>To:joachim@cis.upenn.eduSubject:re: ErrorsI've spotted a basic error in your course on Haskell (https://www.seas.upenn.edu/~cis194/fall16/). Before I proceed, it's cool if you're not receptive to errors being indicated; I've come across a number of professors who would rather take offense than admit we're all human and thus capable of making mistakes... My goal is to find a resource that might be useful well into the future, and a good indicator of that is how responsive the author is to change.

In your introduction note you have written:

n contrast to a classical intro into Haskell, we do not start with numbers, booleans, tuples, lists and strings, but we start with pictures. These are of course library-defined (hence the input CodeWorld) and not part of “the language”. But that does not make them less interesting, and in fact, even the basic boolean type is library defined – it just happens to be the standard library.

Howeverm there is no

`input CodeWorld`

in the code above. Have you been made aware of this error earlier?Regards, ...

Nice. I like when people learn from my lectures. The introduction is a bit werid, but ok, maybe this guy had some bad experiences.

Strangley, I don’t see a mistake in the material, so I respond:

From:Joachim BreitnerTo:Sebastian R. <…@gmail.com>Subject:Re: ErrorsDear Sebastian,

thanks for pointing out errors. But the first piece of code under “Basic Haskell” starts with

`{-# LANGUAGE OverloadedStrings #-} import CodeWorld`

so I am not sure what you are referring to.

Note that these are lecture notes, so you have to imagine a lecturer editing code live on stage along with it. If you only have the notes, you might have to infer a few things.

Regards, Joachim

A while later, I receive this response:

From:Sebastian R. <…@gmail.com>To:Joachim BreitnerSubject:Re: ErrorsGreetings, Joachim.

Kindly open the lecture slides and search for "input CodeWorld" to find the error; it is not in the code, but in the paragraph that implicitly refers back to the code.

You might note that I quoted this precisely from the lectures... and so I repeat myself... this came from

yourlectures; they're not my words!In contrast to a classical intro into Haskell, we do not start with numbers, booleans, tuples, lists and strings, but we start with pictures. These are of course library-defined (hence the input CodeWorld) and not part of “the language”. But that does not make them less interesting, and in fact, even the basic boolean type is library defined – it just happens to be the standard library.

This time around, I've highlighted the issue. I hope that made it easier for you to spot...

Nonetheless, I got my answer. Don't reply if you're going to fight tooth and nail about such a basic fix; it's simply a waste of both of our time. I'd rather learn from somewhere else...

On Tue, Aug 1, 2017 at 11:19 PM, Joachim Breitner wrote:

…

I am a bit reminded of Sean Spicer … “they’re not my words!” … but clearly I am missing something. And indeed I am: In the code snippet, I wrote – correctly – `import CodeWorld`

, but in the text I had `input CodeWorld`

. I probably did write LaTeX before writing the lecture notes. Well, glad to have that sorted out. I fixed the mistake and wrote back:

From:Joachim BreitnerTo:Sebastian R. <…@gmail.com>Betreff:Re: ErrorsDear Sebastian,

nobody is fighting, and I see the mistake now: The problem is not that the line is not in the code, the problem is that there is a typo in the line and I wrote “input” instead of “import”.

Thanks for the report, although you did turn it into quite a riddle… a simple “you wrote import when it should have been import” would have been a better user of both our time.

Regards, Joachim

Am Donnerstag, den 03.08.2017, 13:32 +1000 schrieb Sebastian R.:

…

(And it seems I now made the inverse typo, writing “import“ instead of “input”. Anyways, I did not think of this any more until a few days later, when I found this nice message in my mailbox:

From:Sebastian R. <…@gmail.com>To:Joachim BreitnerSubject:Re: Errorsa simple “you wrote import when it should have been import” would have been a better user of both our time.

We're both programmers. How about I cut ALL of the unnecessary garbage and just tell you to s/import/input/ on that last quotation (the thing immediately before this paragraph, in case you didn't know).

I blatantly quoted the error, like this:

In your introduction note you have written:

n contrast to a classical intro into Haskell, we do not start with numbers, booleans, tuples, lists and strings, but we start with pictures. These are of course library-defined (hence the input CodeWorld) and not part of “the language”. But that does not make them less interesting, and in fact, even the basic boolean type is library defined – it just happens to be the standard library.

Howeverm there is no

`input CodeWorld`

in the code above.Since that apparently wasn't clear enough, in my second email to you I had to highlight it like so:

You might note that I quoted this precisely from the lectures... and so I repeat myself... this came from

yourlectures; they're not my words!In contrast to a classical intro into Haskell, we do not start with numbers, booleans, tuples, lists and strings, but we start with pictures. These are of course library-defined (hence the input CodeWorld) and not part of “the language”. But that does not make them less interesting, and in fact, even the basic boolean type is library defined – it just happens to be the standard library.

This time around, I've highlighted the issue. I hope that made it easier for you to spot...

I'm not sure if you're memeing at me or not now, but it seems either your reading comprehension, or your logical deduction skills might be substandard. Unfortunately, there isn't much either of us can do about that, so I'm happy to accept that some people will be so stupid; after all, it's to be expected and if we don't accept that which is to be expected then we live our lives in denial.

Happy to wrap up this discusson here, Seb...

On Fri, Aug 4, 2017 at 12:22 AM, Joachim Breitner wrote:

…

Well, I chose to be amused by this, and I am sharing my amusement with you.

## How is coinduction the dual of induction?

Earlier today, I demonstrated how to work with coinduction in the theorem provers Isabelle, Coq and Agda, with a very simple example. This reminded me of a discussion I had in Karlsruhe with my then colleague Denis Lohner: If coinduction is the dual of induction, why do the induction principles look so different? I like what we observed there, so I’d like to share this.

The following is mostly based on my naive understanding of coinduction based on what I observe in the implementation in Isabelle. I am sure that a different, more categorial presentation of datatypes (as initial resp. terminal objects in some category of algebras) makes the duality more obvious, but that does not necessarily help the working Isabelle user who wants to make sense of coninduction.

### Inductive lists

I will use the usual polymorphic list data type as an example. So on the one hand, we have normal, finite inductive lists:

`datatype 'a list = nil | cons (hd : 'a) (tl : "'a list")`

with the well-known induction principle that many of my readers know by heart (syntax slightly un-isabellized):

`P nil → (∀x xs. P xs → P (cons x xs)) → ∀ xs. P xs`

### Coinductive lists

In contrast, if we define our lists coinductively to get possibly infinite, Haskell-style lists, by writing

`codatatype 'a llist = lnil | lcons (hd : 'a) (tl : "'a llist")`

we get the following coinduction principle:

```
(∀ xs ys.
R xs ys' → (xs = lnil) = (ys = lnil) ∧
(xs ≠ lnil ⟶ ys' ≠ lnil ⟶
hd xs = hd ys ∧ R (tl xs) (tl ys))) →
→ (∀ xs ys. R xs ys → xs = ys)
```

This is less scary that it looks at first. It tell you “if you give me a relation `R`

between lists which implies that either both lists are empty or both lists are nonempty, and furthermore if both are non-empty, that they have the same head and tails related by `R`

, then any two lists related by `R`

are actually equal.”

If you think of the infinte list as a series of states of a computer program, then this is nothing else than a *bisimulation*.

So we have two proof principles, both of which make intuitive sense. But how are they related? They look very different! In one, we have a predicate `P`

, in the other a relation `R`

, to point out just one difference.

### Relation induction

To see how they are dual to each other, we have to recognize that both these theorems are actually specializations of a more general (co)induction principle.

The `datatype`

declaration automatically creates a *relator*:

`rel_list :: ('a → 'b → bool) → 'a list → 'b list → bool`

The definition of `rel_list R xs ys`

is that `xs`

and `ys`

have the same shape (i.e. length), and that the corresponding elements are pairwise related by `R`

. You might have defined this relation yourself at some time, and if so, you probably introduced it as an inductive predicate. So it is not surprising that the following induction principle characterizes this relation:

```
Q nil nil →
(∀x xs y ys. R x y → Q xs ys → Q (cons x xs) (cons y ys)) →
(∀xs ys → rel_list R xs ys → Q xs ys)
```

Note how how similar this lemma is in shape to the normal induction for lists above! And indeed, if we choose `Q xs ys ↔ (P xs ∧ xs = ys)`

and `R x y ↔ (x = y)`

, then we obtain exactly that. In that sense, the relation induction is a generalization of the normal induction.

### Relation coinduction

The same observation can be made in the coinductive world. Here, as well, the `codatatype`

declaration introduces a function

`rel_llist :: ('a → 'b → bool) → 'a llist → 'b llist → bool`

which relates lists of the same shape with related elements – only that this one also relates infinite lists, and therefore is a coinductive relation. The corresponding rule for proof by coinduction is not surprising and should remind you of bisimulation, too:

```
(∀xs ys.
R xs ys → (xs = lnil) = (ys = lnil) ∧
(xs ≠ lnil ⟶ ys ≠ lnil ⟶
Q (hd xs) (hd ys) ∧ R (tl xs) (tl ys))) →
(∀ xs ys → R xs ys → rel_llist Q xs ys)
```

It is even more obvious that this is a generalization of the standard coinduction principle shown above: Just instantiate `Q`

with equality, which turns `rel_llist Q`

into equality on the lists, and you have the theorem above.

### The duality

With our induction and coinduction principle generalized to relations, suddenly a duality emerges: If you turn around the implication in the conclusion of one you get the conclusion of the other one. This is an example of “co*something* is *something* with arrows reversed”.

But what about the premise(s) of the rules? What happens if we turn around the arrow here? Although slighty less immediate, it turns out that they are the same as well. To see that, we start with the premise of the coinduction rule, reverse the implication and then show that to be equivalent to the two premises of the induction rule:

```
(∀xs ys.
R xs ys ← (xs = lnil) = (ys = lnil) ∧
(xs ≠ lnil ⟶ ys ≠ lnil ⟶
Q (hd xs) (hd ys) ∧ R (tl xs) (tl ys)))
= { case analysis (the other two cases are vacuously true) }
(∀xs ys.
xs = lnil → ys = lnil →
R xs ys ← (xs = lnil) = (ys = lnil) ∧
(xs ≠ lnil ⟶ ys ≠ lnil ⟶
Q (hd xs) (hd ys) ∧ R (tl xs) (tl ys)))
∧ (∀xs ys.
xs ≠ lnil ⟶ ys ≠ lnil
R xs ys ← (xs = lnil) = (ys = lnil) ∧
(xs ≠ lnil ⟶ ys ≠ lnil ⟶
Q (hd xs) (hd ys) ∧ R (tl xs) (tl ys)))
= { simplification }
(∀xs ys. xs = lnil → ys = lnil → R xs ys
∧ (∀x xs y ys. R (cons x xs) (cons y ys) ← (Q x y ∧ R xs ys))
= { more rewriting }
R nil nil
∧ (∀x xs y ys. Q x y → R xs ys → R (cons x xs) (cons y ys))
```

### Conclusion

The coinduction rule is not the direct dual of the induction rule, but both are specializations of more general, relational proof methods, where the duality is clearly present.

More generally, this little excursion shows that it is often beneficial to think of types less as sets, and more as relations – this way of thinking is surprisingly fruitful, and led to proofs of parametricity and free theorems and other nice things.

## Coinduction in Coq and Isabelle

The DeepSpec Summer School is almost over, and I have had a few good discussions. One revolved around coinduction: What is it, how does it differ from induction, and how do you actually prove something. In the course of the discussion, I came up with a very simple coinductive exercise, and solved it both in Coq and Isabelle

### The task

Define the extended natural numbers coinductively. Define the min function and the ≤ relation. Show that min(*n*, *m*) ≤ *n* holds.

### Coq

The definitions are straight forward. Note that in Coq, we use the same command to define a coinductive data type and a coinductively defined relation:

```
CoInductive ENat :=
| N : ENat
| S : ENat -> ENat.
CoFixpoint min (n : ENat) (m : ENat)
:=match n, m with | S n', S m' => S (min n' m')
| _, _ => N end.
CoInductive le : ENat -> ENat -> Prop :=
| leN : forall m, le N m
| leS : forall n m, le n m -> le (S n) (S m).
```

The lemma is specified as

`Lemma min_le: forall n m, le (min n m) n.`

and the proof method of choice to show that some coinductive relation holds, is `cofix`

. One would wish that the following proof would work:

```
Lemma min_le: forall n m, le (min n m) n.
Proof.
cofix.
destruct n, m.
* apply leN.
* apply leN.
* apply leN.
* apply leS.
apply min_le.
Qed.
```

but we get the error message

```
Error:
In environment
min_le : forall n m : ENat, le (min n m) n
Unable to unify "le N ?M170" with "le (min N N) N
```

Effectively, as Coq is trying to figure out whether our proof is correct, i.e. type-checks, it stumbled on the equation `min N N = N`

, and like a kid scared of coinduction, it did not dare to “run” the `min`

function. The reason it does not just “run” a `CoFixpoint`

is that doing so too daringly might simply not terminate. So, as Adam explains in a chapter of his book, Coq reduces a cofixpoint *only* when it is the scrutinee of a `match`

statement.

So we need to get a `match`

statement in place. We can do so with a helper function:

```
Definition evalN (n : ENat) :=
match n with | N => N
| S n => S n end.
Lemma evalN_eq : forall n, evalN n = n.
Proof. intros. destruct n; reflexivity. Qed.
```

This function does not really do anything besides nudging Coq to actually evaluate its argument to a constructor (`N`

or `S _`

). We can use it in the proof to guide Coq, and the following goes through:

```
Lemma min_le: forall n m, le (min n m) n.
Proof.
cofix.
destruct n, m; rewrite <- evalN_eq with (n := min _ _).
* apply leN.
* apply leN.
* apply leN.
* apply leS.
apply min_le.
Qed.
```

### Isabelle

In Isabelle, definitions and types are very different things, so we use different commands to define `ENat`

and `le`

:

```
theory ENat imports Main begin
codatatype ENat = N | S ENat
primcorec min where
"min n m = (case n of
N ⇒ N
| S n' ⇒ (case m of
N ⇒ N
| S m' ⇒ S (min n' m')))"
coinductive le where
leN: "le N m"
| leS: "le n m ⟹ le (S n) (S m)"
```

There are actually many ways of defining `min`

; I chose the one most similar to the one above. For more details, see the `corec`

tutorial.

Now to the proof:

```
lemma min_le: "le (min n m) n"
proof (coinduction arbitrary: n m)
case le
show ?case
proof(cases n)
case N then show ?thesis by simp
next
case (S n') then show ?thesis
proof(cases m)
case N then show ?thesis by simp
next
case (S m') with ‹n = _› show ?thesis
unfolding min.code[where n = n and m = m]
by auto
qed
qed
qed
```

The `coinduction`

proof methods produces this goal:

```
proof (state)
goal (1 subgoal):
1. ⋀n m. (∃m'. min n m = N ∧ n = m') ∨
(∃n' m'.
min n m = S n' ∧
n = S m' ∧
((∃n m. n' = min n m ∧ m' = n) ∨ le n' m'))
```

I chose to spell the proof out in the Isar proof language, where the outermost proof structure is done relatively explicity, and I proceed by case analysis mimiking the `min`

function definition.

In the cases where one argument of `min`

is `N`

, Isabelle’s *simplifier* (a term rewriting tactic, so to say), can solve the goal automatically. This is because the `primcorec`

command produces a bunch of lemmas, one of which states `n = N ∨ m = N ⟹ min n m = N`

.

In the other case, we need to help Isabelle a bit to reduce the call to `min (S n) (S m)`

using the `unfolding`

methods, where `min.code`

contains exactly the equation that we used to specify `min`

. Using just `unfolding min.code`

would send this method into a loop, so we restrict it to the concrete arguments `n`

and `m`

. Then `auto`

can solve the remaining goal (despite all the existential quantifiers).

### Summary

Both theorem provers are able to prove the desired result. To me it seems that it is slightly more convenient in Isabelle because a lot of Coq infrastructure relies on the type checker being able to effectively evaluate expressions, which is tricky with cofixpoints, wheras *evaluation* plays a much less central role in Isabelle, where *rewriting* is the crucial technique, and while one still cannot simply throw `min.code`

into the simpset, so working with objects that do not evaluate easily or completely is less strange.

### Agda

I was challenged to do it in Agda. Here it is:

```
module ENat where
open import Coinduction
data ENat : Set where
N : ENat
S : ∞ ENat → ENat
min : ENat → ENat → ENat
min (S n') (S m') = S (♯ (min (♭ n') (♭ m')))
min _ _ = N
data le : ENat → ENat → Set where
leN : ∀ {m} → le N m
leS : ∀ {n m} → ∞ (le (♭ n) (♭ m)) → le (S n) (S m)
min_le : ∀ {n m} → le (min n m) n
min_le {S n'} {S m'} = leS (♯ min_le)
min_le {N} {S m'} = leN
min_le {S n'} {N} = leN
min_le {N} {N} = leN
```

I will refrain from commenting it, because I do not really know what I have been doing here, but it typechecks, and refer you to the official documentation on coinduction in Agda. But let me note that I wrote this using plain inductive types and recursion, and added `∞`

, `♯`

and `♭`

until it worked.

## The Micro Two Body Problem

Inspired by recent PhD comic “Academic Travel” and not-so-recent xkcd comic “Movie Narrative Charts”, I created the following graphics, which visualizes the travels of an academic couple over the course of 10 months (place names anonymized).

## Bundestag beschließt Ehe für alle

Nach Jahrzehnten des Mauerns und des Blockierens der konservativen Parteien im Bundestag ging plötzlich alles ganz schnell. Auslöser war ein Besuch der Bundeskanzlerin Fräulein Merkel bei Ihrem Amtskollegen Donald Trump. Der Immobilienmogul lebt, sozusagen als Paradebeispiel für den gesellschaftlichen Fortschritt in seinem Land, in einer Ehe mit einer Frau (sogar einer Ausländerin!) lebt. Merkel erzählte danach im Interview mit dem Playboy:

Ich war sehr überrascht und zutiefst bewegt, mitzuerleben, wie fürsorglich, innig und vertraulich die Ehemänner, Verzeihung, Eheleute Trump miteinander umgehen. Und sie sind in den USA damit nicht alleine!

Daher muss ich eingestehen dass ich mir unsicher geworden bin, ob meine Überzeugung in Deutschland noch mehrheitsfähig ist. Ich könnte mir vorstellen, dazu einmal den Bundestag zu befragen – natürlich als Gewissensentscheidung und ohne Fraktionszwang.

Der Koaliationspartner SPD griff diesen Vorschlag umgehend auf und brachte ein „Ehe-für-Alle“ Gesetz auf den Weg, das im entsprechenden Paragrafen des Bürgerlichen Gesetzbuchs den Passus „Die Ehe wird zwischen zwei *Männern* auf Lebenszeit geschlossen.“ durch „Die Ehe wird zwischen zwei *Menschen* auf Lebenszeit geschlossen.“ Der Rest ist Geschichte: Mit den Stimmen der Grünen, der Linkspartei und einiger Abgeordneter der Union (darunter etliche verheiratete Männer!) stimmten dafür. In nur wenigen Monaten können Adam und Eva Müller also im Standesamt den Bund der Ehe eingehen – als wären sie Adam und Stefan Müller.

Besonders ausgiebig feierten die Grünen, die seit ihrer Gründung in den 80ern fanatisch auf diesen Moment hingearbeitet haben. Unvergessen wie Ströbele Anfang der 90er mit einer Dame auf dem Bundespresseball erschien und sie als seine Ehefrau Monika vorstellte (offiziell wohnte sie als Gärtnerin bei ihm). Ebenso unvergessen der März 1996, als die Herren der Grünenfraktion die Abgeordneten der anderen Parteien zu Steak und Pommes einluden und erst hinterher verrieten, dass die Speise tatsächlich und ausschließlich von Frauen zubereitet wurden. Seit dem waren Restaurants mit Unisex-Speisekarten und gemeinsamer Küche im progressiven Berlin immer häufiger anzutreffen.

Frau Gerhard-Ecking (bürgerlich natürlich Fräulein Ecking), Fraktionssprecherin der Grünen, kommentiert den Bundestagsbeschluss:

Frauen dürfen wählen, dürfen als Soldaten dienen. Frauen leiten heutzutage DAX-Konzerne und sogar Samengroßbanken. Es ist unverständlich warum Ihnen trotz dem nicht zugetraut wird, einem Ehemann zu lieben, zu umsorgen, zu unterstützen, mit ihm alt zu werden und sich gegenseitig im Alter abzusichern. Dabei geht es den meisten Ehemännern ja gar nicht darum um diese hohen Werte der Ehe, sie haben es lediglich auf den Steuervorteil abgesehen haben! Endlich also auch Ehemännersplitting für Frauen!

Während Ihrer Rede stand, wie so oft, das bekannte Photomodel Herr Gerhard, hinter ihr und entzückte die Reporter mit einem grau-mellierten Zweiteiler und amüsanter Blümlichenkrawatte. Es heißt, sie hätten gemeinsam ein Kleintierzuchtverein gegründet, um wenigstens bei der Bank ein gemeinsames Konto eröffnen zu könne.

Vehemente Kritik kam wie erwartet von Seiten der katholischen Kirche. Die Doppelspitze der Deutschen Bischofskonferenz, Ehemänner Kardinale Jonas und Hannes Meissner-Stolz, verkündeten in einer Presseerklärung:

Heute ist ein schwarzer Tag für die Christen in der Bundesrepublik. Das heilige Sakrament der Ehe, von Jesus zwölf mal gestiftet, lässt sich nicht per Abstimmung auf Frauen übertragen. Jesus zog mit Jüngern durch das Land, nicht mit Jüngerinnen, und genau so ist Gottes Wille zu verstehen. Frauen und Männer sind von Natur aus zu verschieden. Wenn jetzt noch mehr Männer in Deutschland in so gottloser Weise das Haus und das Bett mit Frauen teilen, wird die Gesellschaft daran zugrunde gehen.

Die Kirche kann Mitglieder, die eine solche „Bundestagsehe“ mit einer Frau eingehen, nicht mehr in ihren Reihen aufnehmen können.

Die Börsen reagierten verhalten. Lediglich die Aktien der Vereinigten Samenbanken notierten mit deutlichen Verlusten. Analysten vermuten dass sich die Gesetzeslage bezüglich Direktzeugung – bisher illegal aber nicht strafbar – in Kürze entsprechend anpasst und dann weniger Frauen die Dienste der Banken in Anspruch nehmen werden.

Fräulein Merkel, die selbst gegen den Gesetzesvorschlag votierte, kommentierte dass sie auch weiterhin an traditionellen, christlichen Werten festhalten wird, und eine Ehe für sie nicht daher in Frage kommt.

## 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`

.↩