# Joachim Breitner's Homepage

## Blog

## Freierzone, jetzt erst recht

Vor drei Tagen habe ich ja hier einen Vorschlag für ein alternatives Fußgängerzonen-Schild für die Karlsruher Brunnenstraße gemacht. Und siehe da, es hat sich jemand (das Tiefbauamt? ein Street-Artist? die arbeitende Bevölkerung der Brunnenstraße?) meinem Vorschlag angenommen, und tatsächlich das Schild geändert:

Mehr Bilder auf meiner Bilder-Seite.

Ich bin gespannt wie lange es so hängen wird. Wenn Ihr es die nächsten Tage seht, lasst es mich wissen!

**Update (24.11.2015):** Jemand auf Instagram hat das Schild auch entdeckt.

**Update (25.11.2015):** Leider hing das Schild schon heute morgen nicht mehr.

**Update (25.11.2015):** Auch ka-news berichtet.

## Freierzone

In Karlsruhe gibt es eine berüchtigte Straße, die Brunnenstraße, die schön zentral zwischen Studentenkneipe und Campus liegt. Diese ist nicht nur für die eine Art von Verkehr interessant, sondern auch für den anderen, normalen Verkehr: Es ist eine Fußgängerzone, die auch für Radfahrer freigegeben ist.

Soweit, so gut, wir sind ja in Karlsruhe. Inhaltlich finde ich diese Beschilderung durchaus sinnvoll. Aber die Gestaltung ist sehr unpassend – eine Frau mit Kind an der Hand ist doch in diesem Milieu äußerst fehl am Platz. Daher, im Folgenden mein Vorschlag zur passenden Verkehrs-Beschilderung: Das Verkehrszeichen 242 in der Rotlicht-Variante:

Ich hoffe das Karlsruher Tiefbauamt liest mit.

**Update**: Ich weiß nicht ob es das Tiefbauamt war, aber irgendwer hat mitgelesen

## Mehr als Trinken mit Linken

An der Litfaßsäule Vor dem Info-Gebäube klebt zur Zeit dieses Plakat:

So eingängige Sprüche sollen wohl nicht nur einem politischem Sprektrum vorbehalten sein, denn kurze Zeit später hingen da noch ein paar mehr Plakate:

(Und ja, ich würde mir Wünschen dass mein Jolla Phone eine bessere Kamera hätte.)

## Constructing a list in a monad revisited

Two years ago, I discussed various ways of constructing a list in a Monad (or, more specifically, in IO) in Haskell, and compared their merits in terms of elegance, stack usage, number of traversals of the list and run-time efficiency.

Recently, two blog posts discussed the issue further and proposed new, more daring alternatives. Neil Mitchell breaks through the abstraction provided by `IO`

, duplicates “the world” and traverses the list twice, and obtains a speed-up for long lists.

Twarn van Laarhoven went even further and wrote custom C-- code to destructively update the tail-pointer of the list cell to be able to create the list completely evaluated on the first start. This basically answers my question from two years ago:

I’m still wondering: What would be required from Haskell, GHC or the monads in question to have a fully satisfactory solution here, i.e. one that is as fast as the naive recursion, as stack efficient as the difference list solution, and allocates no thunks, only list cells?

He also has a variant with a slightly nicer interface around “holes”, i.e. explicit objects on the heap that can later be replaced by indirections. Obviously, both approaches are very unsafe.

I took this as an opportunity to redo my benchmark measurements, and include their variants (named `escapeIO`

, `hackIO`

and `holeIO`

). The following table omits the variants with quadratic performance, as I ran it on longer lists now:

Variant | 10^0 | 10^1 | 10^2 | 10^3 | 10^4 | 10^5 | 10^6 |
---|---|---|---|---|---|---|---|

accumReverse | 37ns | 153ns | 1134ns | 12µs | 208µs | 8540µs | 97ms |

recursion | 29ns | 139ns | 680ns | 6790ns | 160µs | 6441µs | 76ms |

replicateM | 26ns | 126ns | 677ns | 6785ns | 168µs | 6314µs | 78ms |

accumDList | 35ns | 165ns | 995ns | 10µs | 190µs | 9706µs | 100ms |

streams | 27ns | 136ns | 691ns | 6788ns | 173µs | 5771µs | 75ms |

unsafeInterleave | 60ns | 329ns | 2804ns | 28µs | 373µs | 5605µs | 57ms |

listFix | 51ns | 412ns | 4109ns | 56µs | 2761µs | 42ms | 445ms |

escapeIO | 41ns | 187ns | 1808ns | 16µs | 234µs | 4409µs | 45ms |

