Joachim Breitner

Blog

HaL deadline extended

Published 2016-07-05 in sections English, Haskell.

There is this long-running workshop series Haskell in Leipzig, which is a meeting of all kinds of Haskell-interested folks (beginners, experts, developers, scientists), and for year’s instance, HaL 2016, I have the honour of being the program committee chair.

The original deadline passed last week, and after looking through the submissions it became clear that although the quality was good, the quantitiy was still lacking. I therefore extended the submission deadline by two weeks, until July 15th.

So if you have something worth talking about, please do submit a proposal1 and come to Leipzig!.

Why should you submit here? Because it gives you a platform to talk about your ideas to an audience that usually does not consist just of your fellow speakers, as it is often with purely academic workshops, but “real” listeners of various kinds. And it is a fun event.

And why should you come to Leipzig? Because of all the interesting talks and tutorials! Of course I cannot say a lot here yet, besides that our invited speaker Alejandro Russo from Chalmers and Gothenburg University will present his work on information-flow control in Haskell (i.e., SecLib, LIO, MAC, HLIO).


  1. And if you want to save me from sleepless nights, submit the first version a few days before the deadline…

When to reroll a six

Published 2016-07-01 in sections English, Mathe.

This is a story about counter-intuitive probabilities and how a small bit of doubt turned out to be very justified.

It begins with the game “To Court the King” (German: „Um Krone und Kragen“). It is a nice game with dice and cards, where you start with a few dice, and use your dice rolls to buy additional cards, which give you extra dice or special powers to modify the dice that you rolled. You can actually roll your dice many times, but every time, you have to set aside at least one die, which you can no longer change or reroll, until eventually all dice have been set aside.

A few years ago, I have played this game a lot, both online (on yucata.de) as well as in real life. It soon became apparent that it is almost always better to go for the cards that give you an extra die, instead of those that let you modify the dice. Intuitively, this is because every additional die allows you to re-roll your dice once more.

I concluded that if I have a certain number of dice (say, n), and I want to have a sum as high as possible at the end, then it may make sense to reroll as many dice as possible, setting aside only those showing a 6 (because that is the best you can get) or, if there is no dice showing a 6, then a single die with the best score. Besides for small number of dice (2 or 3), where even a 4 or 5 is worth keeping, this seemed to be a simple, obvious and correct strategy to maximize the expected outcome of this simplified game.

It is definitely simple and obvious. But some doubt that it was correct remained. Having one more die still in the game (i.e. not set aside) definitely improves your expected score, because you can reroll the dice more often. How large is this advantage? What if it ever exceeds 6 – then it would make sense to reroll a 6. The thought was strange, but I could not dismiss it.

So I did what one does these days if one has a question: I posed it on the mathematics site of StackExchange. That was January 2015, and nothing happened.

I tried to answer it myself a month later, or at least work towards at an answer, and did that by brute force. Using a library for probabilistic calculations for Haskell I could write some code that simply calculated the various expected values of n dice for up to n = 9 (beyond that, my unoptimized code would take too long):

1:  3.50000 (+3.50000)
2:  8.23611 (+4.73611)
3: 13.42490 (+5.18879)
4: 18.84364 (+5.41874)
5: 24.43605 (+5.59241)
6: 30.15198 (+5.71592)
7: 35.95216 (+5.80018)
8: 41.80969 (+5.85753)
9: 47.70676 (+5.89707)

Note that this calculation, although printed as floating point numbers, is performed using fractions of unbounded integers, so there are no rounding issues that could skew the result.

The result supported the hypothesis that there is no point in rolling a 6 again: The value of an additional die grows and approaches 6 from beyond, but – judging from these number – is never going to reach it.

Then again nothing happened. Until 14 month later, when some Byron Schmuland came along, found this an interesting puzzle, and set out a 500 point bounty to whoever solved this problem. This attracted a bit attention, and a few not very successful attempts at solving this. Eventually it reached twitter, where Roman Cheplyaka linked to it.

Coincidally a day later some joriki came along, and he had a very good idea: Why not make our life easier and think about dice with less sides, and look at 3 instead of 6. This way, and using a more efficient implementation (but still properly using rationals), he could do a similar calculation for up to 50 dice. And it was very lucky that he went to 50, and not just 25, because up to 27, the results were very much as expected, approaching value of +3 from below. But then it surpassed +3 and became +3.000000008463403.

