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

Browse archivesActive forum topics
New forum topics 
Recent comments
14 hours 17 min ago
18 hours 24 min ago
19 hours 15 min ago
19 hours 40 min ago
2 days 4 hours ago
2 days 5 hours ago
2 days 5 hours ago
2 days 5 hours ago
2 days 7 hours ago
2 days 15 hours ago