hackIO | 30ns | 152ns | 1199ns | 11µs | 140µs | 3701µs | 42ms |

holeIO | 40ns | 222ns | 1725ns | 17µs | 218µs | 4446µs | 53ms |

The following graph shows that around 10000, the naive approaches become much slower and the fancy hacks pay of, with Twarn’s tail-pointer-updating code performing the best:

I would really like to see a package that provides a API like Twarn’s holes, either in this raw unsafe variant (but with the garbage collector related code checked), or with a safe API using type hackery similar to the `ST`

monad that ensures that after “normal” code gets its hands on a term possibly involving holes, the holes may no longer be modified.

I have put the code and results on GitHub.

## Incredible Proof Machine put to the test

I’m currently on the way home, returning from a four-day workshop for high school students; ages 13 to 20, grade 9 to 13. My goal was to teach them something about proofs and logic, in a ambitiously formal and abstract way. For this workshop, I created a computer program called “The Incredible Proof Machine” that allows the kids to explore creating a proof, by placing blocks on a canvas and drawing connections between them (see my previous blog post for an introduction).

Subtracting time spent on on breaks, organizational stuff, the time the student needed to prepare a final presentation, I think we were working for a total of 14 hours, during which we covered propositional logic. I generally let the students explore and try to solve the tasks of one session mostly on their own, followed by a common discussion of what they have just done, what it means why it makes sense etc. The sessions were: assumptions and conclusions in general, with conjunction; implication; disjunction; falsum and *tertium non datur*. We also briefly discussed “paper proofs” with the student: how they look, and how they relate to the Proof Machine proofs. We had some lecture notes that we handed out pice-wise after each session.

The sections were mildly^{1} password-protected to avoid that the quicker students would work ahead, thus keeping the group together. One or two of the 13 students were doing very well and eventually, I gave them the passwords to the predicate logic section and let them work them on them on their own. The quickest managed to solve almost all of these as well, but (as far I as I can tell) without a deeper understanding of the quantifiers, and more a mechanical intuition.

As expected, the students were able to solve most of the exercises, even when a proper understanding of the logical semantics was not yet fully developed. This was by design: I believe that this way it was more motivating and encouraging, as they could “make it work”, compared to a more traditional approach of first throwing a lot of theory at them and then expecting them to apply it. This was confirmed by their feedback after the workshop.

I was happy with my implementation. The students immediately could work with it with very few hick-ups, and only one minor bug occurred^{2}, which I could fix on the spot. Having everything run on in the browser was a big plus, given that we had no stable internet connection for everyone: Once the Incredible Proof Machine was loaded, the student could continue to work offline.

Personally, I find that the UI is occasionally too sluggish, especially on the weaker laptops, but it seems that the students did not seem to mind. Some students tried to connect outputs with outputs or inputs with inputs and the visualization did make it clearly visible that such a link is not actually connected to the block. The predicate logic part is a bit less convincing, with e.g. scoping of local constants not easily understood. I would say that this part would work better if some explanation is given before the students start working on the more involved rules.

Our room was equipped with a smartboard, and I was delighted when I found out, mostly by accident, that I could actually use my finger to drag the blocks of the proof and to draw connections. This not only gave me a “Minority Report”-like feeling, but also meant that it was much easier for the students to follow my explanations when they could just watch my hand, instead of trying to locate the mouse pointer on a regular projector. I’m generally doubtful whether such fancy technological toys are useful in the class room, but in this case at least I liked it. The ability to scribble anywhere on the screen was occasionally a plus as well.

All in all I believe the Proof Machine was a useful tool, and I am sure that without it, it would have been tricky to have students voluntarily spend 14 hours on such a relatively dry and abstract topic. Given the amount of work that went into the development, I hope that this will not be the last occasion where it is put to good use. So if you have to teach formal logic and natural deduction-style proofs, you are welcome to use the Incredible Proof Machine to get your students excited. It is purely static, i.e. needs no special server-side infrastructure, and you can define your own logic (i.e. proof rules), sessions and tasks.

Also, there are a few interesting way in which the Proof Machine could be extended. In particular, I’d like it to be able to generate a “normal”, natural-language proof from a given proof – even if it will sound a bit mechanical – and then use hover-highlight effects to relate the formulas and sentences in the text proof to the connections and blocks in the graphical proof. Contributions are welcome!

## The Incredible Proof Machine

In a few weeks, I will have the opportunity to offer a weekend workshop to selected and motivated high school students^{1} to a topic of my choice. My idea is to tell them something about logic, proofs, and the joy of searching and finding proofs, and the gratification of irrevocable truths.

