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  34177 reads

Browse archivesActive forum topics 
Recent comments
1 hour 42 min ago
2 hours 10 min ago
8 hours 7 min ago
8 hours 23 min ago
18 hours 6 min ago
18 hours 21 min ago
18 hours 41 min ago
21 hours 43 min ago
21 hours 55 min ago
1 day 9 hours ago