red-black-tree

a" is a sorted list of length "n" of values of type "a". "IsPermutation a b" is a proof that a is a permutation of b (returned from sort). Here's how you can define a type like SortedList: type SortedList n a = exists min. SortedList' min n a data SortedList' min n a where Empty : SortedList' min 0 a Cons : LessOrEq x y -> (x:a) -> SortedList' y n a -> SortedList' x (1+n) a SortedList thus embeds a proof alongside each element that it is less than or equal to the lower-bound of the remaining list (i.e: the next element). Type-checking this guarantees that `sort` does the right thing, modulo resource-use/performance (or termination, depending on your type checker). Resource use (bounding) can also be type-checked, but requires leveraging the type system even more. These guarantees aren't free -- you have to write the types for them, and you have to prove them by instantiating values of these types. But you can opt in or out of each of these guarantees -- leverage the type system as much as you want. With dynamic typing, you just don't have this tool at your disposal at all. No flexibility to guarantee anything. You're forced to opt out completely.

. Now we need one last piece before digging in to the core. This is the existence of Type-level Naturals. The idea is that, like Red and Black, we introduce two new distinct types, one basic and one parametric. data Zero = Zero data Succ a = Succ a which lets us write (very verbose) naturals like (Succ (Succ (Succ Zero))) == 3 and have the type reflect this exact value (Succ (Succ (Succ Zero))) :: (Succ (Succ (Succ Zero))) (Note this is a little weird, since we can also form the value (Succ 'a' :: Succ Char) which doesn't make much sense. More powerful dependently typed features help here.) Now consider just a branch in the tree, we form that with a simple data type data NodeH l r n a = NodeH (Node l n a) a (Node r n a) which tracks the left and right colors in its type using the l and r type parameters. It also guarantees the constraint that both the left and right child trees have the same black-height. So, if (black3 :: Node Black (Succ Zero) Char) then (NodeH black3 'a' black3 :: NodeH Black Black (Succ Zero) Char). And if (black2 :: Node Black Zero Char) then (NodeH black3 'a' black2) is a compile time type error. So with all these pieces, we can encode the Red/Black criteria directly into our Nodes. Remember already that if we have a Tree it must have the first Node be Black. We can now construct new Nodes in three ways, each of these ways being constrained so as to enforce the balance rules. data Node t n a where -- If we construct a Node with Nil, it forms a leaf. -- Not only are we not allowed to associate left and -- right branches (we don't get to give it a NodeH type), -- we're forced to set the numerical type parameter to Zero ~= 0. Nil :: Node Black Zero a -- If we construct a Node with BlackNode, we can pass a -- subtree with the NodeH parameter, but the type of node we -- get back is necessarily going to increase its height -- since (Succ n) is like (n + 1). BlackNode :: NodeH t0 t1 n a -> Node Black (Succ n) a -- Or we can construct a Red node. In this case, our black-height -- remains unchanged, but we can ONLY do so when we've got a NodeH -- branch with two black subNodes. RedNode :: NodeH Black Black n a -> Node Red n a So, it's a type error to construct a tree in this format which doesn't obey the Red/Black balance rules. Any transformations you write on the tree will be rejected by the compiler if they break the rules.

f null did not exist, and never use it to signify lack of a value. > I think Go occupies a good point along this spectrum, where I can write robust code without arguing with a compiler. When "arguing with a compiler", you're really being faced with bugs now rather than later, when the code is no longer in your head - or worse, in production. If the type checker rejects your program, it is almost certainly broken, and it is better to "argue with a compiler" than to just compile and get a runtime error later. Availability of engineers is a good point, though as a Haskeller, I know both companies seeking Haskell employees and Haskellers seeking employment (preferably in Haskell). Consider the flip-side of the engineers availability is the "Python paradox".

ating each other's invariants poorly. Those are the bugs I spend time on. If you had experience with advanced type systems -- your claims here would carry more weight. People who don't know advanced type systems tend to massively understate their assurance power. For example 2 different communicating services might use "session types" to verify that their protocol guarantees invariants. Or maybe the only type-checked programs are ones forced to reject invalid inputs that violate invariants. > I haven't spent any time at all with Haskell, really, but it seems like a poor trade off to have to learn a bunch and engineer things in a way that's more difficult in order to prevent the easiest bugs. They aren't the "easiest bugs" at all. For example, consider implementing a Red Black Tree. In Go, imagine you had a bug where you rotate the tree incorrectly, such that you end up with a tree of the wrong depth -- surely you would have considered this a "logic" bug. One of the harder bugs that you wouldn't expect to catch with a mere type system. In Haskell, I can write this (lines 27-37): https://github.com/yairchu/red-black-tree/blob/master/RedBla... to specify my red black tree, with type-level enforcement of all of the invariants of the tree. With just these 10 lines, I get a compile-time guarantee that the ~120 lines implementing the tree operations will never violate the tree's invariants. This logic bug simply cannot happen. Learning a bunch of techniques is a one-time investment. After that, you will build better software for the rest of your career. Debugging far fewer bugs for the rest of your career. How could you possibly reject this trade-off, unless you expect a very short programming career?

t program, at least from the invariants' perspective.