## User login## Navigation |
## Type Theory## Constraint-based type inference for guarded algebraic data typesConstraint-based type inference for guarded algebraic data types
By Paul Snively at 2006-02-07 15:16 | Functional | Implementation | Type Theory | login or register to post comments | other blogs | 4720 reads
## Inverse typechecker and theorem proving in intuitionistic and classical logicsAnother cool demonstration from Oleg:
By Ehud Lamm at 2006-02-05 09:09 | Fun | Lambda Calculus | Type Theory | 4 comments | other blogs | 7500 reads
## Exceptional syntax
A nice paper apropos of tail calls and exceptions:
Nick Benton and Andrew Kennedy. 2001. Exceptional syntax. Journal of Functional Programming 11(4): 395-410. By Chung-chieh Shan at 2005-12-22 17:12 | Functional | Type Theory | 16 comments | other blogs | 40561 reads
## Module Mania: A Type-Safe, Separately Compiled, Extensible InterpreterModule Mania: A Type-Safe, Separately Compiled, Extensible Interpreter
This is an excellent example of how the ML module language doesn't merely provide encapsulation but also strictly adds expressive power. It also demonstrates how a dynamic language (Lua) can be embedded in the statically-typed context of ML. Finally, it demonstrates that none of this need come at the expense of separate compilation or extensibility. Norman Ramsey's work is always highly recommended. By Paul Snively at 2005-12-07 14:58 | DSL | Functional | General | Implementation | Semantics | Theory | Type Theory | login or register to post comments | other blogs | 7044 reads
## ClassicJava in PLT Redex
This might be interesting to folks curious about how to formalize a real language, or about how PLT Redex works in practice. By Paul Snively at 2005-12-07 14:51 | General | Implementation | Semantics | Theory | Type Theory | login or register to post comments | other blogs | 5762 reads
## Generalized Algebraic Data Types and Object-Oriented Programming
Generalized Algebraic Data Types and Object-Oriented Programming. Andrew Kennedy and Claudio Russo. OOPSLA, October 2005, San Diego, California.
Generalized algebraic data types (GADTs) have received much attention recently in the functional programming community. They generalize the type-parameterized datatypes of ML and Haskell by permitting constructors to produce different type-instantiations of the same datatype. GADTs have a number of applications, including strongly-typed evaluators, generic pretty-printing, generic traversals and queries, and typed LR parsing. We show that existing object-oriented programming languages such as Java and C# can express GADT definitions, and a large class of GADT-manipulating programs, through the use of generics, subclassing, and virtual dispatch. However, some programs can be written only through the use of redundant run-time casts. We propose a generalization of the type constraint mechanisms of C# and Java to avoid the need for such casts, present a Visitor pattern for GADTs, and describe a switch construct as an alternative to virtual dispatch on datatypes. We formalize both extensions and prove a type soundness result. I've been waiting for awhile for this paper to be available online. This paper is, of course, related to the other items posted here about GADTs. The examples in the introduction might be somewhat relevant to the recent discussion about the static versus dynamic features of Java, and its type system. By Ehud Lamm at 2005-11-24 20:47 | OOP | Software Engineering | Type Theory | 7 comments | other blogs | 44266 reads
## What good is Strong Normalization in Programming Languages?There's a neat thread about strong normalization happening on The Types Forum.
Termination is good:
Termination is
Termination is good and with fixpoints is turing complete?
Terminating reductions allows exhaustive applications of optimizations:
Rene Vestergaard also gave a link to a 2004 discussion of strong normalization on the rewriting list. By shapr at 2005-11-17 12:31 | Implementation | Lambda Calculus | Theory | Type Theory | 15 comments | other blogs | 7751 reads
## Extensible Records With Scoped Labels
Extensible Records With Scoped Labels
Daan Leijen Records provide a safe and flexible way to construct data structures. We describe a natural approach to typing polymorphic and extensible records that is simple, easy to use in practice, and straightforward to implement. A novel aspect of this work is that records can contain duplicate labels, effectively introducing a form of scoping over the labels. Furthermore, it is a fully orthogonal extension to existing type systems and programming languages...Last time one of Daan's papers was mentioned, there was a very positive response (after Frank reminded us a couple of times). This is equally good: clever, elegant, and clearly presented. (Between this and the Sheard paper, it's a good week for practical type systems...) By Matt Hellige at 2005-11-15 16:29 | Implementation | Type Theory | 9 comments | other blogs | 12830 reads
## 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 :) ## Just What is it that Makes Martin-Lof's Type Theory so Different, so Appealing?Martin-LÃ¶f's Type Theory (M-LTT) was developed by Per Martin-LÃ¶f in the early 1970s, as a constructive foundation for mathematics. The theory is clear and simple. Because of this it has been used for everything from program derivation to handling donkey sentences. Yet another propositions-as-types tutorial. It seems pretty easy to follow, and it is quite short (16 pages). P.S Why all the theory on LtU these days? Because the editors who keep posting are into theory. The other editors should be nudged to start posting cool hands-on stuff... |
## Browse archives## Active forum topics |

## Recent comments

3 days 8 hours ago

4 days 8 hours ago

4 days 10 hours ago

4 days 10 hours ago

5 days 16 hours ago

5 days 17 hours ago

6 days 11 hours ago

6 days 13 hours ago

6 days 13 hours ago

1 week 5 hours ago