In other words: If you have roll 28 dice, and you have exactly two dice showing a 3, then it gives you better expected score if you set aside only one 3, and not both of them. The advantage is minuscule, but that does not matter – it is there.

From then on, the results behaved strangely. Between 28 and 34, the additional value was larger than 3. Then, from 35 on again lower than 2. It oscillated. Something similar could be observed when the game is played with coins.

Eventually, joriki improved his code and applied enough tricks so that he could solve it also for the 6-sided die: The difference of the expected value of 198 dice and having 199 dice is larger than 6 (by 10 − 21...)!

The optimizations that allowed him to calculate these numbers in a reasonable amount of time unfortunately was to assume that my original hypothesis (never rerolling a 6 is optimal), which held until n < 199. But this meant that for n > 199, the code did not yield correct results.

What is the rationale of the story? Don’t trust common sense when it comes to statistics; don’t judge a sequence just from a few initial numbers; if you have an interesting question, post it online and wait for 16 months.

Eindrücke von der GPN16

Published 2016-05-30 in sections Deutsch, Digital World.

Letztes verlängertes Wochenende war wie die alljährliche Gulaschprogrammiernacht des Karlsruher Chaos-Computer-Club-Ablegers entropia, und ich war natürlich dabei.

Ich halte mich auf GPNs vorwiegend ans Vortragsprogramm und erfuhr diesmal, was es Neues bei Rust gibt, wie man im Weltraum kommuniziert und wie man sich mit Raumschiffhüllen vor dem Weltraum schützt. Mein erster Gleitschirmfluglehrer, Alex Zosel, erzählte von seinem Volocopter.

Ich selbst habe mich auch am Programm beteiligt:

  • Ich bot einen Workshop zu meiner Incredible Proof Machine an. Erwartet hatte ich vielleicht fünf bis zehn Teilnehmer, alle mit Laptop, die mit ein bisschen Anleitung mit der Proof Machine spielen oder vielleicht auch daran basteln wollen. Statt dessen wartete ein überfüllter Workshopraum mit über 40 Teilnehmern auf mich, so dass das Ganze dann in einen Stegreif-Vortrag über Aussagenlogik im Allgemeinen und die Proof Machine im Speziellen ausartete.

    Das Feedback zur Proof Machine war sehr positiv. Schon vor dem Workshop sah ich einige GPN-Teilnehmer eifrig Beweise zusammenklicken. Nach dem Workshop wurde ich gebeten, doch statt Professor X an Universität Y die Logik-Vorlesung zu halten.

    Ich hatte am Freitag der Proof Machine ein neues Feature spendiert: Sie zeigt jetzt an, wie komplex der erstellte Beweis (gemessen in der Anzahl der Blöcke) ist, und wie weit man vom bekannten Optimum entfernt ist. Dazu brauche ich natürlich diese Werte, und so bat ich einfach die Workshop-Teilnehmer, von ihren Beweisen diese Zahlen zu melden, was zu einer kleinen Flut an Github-Pull-Requests führte. So einfach bekommt man neue Mitarbeiter!

  • Ich stellte in einem Vortrag mein Git-Performance-Dashboard gipeda, das ich für den Haskell-Compiler GHC geschrieben habe. Den Slot füllte ich gemeinsam mit Sebastian Graf, der sein darauf aufbauendes Tool feed-gipeda vorstellte. Mein Vortrag war jetzt nicht die große Publikums-Show, aber ich denke, dass die, die gipeda vielleicht einsetzen wollen, jetzt wissen, was es genau macht.

Am Samstag Abend war dann noch ein wenig vergnügliches Programmieren angesagt, als ich meinem Kollegen Martin Mohr half, in Django eine Web-Version eines Geschichten-Erzähl-Spiels umzusetzten.

Was ich diese GPN vermisste waren die eigentlich traditionellen Geek-Beschäftigungs-Maßnahmen wie das Programmierspiel, die Schitzeljagd und den GameJam. Wer für nächstes Jahr ein Programmierspiel auf die Beine stellen will, kann sich bei mir melden; ich hab seit zwei Jahren etwa so-gut-wie-fertiges; bisher fehlten mir lediglich die Mitstreiter für die Vor-Ort-Organisation.

