Depently typed my ass

Creating libraries for dependently typed languages is an interesting problem. I worked for a while on making a tree map (like Haskell's Data.Map) that took advantage of dependent types; for example, supplying proofs that a key either exists or does not in tree. There are oodles of things to compute and prove, it's not clear what a nice API would look like. For example, a proof that a key either exists or does not is a much larger data structure than a simple boolean true/false. I am really excited to see what these sorts of libraries will look like.

If the GNU kernel had been ready last spring, I'd not have bothered to
even start my project: the fact is that it wasn't and still isn't. Linux
wins heavily on points of being available now.

Install kentoo, entire /g/ populace