While proving things on paper is already quite nice, it is much more fun to use an interactive theorem prover, such as Isabelle, Coq or Agda: You get immediate feedback, you can experiment and play around if you are stuck, and you get lots of small successes. Someone^{2} once called interactive theorem proving “the worlds most geekiest videogame”.

Unfortunately, I don’t think one can get high school students without any prior knowledge in logic, or programming, or fancy mathematical symbols, to do something meaningful with a system like Isabelle, so I need something that is (much) easier to use. I always had this idea in the back of my head that proving is not so much about writing text (as in “normally written” proofs) or programs (as in Agda) or labeled statements (as in Hilbert-style proofs), but rather something involving facts that I have proven so far floating around freely, and way to combine these facts to new facts, without the need to name them, or put them in a particular order or sequence. In a way, I’m looking for labVIEW wrestled through the Curry-Horward-isomorphism. Something like this:

So I set out, rounded up a few contributors (Thanks!), implemented this, and now I proudly present: **The Incredible Proof Machine**^{3}

This interactive theorem prover allows you to do perform proofs purely by dragging blocks (representing proof steps) onto the paper and connecting them properly. There is no need to learn syntax, and hence no frustration about getting that wrong. Furthermore, it comes with a number of example tasks to experiment with, so you can simply see it as a challenging computer came and work through them one by one, learning something about the logical connectives and how they work as you go.

For the actual workshop, my plan is to let the students *first* try to solve the tasks of one session on their own, let them draw their own conclusions and come up with an idea of what they just did, and *then* deliver an explanation of the logical meaning of what they did.

The implementation is heavily influenced by Isabelle: The software does not know anything about, say, conjunction (∧) and implication (→). To the core, everything is but an untyped lambda expression, and when two blocks are connected, it does unification^{4} of the proposition present on either side. This general framework is then instantiated by specifying the basic rules (or axioms) in a descriptive manner. It is quite feasible to implement other logics or formal systems on top of this as well.

Another influence of Isabelle is the non-linear editing: You neither have to create the proof in a particular order nor have to manually manage a “proof focus”. Instead, you can edit any bit of the proof at any time, and the system checks all of it continuously.

As always, I am keen on feedback. Also, if you want to use this for your own teaching or experimenting needs, let me know. We have a mailing list for the project, the code is on GitHub, where you can also file bug reports and feature requests. Contributions are welcome! All aspects of the logic are implemented in Haskell and compiled to JavaScript using GHCJS, the UI is plain hand-written and messy JavaScript code, using JointJS to handle the graph interaction.

Obviously, there is still plenty that can be done to improve the machine. In particular, the ability to create your own proof blocks, such as proof by contradiction, prove them to be valid and then use them in further proofs, is currently being worked on. And while the page will store your current progress, including all proofs you create, in your browser, it needs better ways to save, load and share tasks, blocks and proofs. Also, we’d like to add some gamification, i.e. achievements (“First proof by contradiction”, “50 theorems proven”), statistics, maybe a “share theorem on twitter” button. As the UI becomes more complicated, I’d like to investigating moving more of it into Haskell world and use Functional Reactive Programming, i.e. Ryan Trickle’s reflex, to stay sane.

Customers who liked **The Incredible Proof Machine** might also like these artifacts, that I found while looking whether something like this exists:

- Easyprove, an interactive tool to create textual proofs by clicking on rules.
- Domino On Acid represents natural deduction rules in propositional logic with → and ⊥ as a game of dominoes.
- Proofscape visualizes the dependencies between proofs as graphs, i.e. it operates on a higher level than
**The Incredible Proof Machine**. - Proofmood is a nice interactive interface to conduct proofs in Fitch-style.
- Proof-Game represents proofs trees in a sequent calculus with boxes with different shapes that have to match.
- JAPE is an editor for proofs in a number of traditional proof styles. (Thanks to Alfio Martini for the pointer.)
- Logitext, written by Edward Z. Yang, is an online tool to create proof trees in sequent style, with a slick interface, and is even backed by Coq! (Thanks to Lev Lamberov for the pointer.)
- Carnap is similar in implementation to
**The Incredible Proof Machine**(logical core in Haskell, generic unification-based solver). It currently lets you edit proof trees, but there are plans to create something more visual. - Clickable Proofs is a (non-free) iOS app that incorporates quite a few of the ideas that are behind
**The Incredible Proof Machine**. It came out of a Bachelor’s thesis of Tim Selier and covers propositional logic. - Euclid the game by Kasper Peulen is a nice game to play with geometric constructions.

