Skip to content

Latest commit

 

History

History
13 lines (8 loc) · 929 Bytes

README.md

File metadata and controls

13 lines (8 loc) · 929 Bytes
Raw

Red-black tree

This is a basic implementation of a red-black tree in F#, which is pretty close to being correct by construction. The invariants are imposed at the type level, so that if you have successfully constructed a tree, it is automatically a red-black tree (though we cannot help you get elements the right way round, so we can't guarantee that traversal is in sorted order; that is ensured by property-based and exhaustive testing).

Interesting points

  • An absolutely egregious use of units of measure to encode type-level naturals in such a way that we can unbox them away at runtime; thanks to Toby Shaw for this abomination.

Things to fix

  • Can we get some constraints at the type level to help us get the values assigned to the various nodes in the right order?
  • Can we get some kind of better proof that we are not violating the invariants? There's nothing to help us get the elevate calls right.