Joachim Breitner

Blog

Explicit vertical alignment in Haskell

Published 2016-08-30 in sections English, Haskell.

Chris Done’s automatic Haskell formatter hindent is released in a new version, and getting quite a bit of deserved attention. He is polling the Haskell programmers on whether two or four spaces are the right indentation. But that is just cosmetics…

I am in principle very much in favor of automatic formatting, and I hope that a tool like hindent will eventually be better at formatting code than a human.

But it currently is not there yet. Code is literature meant to be read, and good code goes at length to be easily readable, and formatting can carry semantic information.

The Haskell syntax was (at least I get that impression) designed to allow the authors to write nicely looking, easy to understand code. One important tool here is vertical alignment of corresponding concepts on different lines. Compare

maze :: Integer -> Integer -> Integer
maze x y
| abs x > 4  || abs y > 4  = 0
| abs x == 4 || abs y == 4 = 1
| x ==  2    && y <= 0     = 1
| x ==  3    && y <= 0     = 3
| x >= -2    && y == 0     = 4
| otherwise                = 2

with

maze :: Integer -> Integer -> Integer
maze x y
| abs x > 4 || abs y > 4 = 0
| abs x == 4 || abs y == 4 = 1
| x == 2 && y <= 0 = 1
| x == 3 && y <= 0 = 3
| x >= -2 && y == 0 = 4
| otherwise = 2

The former is a quick to grasp specification, the latter (the output of hindent at the moment) is a desert of numbers and operators.

I see two ways forward:

  • Tools like hindent get improved to the point that they are able to detect such patterns, and indent it properly (which would be great, but very tricky, and probably never complete) or
  • We give the user a way to indicate intentional alignment in a non-obtrusive way that gets detected and preserved by the tool.

What could such ways be?

  • For guards, it could simply detect that within one function definitions, there are multiple | on the same column, and keep them aligned.
  • More general, one could take the approach lhs2Tex (which, IMHO, with careful input, a proportional font and with the great polytable LaTeX backend, produces the most pleasing code listings) takes. There, two spaces or more indicate an alignment point, and if two such alignment points are in the same column, their alignment is preserved – even if there are lines in between!

    With the latter approach, the code up there would be written

    maze :: Integer -> Integer -> Integer
    maze x y
    | abs x > 4   ||  abs y > 4   = 0
    | abs x == 4  ||  abs y == 4  = 1
    | x ==  2     &&  y <= 0      = 1
    | x ==  3     &&  y <= 0      = 3
    | x >= -2     &&  y == 0      = 4
    | otherwise                   = 2

    And now the intended alignment is explicit.

(This post is cross-posted on reddit.)

Eine Woche Philadelphia

Published 2016-08-05 in sections Deutsch, Philadelphia.

Es ist wieder Freitag, und ich sitze wieder in einem Zug. Letzte Woche war es der ICE nach Philadelphia (mit einmal Umsteigen am Flughafen Frankfurt), jetzt ist es der Amtrak Northeastern Regional train nach Boston, wo ich übers Wochenende eine Freundin besuche. Erzählen will ich jetzt aber nicht von Boston, sondern von meiner ersten Woche Philadelphia.

Die Wohnung

Nach dem dank Premium-Economy-Platz (günstiger als ein Economy-Flug mit zusätzlichem Freigepäck) recht angenehmen Flug und einer Stunde unnützem Warten in der Schlange vor der Passkontrolle erreichte ich am späten Nachmittag per Taxi mein neues Zuhause im Westen von Philadelphia. Es war heiß, schwül und unangenehm schwitzig.

Der Schlüssel lag – wie vereinbart – im Briefkasten. Der erste Eindruck des Wohn- und Esszimmers war mäßig: Geräumig, aber es stand viel Krempel herum.

