In the .NET Socket API, if you call methods in the wrong order, the Socket class will throw an exception. Wouldn't it be better if it guided you into the pit of success at compile time? One pattern from the Gang of Four book holds the key to proving that prerequisites happen first.
You can compute how many degrees of freedom are in a problem. This tells you how many decisions you can make, or how many values it takes to describe the current state. Knowing this will tell you some interesting things about the solution to that problem.
Daan Leijen explores the balance between type constraints, which make it possible to prove interesting assertions about values, and generalizations, which make it easy to express types. Finding this balance is sometimes a hard problem, leading some to abandon statically typed languages for dynamically typed ones. In Extensible Records with Scoped Labels, Daan shows us how we can take on some of the power of dynamic typing -- extension -- without giving