PS: Das Gulasch war lecker!

Das Mitschriebwiki zieht um

Published 2016-05-11 in sections Digital World, Deutsch.

Vor bald 12 Jahren habe ich die Webseite http://mitschriebwiki.nomeata.de/ (damals noch unter anderem Namen) ins Leben gerufen, auf der Karlsruher Studenten ihre schön geTeXten Mitschriebe ihrer Mathematik-Vorlesungen hochladen konnten. So kamen im Laufe der Jahre 35 Dokumente zusammen.

In letzter Zeit wurde es ruhig um das Mitschriebwiki, und auch ein Layout-Redesign durch meinen Bruder konnte die Seite nicht mehr mit neuem Leben füllen. (Wo teilen die Studenten heute eigentlich ihre Mitschriebe?) Da ich selbst bald aus Karlsruhe wegziehen werde, ist es nicht mehr sinnvoll, wenn die Software weiter auf meinem privaten Server läuft.

Andererseits floß dort viel Arbeit rein und einige der Mitschriebe werden auch weiterhin regelmäßig von heutigen Studenten heruntergeladen (600 Downloads dieses Jahr, 2000 Downloads letztes Jahr). Außerdem wird es an einigen Stellen im Internet verlinkt.

Daher stelle ich das Mitschriebwiki auf folgende, nachhaltige, Hosting-Lösung um:

Die Wiki-Software “latexki”, die ich eigens für das Mitschriebwiki gebaut hatte, wird dabei auch weiter verwendet, allerdings nur noch um die Ausgabedateien zu generieren – die Skripte, die es ermöglichten, im Webbrowser die Dokumente zu bearbeiten und (mit Konfliktresolution!) direkt ins SVN zu schreiben werden nicht weiter verwendet (was mich ruhiger schlafen lässt). Ich habe nicht vor an der Software noch viel zu ändern, außer dafür zu sorgen, dass sie weiter kompiliert. Ihr findet den Code auf https://github.com/nomeata/latexki

Ich möchte mich an der Stelle nochmal bei allen Mitschriebwiki-Mitautoren bedanken und hoffe, dass die Texte noch vielen weiteren Studentengenerationen eine wertvolle Hilfe ist.

Doctoral Thesis Published

Published 2016-05-09 in sections English.

I have officially published my doctoral thesis “ Lazy Evaluation: From natural semantics to a machine-checked compiler transformation” (DOI: 10.5445/IR/1000054251). The abstract of the 226 page long document that earned me a “summa cum laude” reads

