Putting curry-howard to work
Tim Sheard · 2005
Abstract The Curry-Howard isomorphism states that types are propositionsand that programs are proofs. This allows programmers to state and enforce invariants of programs by using types. Unfortunately,the type systems of today's functional languages cannot directly express interesting properties of programs. To alleviate this prob-lem, we propose the addition of three new features to functional programming languages such as Haskell: Generalized AlgebraicDatatypes, Extensible Kind Systems, and the generation, propagation, and discharging of Static Propositions. These three new fea-tures are backward compatible with existing features, and combine to enable a new programming paradigm for functional program-mers. This paradigm makes it possible to state and enforce interesting properties of programs using the type system, and it does this inmanner that leaves intact the functional programming style, known and loved by functional programmers everywhere. Categories and Subject Descriptors D.3 [Software]: Program-ming Languages