Introduction
Dependent types, and the idea of baking both algorithmic and business constraints into the type system are very exciting to me. However, beyond a few toy examples of Peano arithmetic and vectors, I haven't found a lot of examples online. So in the spirit of scratching my own itch, I am going to working through implementing a left-leaning red-black tree, capturing as many of the constraints as possible in the type system.A warning at the outset, I am relatively new to Haskell and very new to dependent types, so I welcome any feedback on both my Haskell, if it is not idiomatic, my use of dependent types and my choice of library dependencies. This series will be based entirely on GHC, and I will make liberal use of GHC extensions.
Find my Github repository at:
https://github.com/farrellm/dependent-rbtree
Dependencies
Note that GHC does have type-level natural numbers built in1. However, in my experimentation, these seem not to be useful for more complex use cases. Rather I will be using the following libraries:
- singletons - Seems to be the de factor standard for dependent types in GHC, I depend on it transitively
- type-natural - A powerful library for type level natural numbers implemented in with the singletons library
Also, I will be using stack, rather than cabal, to manage the project. At the moment, stack seems to be a saner tool for managing Hackage dependencies.
Overview
Red-black trees have several defining properties2:
- Binary search tree
- Alternating red-black properties
- Consistent black-height
Left-leaning red-black trees add:
- Require that all 3-nodes lean left.
Property 1 is beyond the scope of this blog; at some future time I may attempt to port this to Idris, at which time I will attempt 1.
Property 2 can be easily captured using ADTs.
Property 3 is my primary target with dependent types.
Property 4 I haven't thought about enough yet :-)
Property 3 is my primary target with dependent types.
Property 4 I haven't thought about enough yet :-)
No comments:
Post a Comment