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.