User loginNavigation 
Generalized Algebraic Data Types and ObjectOriented Programming
Generalized Algebraic Data Types and ObjectOriented 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 typeparameterized datatypes of ML and Haskell by permitting constructors to produce different typeinstantiations of the same datatype. GADTs have a number of applications, including stronglytyped evaluators, generic prettyprinting, generic traversals and queries, and typed LR parsing. We show that existing objectoriented programming languages such as Java and C# can express GADT definitions, and a large class of GADTmanipulating programs, through the use of generics, subclassing, and virtual dispatch. However, some programs can be written only through the use of redundant runtime 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 20051124 20:47  OOP  Software Engineering  Type Theory  other blogs  40527 reads

Browse archivesActive forum topics 
Recent comments
1 hour 12 min ago
2 hours 25 min ago
2 hours 36 min ago
2 hours 50 min ago
3 hours 18 min ago
12 hours 53 min ago
16 hours 15 min ago
1 day 13 hours ago
3 days 11 hours ago
3 days 11 hours ago