I have met with claims that the static typing is useless as it is not mathematical proof (OK – for those knowing the discussion – I exaggerated a lot). However to large extend the static typing is prove of some sort and depending on the code it might be a prove of even quite strong properties.

As chosen field I tried to use LLRB trees – I have implemented them quite long time ago and I’ve run into problems that violated the pre and post conditions. Even when problem was discovered it took some time to find out the underlaying problems (my inexperience didn’t helped probably either)

I’ve tried to reimplement the code in GHC Haskell with following rules:

- Using only ‘safe’ extensions
- Making all functions total and without use of
`undefined`

or `error`

- Ensuring that all properties of tree are preserved

Unfortunately this was my first time I used some of the concepts (like Zipper) so the implementation and description might be not the best (comments and corrections welcome).

Continue reading →