Anders mein Zimmer: In dem als „möbliert ohne Bett“ beworbenem Zimmer stand weniger herum als erwartet. So war da zwar ein kleiner Schreibtisch, aber kein Stuhl dazu. Was auch nicht da war war die aufblasbare Luftmatratze meiner Mitbewohnerin, die mir versprochen hatte, diese in das Zimmer zu legen.

Ich spazierte noch einmal die Baltimore Avenue entlang und kaufte bei einem genossenschaftlich betriebenen und ökologisch angehauchtem Supermarkt das nötigste (Tee, Milch, Oatmeal).

Aber bald machte sich die Müdigkeit breit (gefühlt war es ja bereits vier Uhr morgens). Ich hatte zwar kein Bett, aber zum Glück hatte ich Isomatte und Schlafsack mitgenommen. Die breitete ich aus, steckte als Kissen einen Pulli in einen Stoffbeutel, und legte mich schlafen. Wegen Hitze und unbequemer Matratze schlief ich allerdings nicht ein, und kurz drauf klopfte es an meiner Tür: Jene Mitbewohnerin zeigte sich und brachte mir die Luftmatratze. Dank elektrischer Pumpe war diese auch schnell einsatzbereit, so dass ich die erste Nacht doch auf etwas halbwegs bettähnlichem verbringen konnte.

Am nächsten Tag oder, besser, in der nächsten Nacht machte sich der Jetlag noch deutlich bemerkbar. Ich schlief nur bis zwei Uhr morgens (ich bin die letzten Jahre wohl zu regelmäßig um acht Uhr aufgestanden). Ich versuchte dann noch so gut es geht zu dösen, aber um vier Uhr war ich endgültig zu wach und begann, Zeug am Rechner zu erledigen.

Als es dann wirklich Morgen war und ich gefrühstückt hatte (und ich die Theorie aufgestellt habe, dass dort wenige Leute den Schwarztee zum selber abfüllen kaufen, er daher entsprechend lange in dem Laden stand und so etwas an Geschmack verloren hat) machte ich mich auf den Weg, die wichtigsten ersten Erledigungen zu machen: Erst eröffnete ich ein Bankkonto, was erstaunlich unproblematisch war, zumindest solange mir die Debit-Karte reicht. Dann ging es zum IKEA. Bisher habe ich IKEA gemieden und versucht, bei Einzelgeschäften oder kleineren Ketten zu kaufen, aber in dem Fall überwog die Bequemlichkeit, zu einem Laden zu gehen, wo ich ungefähr weiß, was mich erwarte, wo ich alles bekomme was ich brauche und der mir die Einkäufe nach Hause liefert.

Ich brauchte etwa eine Stunden mit dem Bus von West Philadelphia zum IKEA in Süd-Philadelphia, und besorgte mir ein Bett, eine Matratze, eine Decke, Kissen, Bezüge, einen Schreibtischstuhl und ein Bücherregal. Das zu finden brauchte auch nur kaum länger als das Warten am Schalter der die Nach-Hause-Lieferungen entgegennimmt. Aber das Warten zahlte sich aus: Nicht nur dass die Möbel für nur 40$ noch am gleichen Tag geliefert werden, auch entdeckte der Mitarbeiter auf dem Kassenzettel dass mir der Bettrahmen doppelt berechnet wurde, und der Fehler lies sich korrigieren.

Mit der Ansage, dass „zwischen fünf und neun Uhr“ meine Möbel geliefert werden, und einem großen Beutel mit allen kleineren Artikeln, die sie nicht liefern wollten in der Hand machte ich mich auf dem Weg zur Bushaltestelle. Kurz vor fünf war ich dann zu Hause und wartete gespannt ob das mit der Lieferung klappt. Tatsächlich: Halb 9 fuhr ein Laster vor und mir wurden meine Möbel ins Haus gestellt.

Hammermäßiges Werkzeug

Hammermäßiges Werkzeug

