Dependent types are a way of proving facts about your program at compile time. One interesting use case of dependent types, which I've discovered recently, is ensuring consistency in a sharded database system. Sharding is a database practice where different pieces of data are stored in different physical databases ...