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

Browse archivesActive forum topicsNew forum topics

Recent comments
3 hours 55 min ago
5 hours 14 min ago
5 hours 36 min ago
9 hours 7 min ago
14 hours 59 min ago
15 hours 5 min ago
17 hours 32 sec ago
1 day 2 hours ago
1 day 22 hours ago
2 days 8 hours ago