Erfreut, nicht noch eine Nacht auf der Luftmatratze schlafen zu müssen machte ich mich an den Zusammenbau. Ich hatte in meiner IKEA-Unerfahrenheit nicht bedacht, dass man sogar für IKEA-Möbel eigenes Werkzeug braucht (also, Schraubenzieher und Hammer) und musste auf mein Taschenmesser sowie – als Hammerersatz – einen Fahrradständer, den ich im Krempel im Wohnzimmer fand, zurückgreifen. Zumindest bis meine Mitbewohnerin dann doch zumindest einen Kreuzschlitz-Schraubenzieher fand. Bei insgesamt über 150 Schrauben wäre das mit dem Taschenmesser auch auf Dauer recht unangenehm geworden.

Es dauerte bis nach 11 Uhr bis das Bett dann endlich stand. Ich hatte immernoch vom Jetlag, und während ich die letzten Schrauben reindrehte musste ich aktiv verhindern, dass mir die Augen zufielen. Als das Bett fertig gebaut, und das Bettzeug aufgezogen war, schlief ich dann auch schnell, und immerhin ein wenig länger als die Nacht zuvor (ich glaube bis um 6?).

Die restlichen Möbel baute ich dann am Sonntag auf. Ich habe ein paar Bilder des fertigen Zimmers gemacht.

Stillleben mit Tux

Stillleben mit Tux

Mein erster Eindruck der Wohnung trog übrigens: Am Mittwoch Abend gab es ein Treffen der Bewohner und wir misteten Kühlschrank, Küche, Esszimmer und Wohnzimmer aus. Nun macht das Haus einen ganz wohnlichen Eindruck. Mit der Truppe – aus drei Frauen und drei Männern, wobei einer noch nicht eingezogen ist – scheine ich gut zurecht zu kommen. Es besteht wohl prinzipiell Interesse an Brettspielen (und wenn ich Sonntag Abend nicht zu früh zu müde gewesen wäre, hätten wir wohl was gespielt), wir haben einen Gruppenchat eingerichtete (wofür ich noch einen Instant Messenger installieren musste, Group me in diesem Fall), einer war beim Swing-Tanzen dabei und eine weitere will auch mal mit. Von gemeinsam Kochen war zumindest mal die Rede (und ich werds mal mit Käßspätzle probieren).

Die Uni

Aber ich bin ja nicht wegen einer netten WG hier hergezogen, sondern um als Post-Doc an der University of Pennsylvania zu arbeiten. Also begab ich mich Montag früh zu Fuß in das Gebäude mit meinem Büro, der sogenannten Levine Hall. Von meiner Wohnung aus sind es 20 Minuten zu Fuß, Fotos von meinem Arbeitsweg habe ich bereits hochgeladen.

Dort angekommen schaute ich erst bei der Sekretärin des Lehrstuhls vorbei, die mich in mein schönes zwei-Mann-Büro mit großem Fenster und Blick zum Innenhof führte. Auf dem Schreibtisch stand bereits mein neuer Laptop, für den ich eine Woche vorher meine Wunschkonfiguration gemailt hatte. Auch lag da der Schlüssel, die Mitarbeiterkarte, meine Zugangsdaten fürs Uni-Netz und ein Stapel an den üblichen Formularen, wobei die Daten, die der Personalabteilung bereits bekannt waren, schon vorausgefüllt waren. Ich bekam noch eine kurze Tour zu Küche und Kopierraum, und schon konnte ich loslegen.

Pustekuchen.

Dort angekommen schaute ich erst einmal bei einer Mitarbeiterin der Verwaltung vorbei, die mir die freien Schreibtische zeigen sollte. Allerdings war ich (Jetlagbedingt) mit halb 9 etwas zu früh, und lümmelte eine halbe Stunde herum, bevor dann jemand kam und mir meine Möglichkeiten zeige.

