# Projects

### Demo: Image Compression with SVD

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

### Operational Transformation

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

### quantities

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.

idris api-design

### diagrams-rubiks-cube

This library draws Rubik's Cubes using `diagrams`

.
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

### Purely Functional Data Structures in Idris

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.

idris algorithms

### uni-spicker

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

### Curry Club Augsburg

I designed the logo and website for the local Haskell/FP user group which I have co-founded.

webdesign hakyll

### Halma

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!

haskell

# Open Source Contributions

### reroute

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

### Timsort

I contributed an implementation of my favorite sorting algorithm to `vector-algorithms`

. The great thing about Timsort is ~~its name~~ that it is very fast (meaning linear time) on data that is already (partially) sorted.

haskell algorithms

### engine-io

This Haskell library by Oliver Charles provides the server component for engine-io, a protocol providing a socket-like communication channel between web clients and servers.
I wrote the `engine-io-yesod`

backend.
I'm also a co-maintainer of the library.

haskell

### lightyear

This parser combinator library is the Idris equivalent to `parsec`

.
I've converted it to continuation-passing style, which solved a stack overflow problem, and contributed a JSON parser as an example.

idris algorithms