Making illegal state unrepresentable in Idris Introduction A few years ago, Amos (AKA fasterthanlime) wrote a really great article entitled Aiming for correctness with types. It's a lengthy post, but at heart it was about how, by more faithfully modeling our world at the type level, we can avoid a great number of runtime bugs & errors (a topic near to my heart). He used as a running example the problem of building an authenticating proxy for a web service. In particular, he dug in to modeling HT...