Zuerst ein Schreibtisch im Nachbarflügel, zwei Stockwerke tiefer als meine Gruppe, in einem langgezogenem Zimmer, in dem mehrere Reihen kleiner Schreibtische reingequetscht wurden. Am schmalen Ende ein Fenster, recht groß, aber über Kopfhöhe. Nein Danke. Als nächstes ein Schreibtisch, im gleichen Stockwerk wie meine Gruppe, aber drei Flure weit weg, in einem Zimmer ohne Fenster und 4 Plätzen drin. Ein wenig besser.

Dann fragte ich nochmal ausdrücklich nach Zimmer 513 oder 514, wo die anderen Post-Docs und Doktoranden meiner Gruppe sitzen. Sie ging in ihr Büro zurück, ging ein paar Ausdrücke durch und tatsächlich, in 514 ist wohl gerade jemand fertig geworden. Und das wurde es dann – aber warum nicht gleich?

Hässlich ist es leider trotzdem: Ein geschätzt 5m×10m großes Zimmer, mit Trennwänden in zwei Quadrate geteilt, und in jedem Quadrat in jeder Ecke ein Arbeitsplatz gepackt.

Meine Ecke

Meine Ecke

Formulare waren natürlich auch keine vorausgefüllt. Ich ging also zur Personalabteilung, füllte dort eine Hand voll Zettel aus, und gab sie ab. Nachdem diese dann bearbeitet wurden (am Donnerstag) stellten sie fest dass ein Zettel fehlte, den ich zwar am Montag dabei hatte, aber da keiner haben wollte. Den brachte ich dann am Freitag. Im Gegenzug gab es ein Formular, mit dem ich zur PennCard-Ausgabestelle ging und meine Mitarbeiterkarte bekam. Wieder im Büro wollte ich damit meinen Uni-Zugang einrichten, und erfuhr, dass ich dazu erst mit meiner PennCard bei der PennCard-Ausgabestelle vorbeischauen muss, um ein Registrierungscode zu erhalten… Es stellt sich die Frage, warum dir mir nicht gleich gesagt haben „Hier ist Ihre PennCard, brauchen Sie auch einen Uni-Zugang?“. Also wieder hin, in der Schlange gewartet, Zugangscode erhalten, wieder an meinen Laptop, und endlich meinen sogenannten PennKey erhalten – es war sogar noch joachim frei. Damit konnte ich jetzt den Benutzeraccount an der Fakultät beantragen, und wenn der dann nächste Woche da ist kann ich so langsam richtig arbeiten (Webseiten für die Vorlesung, die ich halten werde, einrichten und solche Sachen).

Apropos Arbeiten: Mein neuer Dienst-Laptop ist noch lang nicht da, das dauert noch zwei Wochen oder so. Ich verwende also noch den aus Karlsruhe, den ich netterweise ein wenig länger benutzen darf. Und Internetzugang hab ich auch nur dank eduroam (dem weltweiten WLAN-Verbund für Akademiker) und meinen Karlsruher Zugangsdaten. Hätte ich das nicht, ich könnte so ungefähr gar nichts machen.

Alles in allem habe ich nicht das Gefühl, ein willkommener, gebrauchter und geschätzter neuer Mitarbeiter zu sein, sondern eher wie ein Besucher, dem die Uni gnädigerweise erlaubt, sich in einer Ecke, die gerade frei ist, einzurichten und den man sonst sich selbst überlässt. Aber ich befürchte dass es einfach keine gut organisierte Verwaltung ist und es vermutlich auch neuen Professoren so ergehen würde (mal abgesehen von den hässlichen Schreibtischen: Die haben schöne Büros mit große Fensterfront).

Immerhin sind die Kollegen (wenn auch über mehrere Büros verteilt) soweit nett und umgänglich, und meinen Ambitionen, ein gemeinsames Mittagessen draußen zur Institution zu machen, offen gegenüber. Es gibt hier, soweit ich das sehe, keine Mensa wie ich sie kenne. Die Hälfte der Mitarbeiter bringt sich Essen in Tupperdosen mit und wärmt es in der Mikrowelle auf, die andere geht raus und zu einem der vielen Foodtrucks (= mobile Imbissbuden), die Essen verschiedener Art in mit der Mensa vergleichbarer Qualität anbieten. Letztes produziert pro Mahlzeit leider mindestens eine Plastiktüte, ein Plastik- oder Styropor-Behälter und eine Plastikgabel an Müll.