Students with migration background supported by the START scholarship↩

Does anyone know the reference?↩

We almost named it “Proofcraft”, which would be a name our current Minecraft-wild youth would appreciate, but it is alreay taken by Gerwin Kleins blog. Also, the irony of a theorem prover being in-credible is worth something.↩

Luckily, two decades ago, Tobias Nipkow published a nice implementation of higher order pattern unification as ML code, which I transliterated to Haskell for this project.↩

## Quickest path to a local apt repository

As I’m writing this, DebConf 15 is coming to an end. I spend most of my time improving the situation of the Haskell Packages in Debian, by improving the tooling and upgrading our packages to match Stackage 3.0 and build against GHC 7.10. But that is mostly of special interest (see this mail for a partial summary), so I’d like to use this post to advertise a very small and simple package I just uploaded to Debian:

During one of the discussion here I noticed that it is rather tricky to make a locally built package available to `apt-get`

. The latest version in unstable allows one to install a debian package simply by running `apt-get install`

on it, but in some cases, e.g. when you want a convenient way to list all packages that you made available for local use, this is insufficient.

So the usual approach is to create a local apt repository with your packages. Which is non-trivial: You can use `dpkg-scanpackage`

, `apt-ftparchive`

or `reprepro`

. You need to create the directories, run the commands, add the repository to your local sources. You need to worry about signing it or setting the right options to make apt-get accept it without signing.

It is precisely this work that my new package `local-apt-repository`

automates for you: Once it is installed, you simply drop the `.deb`

file into `/srv/local-apt-repository/`

and after the next `apt-get update`

the package can be installed like any other package from the archive.

I chose to use the advanced features that `systemd`

provides – namely activation upon path changes – so works best with `systemd`

as the init system.

If you want to contribute, or test it before it passes the NEW queue, check out the git repository.

## Running circle-packing in the Browser, now using GHCJS

Quite a while ago, I wrote a small Haskell library called circle-packing to pack circles in a tight arrangement. Back then, I used the Haskell to JavaScript compiler fay to create a pretty online demo of that library, and shortly after, I create the identical demo using haste (another Haskell to JavaScript compiler).

The main competitor of these two compilers, and the most promising one, is GHCJS. Back then, it was too annoying to install. But after two years, things have changed, and it only takes a few simple commands to get GHCJS running, so I finally created the circle packing demo in a GHCJS variant.

Quick summary: Cabal integration is very good (like haste, but unline fay), interfacing JavaScript is nice and easy (like fay, but unlike haste), and a quick check seems to indicate that it is faster than either of these two. I should note that I did not update the other two demos, so they represent the state of fay and haste back then, respectively.

With GHCJS now available at my fingertips, maybe I will produce some more Haskell to be run in your browser. For example, I could port FrakView, a GUI program to render, expore and explain iterated function systems, from GTK to HTML.

## Tiptoi auf der GPN 15

Soeben findet in Karlsuhe die Gulaschprogrammiernacht statt, eine ein Chaos-Event mit Vorträgen, Workshops, allerlei Technikspielereien und, wie der Name sagt, auch Gulasch. Ich hab hier einen Vortrag zu (mal wieder) meinen Tiptoi-Basteleien gehalten. Entgegen meiner anfänglichen Sorgen war der Vortragssaal mit geschätzt 40 Leuten ganz ansehnlich gefüllt. In Anschluss habe ich noch einen Workshop angeboten, soll heißen, wer wollte macht seinen ersten Schritte mit dem tttool und ich helf über die ersten Hürden. Besonders gefreut hab ich mich über ein junges Mädchen, das ausführlich ihre Vorstellung von Rezepten mit Tiptoi-Unterstützung erläuterte.

Ansonsten hab ich von der GPN noch nicht viel mitbekommen, da ich gerade erst angekommen bin...

## ZuriHac 2015

Last weekend, I attended ZuriHac 2015, which was, as always, a pleasant event. I did not actually do a lot, besides some maintenance of Debian Haskell packages, but had some nice chats. It is always very motivating to hear that people read my blog, or that they found my talk (such as the Haskell Bytes talk at Galois) helpful.

My plan was to work on gipeda and perf.haskell.org. I did not do much until an hour before I had to leave, when Lennard Kolmodin came around and I showed him the software. He liked it so far, so we quickly set up an instance of gipeda for the “binary” library. It is not finished yet, as more benchmarks need to be extracted from the build log. That was motivating, and I got further ideas to implement during the train ride back. If only that had happened earlier during the weekend...