Singular value decomposition is an important matrix factorisation. It can be used to approximate a matrix by a matrix of lower rank, which can be stored and processed more efficiently. This interactive webpage allows the user to compress images (which can be regarded as combination of three matrices, one for each color channel) using SVD and see how the quality of the compressed image depends on the number of singular values.
visualization math react
OT is the synchronization algorithm used in many real-time collaborative applications like Etherpad and Google Docs. It is based on a transform function for merging concurrent changes. I've implemented a family of OT libraries in several programming languages, wich include a transform function for text documents and client/server modules. I have also created an interactive visualization, which helps understanding OT.
haskell visualization algorithms d3
A library for type-safe physical computations in the dependently typed programming language Idris. It makes unit errors impossible by tagging each float that represents a physical measurement with its unit. A value can be converted from one unit to another unit provided that the units have the same quantity (e.g. area). To ensure this at compile time, units are indexed by their quantity. The library uses the observation that both units and quantities are a free abelian group and the existence of a natural group homomorphism φ : Units → Quantities.
This library draws Rubik's Cubes using
Given a start (or end state) and a series of steps to follow, it can produce images like the one on the right.
I used Edward Kmett's
lens library to succinctly express the calculation of the new facets after a rotation.
I used this library to generate the images for this solution guide.
haskell math writing
Implementations of various functional data structures from Okasaki's book and elsewhere in the dependently typed programming language Idris. Where possible, I tried to use size-indices. All implementations have been verified as total by the Idris compiler.
Cheat sheets which I'm writing to prepare for exams and as a reference for later. All together, they comprise over 150 pages of dense mathematics and computer science!
latex math writing
I designed the logo and website for the local Haskell/FP user group which I have co-founded.
I implemented the game rules and a simple
diagrams-based GUI for my favorite board game.
A friend of mine wrote a simple AI using search trees, which is actually quite hard to beat!
Open Source Contributions
This library implements the routing in the Spock Haskell web framework. It uses type-level lists to index routes by thy types of their parameters. I've implemented it together with Alexander Thiemann, the author of Spock, during HacBerlin2014. I've also written a tutorial on the new routing system for the Spock blog.
haskell api-design writing