Philadelphia

Mangels fahrbarem Untersatz (ein neues Fahrrad wurde bestellt und werde ich nächste Woche in Betrieb nehmen; ich werde berichten) ist mein Radius bisher auf den Campus und mein westlich angrenzendes Viertel begrenzt. Aber fürs erste genügt das und ich komme auch zu Fuß gut genug rum, wenn nicht gerade eine Straßenbahn kommt und ich diese nehme.

Der öffentliche Nahverkehr ist soweit in Ordnung. Es gibt ein paar Straßenbahnen (davon eine direkt von vor meiner Haustüre zur Uni) und in Philadelphia insgesamt viele Buslinen. Manches wirkt allerdings etwas undurchdacht:

  • Es gibt meines Wissens keine Karte von Philadelphia mit allen Buslinien drauf, weder Online und erst recht nicht an den Bushaltestellen, wo man sie erwarten würde. Für jede einzelne Buslinie gibt es Karten online, aber die kann ich ja schlecht alle anschauen. Wie ich von West Philadelphia zum IKEA komme habe ich nur per Google herausgefunden.

  • Die verschiedenen Straßenbahnen fahren in der Stadtmitte und auf dem (genauer: unter dem) Campus auf der selben Strecke und fächern sich dann gen Westen auf. Die Straßenbahnnummer steht allerdings nur vorne am Wagen, von der Seite sehen sie alle gleich aus. Wenn man also in der unterirdischen Campus-Station sitzt, wartet und vielleicht ein Buch liest, muss man trotzdem jede einfahrende Bahn rechtzeitig anschauen und die Liniennummer lesen, sonst weiß man nicht, ob man einsteigen soll oder nicht. Es gibt zwar eine Digitalanzeige in der Station, aber die zeigt den Namen der Station an, und nicht etwas wann die nächste Bahn kommt, und welche das ist.

Welche Bahn kommt da jetzt?

Welche Bahn kommt da jetzt?

Es fällt auch auf dass die Zusammensetzung der Bevölkerung sehr davon abhängt, wo man gerade ist. Im IKEA ist es so bunt gemischt ist, wie man es von einer amerikanischen Großstadt erwartet. Im Bus auf dem Weg zum IKEA waren es fast nur Schwarze, die tendenziell eher ärmer wirken. Auf dem Campus laufen wiederum deutlich mehr mit asiatischem Ursprung herum. Mein Wohnviertel scheint ein Gentrifizierungs-Schauplatz zu sein: Restaurants, Hippe Cafes, alternative Läden, Eismanufakturen, aber je weiter nach Osten (weg vom Campus) man kommt, desto heruntergekommener die Gegend. Irgendwo da war mal ein RadioShack (eine allgegenwärtige Elektronik- und Technikkette), und das Schild war auch noch auf dem Gebäude, aber drin war ein Krämer mit Sofas, Kabeln, Lautsprechern und weiß nicht was. Hier laufen mehr „kaputte Gestalten“ herum und ich wurde mehrfach angebettelt. (Aber alles noch so dass zumindest ich mich nicht unwohl oder unsicher gefühlt habe.)

Ein erstes Fazit

Bisher muss ich sagen dass das noch keine Verbesserung meiner Gesamtlebenssituation ist, eher im Gegenteil. Ich hatte es mir nach 12 Jahren in Karlsruhe halt doch ganz gut eingerichtet gehabt. Aber übernächste Woche kommt meine Chefin aus dem Urlaub, und kurz darauf beginnen die Vorlesungen. Wenn ich dann erst mal etwas vernünftiges zu tun habe und mich ein wenig eingelebt habe, kann das ja noch was werden.

