User loginNavigation |
Putting Curry-Howard to Work
via LtU forums:
The Curry-Howard isomorphism states that types are propositions and 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 problem, we propose the addition of three new features to functional programming languages such as Haskell: Generalized Algebraic Datatypes, Extensible Kind Systems, and the generation, propagation, and discharging of Static Propositions. These three new features are backward compatible with existing features, and combine to enable a new programming paradigm for functional programmers. This paradigm makes it possible to state and enforce interesting properties of programs using the type system, and it does this in manner that leaves intact the functional programming style, known and loved by functional programmers everywhere.The paper is short and reasonably easy to read, also the examples are very realistic - check section 13 as a starter. Getting half through the paper made we willing to play with implementation, getting to the last page made my hands itching to implement my own PL with a similar type system. You are warned :) |
Browse archives
Active forum topics |
Recent comments
20 weeks 4 days ago
20 weeks 4 days ago
20 weeks 4 days ago
42 weeks 5 days ago
47 weeks 21 hours ago
48 weeks 5 days ago
48 weeks 5 days ago
51 weeks 2 days ago
1 year 3 weeks ago
1 year 3 weeks ago