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

Browse archivesActive forum topicsNew forum topics

Recent comments
4 min 32 sec ago
28 min 58 sec ago
31 min 7 sec ago
2 hours 23 min ago
4 hours 41 min ago
8 hours 35 min ago
10 hours 38 min ago
16 hours 48 min ago
17 hours 31 min ago
19 hours 14 min ago