PS: Es kamen beide Pakete an. Das erste war schon da als ich kam, aber da nur das eine da war, und dieses vom Transport recht lädiert war, habe ich für das schon schwarz gesehen, aber eine Woche stand auch das auf der Veranda. Immerhin.

Ein schlüsselloser Moment

Published 2016-07-29 in sections Deutsch, Philadelphia.

Im Moment nenne ich keinen Schlüssel mein eigen. Ein seltener und seltsamer Zustand, der nur eines heißen kann: Ich ziehe gerade um. Gerade bin ich, mit großem Koffer, großem Rucksack, Handgepäckkoffer und Laptoptasche beladen, in einen gut gefüllten ICE gestiegen. Der bringt mich an den Frankfurter Flughafen, und von dort geht es dann non-stop nach Philadelphia, wo ich die nächsten zwei Jahre leben und an der University of Pennsylvania arbeiten werden.

Reisefertig

Reisefertig

Es gab mehrere Wünsche nach Berichten. Statt Rundmails zu schicken fülle ich lieber -- wie schon während meiner Zeit in Ghana, Indien und Cambridge -- meinen Blog wieder mit mehr (nicht-technischem) Leben.

Nun bin ich zwar noch nicht in Philadelphia, aber die ersten Reise-bezogenen Anekdoten kann ich bereits zum Besten geben.

Die Abmeldebestätigung

Wer aus Deutschland wegzieht hat sich behördlich abzumelden, so will es das Gesetz. Also gut, ich gehe Anfang Juli zum Bürgerbüro (das unterbeschäftigte in Hagsfeld, wo man immer sofort drankommt).

Erst verlangt die Mitarbeiterin eine Bescheinigung der Vermieterin, dass ich die Wohnung gekündigt habe. Nun kann ich eine solche nicht vorlegen: Meine Vermieterin wollte mich opportunistischer weise nicht aus dem Mietvertrag entlassen, sondern verlangte, dass meine Mitbewohnerin und ich erst ordnungsgemäß kündigen, bevor sie – eventuell und zu schlechteren Bedingungen – mit ihr einen neuen Vertrag aussetzt. Darauf haben wir uns nicht einlassen wollen, und so bleibe ich weiterhin, zumindest pro-forma, Mieter der Wohnung. Nach ein bisschen gut Zureden akzeptierte die Frau vom Bürgerservice das und verzichtete auf eine Kündigungsbescheinigung.

Dann fiel ihr Blick auf mein Auszugsdatum und sie meinte, dass ich zu früh da wäre: Abmeldungen sind erst eine Woche vor dem Wegzug möglich! Welch unsinnige Regel… und ich hatte wenig Lust, in der letzten, mit Umzugs- und Abschiedsstress gefüllten Woche, nochmal nach Hagsfeld zu radeln.

Ich: „Kann ich den Antrag eigentlich auch per Post schicken?“
Sie: „Ja, das geht auch.“
Ich: „Und was passiert wenn ich das schon heute per Post schicke?“
Sie: „Dann bleibt es bis eine Woche vor Ihrem Wegzug liegen.“
Ich: „Aha. Kann ich dann den Antrag nicht einfach jetzt bei Ihnen lassen?“
Sie: „Öh. Ja. Das geht auch.“

Sie legte den Antrag auf einen der Schreibtisch-Stapel, und schrieb in Ihren Papier-Kalender für den letzten Monat groß „Abmeldung Breitner“. Zufrieden ging ich von dannen, in der Erwartung die Sache geklärt zu haben und am Dienstag die Bescheinigung (die ich für GEZ, Banken, Versicherungen etc. brauche) im Briefkasten vorzufinden.

Am Dienstag war nichts im Briefkasten. Am Mittwoch nicht. Gestern radelte ich also zum Amt. Die Dame erinnerte sich wohl, zog ohne Kommentar meinen Antrag aus dem Stapel, auf den sie ihn vor drei Wochen legte, und meinte, es fehle ja noch die Bescheinigung vom Vermieter…