In order to solve a long-standing problem with list fusion, a new compiler transformation, 'Call Arity' is developed and implemented in the Haskell compiler GHC. It is formally proven to not degrade program performance; the proof is machine-checked using the interactive theorem prover Isabelle. To that end, a formalization of Launchbury`s Natural Semantics for Lazy Evaluation is modelled in Isabelle, including a correctness and adequacy proof.

and I assembled all relevant artefacts (the thesis itself, its LaTeX-sources, the Isabelle theories, various patches against GHC, raw benchmark results, errata etc.) at http://www.joachim-breitner.de/thesis/.

Other, less retrospective news: My paper on the Incredible Proof Machine got accepted at ITP in Nancy, and I was invited to give a keynote demo about the proof machine at LFMTP in Porto. Exciting!

Tiptoi-Bastelei mit meinem Neffen

Published 2016-05-07 in sections Deutsch, Tiptoi.

Schon mit einem 4½-jährigen kann man wunderbar eigene Tiptoi-Bastelein erstellen, so wie ich gestern abend mit meinem Neffen:

Der Künstler und sein Werk

Der Künstler und sein Werk

  1. Mein Neffe durfte ein DIN-A4-Blatt bemalen, mit worauf immer er Lust hatte. Bei uns kam das Werk, das im obigen Bild am unteren Rand zu sehen ist.

  2. Dann ließ ich ihn alle Elemente des Bildes beschreiben, während ich seine Stimme mit dem Laptop aufnahm. Zwar nur mit mit dem eingebauten Mikro, aber für eine kleine schnelle Bastelei genügt das, wenn ich die Aufnahme hinterher mit Audacity laut genug mache (Ich habe das über „Normalisieren“ gemacht, bin aber nicht sicher ob dass der richtige Knopf dafür war). Da er das Werk dann zu Hause seiner Schwester zeigen will, ließ ich ihn zusätzlich ein „Hallo Schwester“ für den Anschalt-Sound sprechen.

    Meinem Neffe machte es sichtlich Spaß, seine Stimme aufzunehmen; gleichzeitig ist es eine gute Übung im deutlich Sprechen und im Hand-aus-dem-Mund nehmen.

    Das war es leider auch schon an Arbeitsschritten, an denen mein Neffe mitarbeiten konnte.

  3. Die Aufnahmen speicherte ich (22050Hz, mono, OGG) in ein Verzeichnis, und legte eine einfache YAML-Datei neffe.yaml an:

    language: de
    welcome: HalloSchwester
    product-id: 901
    scripts:
      Auto:
        - P(Auto)
      Feuerwehrhaus:
        - P(Feuerwehrhaus)
      ...
  4. Mit dem Tiptoi-Tool und dem Befehl tttool assemble neffe.yaml erstelle ich die GME-Datei für den Stift, und mit tttool oid-codes neffe.yaml die PNG-Dateien mit den optischen Codes.

  5. Ich fotografierte das Blatt Papier ab und lud das als Hintergrund in ein GIMP-Projekt mit den üblichen Einstellungen (1200dpi, A4). Die Qualität ist nicht wichtig; ich habe das nur genommen, um die Codes ungefähr zu positionieren und auszurichten. Danach blendete ich das Hintergrundsbild wieder aus.

  6. Diese Codes druckte ich auf ein leeres Blatt Papier. Dieses legte ich über die Zeichnung und hielt es gegen das Licht, um zu prüfen, ob die Codes wirklich gut ausgerichtet sind. Jene, die etwas daneben lagen, hab eich dann in GIMP noch einmal verschoben.

  7. Als alles passte, legte ich die Original-Zeichnung in den Drucker (auf die Richtige Orientierung achten!) und druckte die Codes darauf. Das geht nur einmal, also nichts falsch machen!

Achtung: Aufnahme!

Achtung: Aufnahme!

Und fertig: Eine Kinderzeichnung mit Erklärungen vom Künstler persönlich, für seine Schwester und alle seine Freunde. Alles in allem etwa 60 bis 90 Minuten, davon mehr als die Hälfte mit meinen Neffen gemeinsam.

Doktorhut

Published 2016-04-27 in sections Deutsch.

Vorgestern, am 25. April um kurz vor 16 Uhr, wurde mir aus gegebenem Anlass von meinen Kollegen am Lehrstuhl für Programmierparadigmen des Karlsruher Instituts für Technologie ein schwarzer, viereckiger Hut überreicht:

Mein Doktorhut

Mein Doktorhut

Der Tradition entsprechend ist der Hut mit verschiedenen Aufbauten versehen, die etwas mit meinen Hobbies oder meiner Arbeit am Institut zu tun haben. Im Folgenden eine Erklärung der Aufbauten, vor allem für mich selbst in 30 Jahren:

  • Ein Gleitschirm, da ich seit ein paar Jahren Gleitschirm fliege
  • Eine organene Pyramide, das Logo der Karlsruher Spielepyramide, deren dienstäglichen offenen Spieleabend ich oft besuche, und wo ich schon viele Brettspiele kennen gelernt habe
  • Tanzende Paare, da ich, seit ich vor 2½ Jahren mit dem Swing-Tanzen angefangen habe, nun mehrmals die Woche zu Kursen oder zu Socials gehe
  • Ein Straßenschild, was auf die Geschichte mit der Freierzone anspielt
  • Eine leere Knoppers-Packung. Zeitweise wurde am Lehrstuhl nach Feierabend eine Runde Enemy Territory gespielt, und eines Tages ersetzte ich ein paar der Audio-Samples des Spiels durch Aufnahmen meiner Stimme, wo statt „Tank“ oder „Bomb“ eben von „Knoppers“ die Rede war. Dank netzwerkweiter Installation des Spiels ertönte das dann auch bei all meinen Kollegen aus dem Lautsprecher. Soweit ich weiß wurde das bisher nicht rückgängig gemacht.
  • Legosteine, mit denen man Beweise im Stile der Incredible Proof Machine zusammen bauen kann
  • Eine Packung „Philadelphia – Postdocstufe“, da ich diesen Sommer als Post-Doc an der University of Pennsylvania in Philadelphia anfangen werde.

All diese Aufbauen sind per Magnet am Hut befestigt und fehlten ursprügnlich. Erst als ich mit einem Tiptoi-Stift diese Papierzettelchen angetippt hatte, und der Spruch “evaluating thunk” ertönte, wurde mir der jeweilige Aufbau gegeben – ganz im Sinne der „Lazy evaluation“, die auch im Titel meiner Dissertation steht, und selbst eine Anspielung auf meine Tiptoi-Basteleien und das tttool.

Der Zylinder des Huts ist mit Bilderrätseln dekoriert, die noch die Begriffe „Haskell“, „Isabelle“ und „Debian“ darstellten.

Zusätzlich bekam ich eine Langhaar-Perücke, mit der ich mich wieder in die Zeit vor dem großen Schnitt zurückversetzen kann, wie man auf den Bildern von meiner Verteidigung sieht.

Vielen Dank an die Bastler!

Free Paradoxes

Published 2016-02-17 in sections English, Comedy.
Maybe it works if he is a freelancer?

Maybe it works if he is a freelancer?

GHC performance is rather stable

Published 2016-02-09 in sections English, Haskell.

Johannes Bechberger, while working on his Bachelor’s thesis supervised by my colleague Andreas Zwinkau, has developed a performance benchmark runner and results visualizer called “temci”, and used GHC as a guinea pig. You can read his elaborate analysis on his blog.

This is particularly interesting given recent discussions about GHC itself becoming slower and slower, as for example observed by Johannes Waldmann and Anthony Cowley.

Johannes Bechberger’s take-away is that, at least for the programs at hand (which were taken from the The Computer Language Benchmarks Game, there are hardly any changes worth mentioning, as most of the observed effects are less than a standard deviation and hence insignificant. He tries hard to distill some useful conclusions from the data; the one he finds are:

  • Compile time does not vary significantly.
  • The compiler flag -O2 indeed results in faster code than -O.
  • With -O (but not -O2), GHC 8.0.1 is better than GHC 7.0.1. Maybe some optimizations were promoted to -O?

If you are interested, please head over to Johannes’s post and look at the gory details of the analysis and give him feedback on that. Also, maybe his tool temci is something you want to try out?

Personally, I find it dissatisfying to learn so little from so much work, but as he writes: “It’s so easy to lie with statistics.”, and I might add “lie to yourself”, e.g. by ignoring good advise about standard deviations and significance. I’m sure my tool gipeda (which powers perf.haskell.org) is guilty of that sin.

Maybe a different selection of test programs would yield more insight; the benchmark’s games programs are too small and hand-optimized, the nofib programs are plain old and the fibon collection has bitrotted. I would love to see a curated, collection of real-world programs, bundled with all dependencies and frozen to allow meaningful comparisons, but updated to a new, clearly marked revision, on a maybe bi-yearly basis – maybe Haskell-SPEC-2016 if that were not a trademark infringement.

Protecting static content with mod_rewrite

Published 2016-02-08 in sections English, Digital World.

Since fourteen years, I have been photographing digitally and putting the pictures on my webpage. Back then, online privacy was not a big deal, but things have changed, and I had to at least mildly protect the innocent. In particular, I wanted to prevent search engines from accessing some of my pictures.

As I did not want my friends and family having to create an account and remember a password, I set up an OpenID based scheme five years ago. This way, they could use any of their OpenID enabled account, e.g. their Google Mail account, to log in, without disclosing any data to me. As my photo album consists of just static files, I created two copies on the server: the real one with everything, and a bunch of symbolic links representing the publicly visible parts. I then used mod_auth_openid to prevent access to the protected files, unless the users logged in. I never got around of actually limiting who could log in, so strangers were still able to see all photos, but at least search engine spiders were locked out.

But, very unfortunately, OpenID did never really catch on, Google even stopped being a provider, and other promising decentralized authentication schemes like Mozilla Persona are also phased out. So I needed an alternative.

A very simply scheme would be a single password that my friends and family can get from me and that unlocks the pictures. I could have done that using HTTP Auth, but that is not very user-friendly, and the login does not persist (at least not without the help of the browser). Instead, I wanted something that involves a simple HTTP form. But I also wanted to avoid server-side programming, for performance and security reasons. I love serving static files whenever it is feasible.

Then I found that mod_rewrite, Apache’s all-around-tool for URL rewriting and request mangling, supports reading and writing cookies! So I came up with a scheme that implements the whole login logic in the Apache server configuration. I’d like to describe this setup here, in case someone finds it inspiring.

I created a login.html with a simple HTML form:

<form method="GET" action="/bilder/login.html">
 <div style="text-align:center">
  <input name="password" placeholder="Password" />
  <button type="submit">Sign-In</button>
 </div>
</form>

It sends the user to the same page again, putting the password into the query string, hence the method="GET"mod_rewrite unfortunately cannot read the parameters of a POST request.

The Apache configuration is as follows:

RewriteMap public "dbm:/var/www/joachim-breitner.de/bilder/publicfiles.dbm"
<Directory /var/www/joachim-breitner.de/bilder>
 RewriteEngine On

 # This is a GET request, trying to set a password.
 RewriteCond %{QUERY_STRING} password=correcthorsebatterystaple
 RewriteRule ^login.html /bilder/loggedin.html [L,R,QSD,CO=bilderhp:correcthorsebatterystaple:www.joachim-breitner.de:2000000:/bilder]

 # This is a GET request, trying to set a wrong password.
 RewriteCond %{QUERY_STRING} password=
 RewriteRule ^login.html /bilder/notloggedin.html [L,R,QSD]

 # No point in loggin in if there is already the right password
 RewriteCond %{HTTP:Cookie} bilderhp=correcthorsebatterystaple
 RewriteRule ^login.html /bilder/loggedin.html [L,R]

 # If protected file is requested, check for cookie.
 # If no cookie present, redirect pictures to replacement picture
 RewriteCond %{HTTP:Cookie} !bilderhp=correcthorsebatterystaple
 RewriteCond ${public:$0|private} private
 RewriteRule ^.*\.(png|jpg)$ /bilder/pleaselogin.png [L]

 RewriteCond %{HTTP:Cookie} !bilderhp=correcthorsebatterystaple
 RewriteCond ${public:$0|private} private
 RewriteRule ^.+$ /bilder/login.html [L,R]
</Directory>

The publicfiles.dbm file is generated from a text file with lines like

login.html.en 1
login.html.de 1
pleaselogin.png 1
thumbs/20030920165701_thumb.jpg 1
thumbs/20080813225123_thumb.jpg 1
...

using

/usr/sbin/httxt2dbm -i publicfiles.txt -o publicfiles.dbm

and whitelists all files that are visible without login. Make sure it contains the login page, otherwise you’ll get a redirect circle.

The other directives in the above configure fulfill these tasks:

  • If the password (correcthorsebatterystaple) is in the query string, the server redirects the user to a logged-in-page that tells him that the login was successful and instructs him to reload the photo album. It also sets a cookie that will last very long -- after all, I want this to be convenient for my visitors. The query string parsing is not very strict (e.g. a password of correcthorsebatterystaplexkcdrules would also work), but that’s ok.
  • The next request detects an attempt to set a password. It must be wrong (otherwise the first rule would have matched), so we redirect the user to a variant of the login page that tells him so.
  • If the user tries to access the login page with a valid cookie, just log him in.
  • The next two rules implement the actual protection. If there no valid cookie and the accessed file is not whitelisted, then access is forbidden. For requests to images, we do an internal redirect to a placeholder image, while for everything else we redirect the user to the login page.

And that’s it! No resource-hogging web frameworks, not security-dubious scripting languages, and a dead-simple way to authenticate.

Oh, and if you believe you know me well enough to be allowed to see all photos: The real password is not correcthorsebatterystaple; just ask me what it is.