Erneut erklärte ich meine Situation, wedelte mit Visum und Mietvertrag in Philadelphia. Wenige Minuten später lief ich mit der Abmeldebestätigung in der Hand aus dem Büro. Selber und vor Ort klären ist halt doch das einzig wahre.

Das Paket

Wer denkt, dass ich wohl kaum mit den vier oben genannten Gepäckstücken einen Umzug hinbekomme, hat recht: Ein paar Sachen (Brettspiele, Bücher, Wintersachen) wollte ich per Post vorausschicken. Verunsichert durch Horrorgeschichten über die Behandlung von Postpaketen folgte ich dem Rat einer Freundin, statt Pappkartons stapelbare Kunststoffkisten vom Baumarkt zu nehmen, die nicht nur den Inhalt besser schützen sondern auch dort zum Verstauen geschickt sind.

Nun heißt es auf der Webseite von DHL, dass ein Postpaket eine „formstabile Außenhülle aus Pappe, Wellpapper oder Packpapier hat“. Ist meine Kiste nun ein Postpaket?

Wie heut zu Tage Usus fragte ich per Twitter bei DHL nach. Die Antwort klang gut („ja, können Sie schicken“) mit Einschränkungen („ist Sperrgut, kostet extra“). Auf Nachfrage wurde noch ergänzt dass es in Ordnung wäre, wenn ich das Paket in Packpapier einschlage, was allerdings bei einer Kunststoffkiste mit Profilrillen außen wenig sinnvoll wäre.

Ein kurzer Anruf bei der Hotline ergab Widersprüchliches: Laut der Mitarbeiterin dort wäre auch eine Kunststoffkiste ein normales Paket.

Die Pakete

Die Pakete

Also ließ ich es drauf ankommen und wuchtete die zwei Kisten (16 und 25kg) zum Postschalter in der Waldstadt. Mit suggestiver Überzeugung („diese zwei Pakete“) und Small-Talk („Umzug nach USA“) versuchte ich, jegliche Zweifel der Mitarbeiterin im Kern zu ersticken, was vermutlich nicht nötig gewesen wäre, denn die Kisten wurden ohne mit der Wimper zu zucken angenommen.

Spannend bleibt ob und wann die Kisten in den USA ankommen, und was der Zoll damit macht. Zuletzt wurden sie, laut Tracking, vor acht Tagen am Flughafen in Frankfurt gesehen.

Abschiedsmarathon

Die letzte Woche war, nicht überraschend, ein Abschiedsmarathon:

  • Am Sonntag in Herrenberg von meiner Familie und meinen treuen Schulfreunden.
  • Am Montag von meiner Mitbewohnerin und vom Tanzkurs.
  • Am Dienstag von dem Hund meiner Mitbewohnerin (den ich tagsüber sitten sollte) und abends von beim Social Dance von den Swing-Tänzern (denen ich zum Abschied die Live-Band „Insta Swing“ engagierte, die mein Schulfreund Ruben Maisenbacher extra auf die Beine stellte, und die mir im Gegenzug ein nettes „Freunde-Buch“ ausfüllten).
  • Am Mittwoch von meiner Arbeitsgruppe an der Uni, die da geschickterweise den Betriebsausflug hinlegte (Paddeln auf der Kocher, anschließend in den Biergarten, wo ich sogar noch ein auf mich gedichtetes Ständchen hören durfte).
  • Am Donnerstag dann zuletzt sehr entspannt und nett von meinen Karlsruher Freunden bei meinem letzten AbendmahlPicknick im Fasanengarten.

Bilder aus der Woche finden sich (wie dann bald die ersten Bilder aus den USA) in meinem Photoalbum, das Passwort könnt ihr bei mir erfahren.

So gehen zwölf Jahre Karlsruhe zu Ende, und etwas neues beginnt. Ich werde berichten.

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!