OBJECT-ORIENTED PROGRAMMING, SYSTEMS, LANGUAGES and APPLICATIONS
 
 
Program
 


Program (2mb PDF)

Explore
  Invited Speakers
  Onward!
  Panels
  Workshops
Discover
  Research Papers
  Student Research Comp.
  Posters
  Doctoral Symposium
  Educators' Symposium
  Wiki Symposium
  Dynamic Lang. Symp.
Understand
  Tutorials
  Essays
  Practitioner Reports
  Demonstrations
Create
  DesignFest
  Lightning Talks
  FlashBoF
  Instant Arts School Exp.
 
Other Events
 
Resort Map (364kb PDF)
 
Resort Map (JPG)

 

 
Basket
 

view, help

"Generalized Algebraic Data Types and Object-Oriented Programming"

 

 
Page
 

Printer-friendly

 
 
  > Research Papers > Type Types

 : Tuesday

Generalized Algebraic Data Types and Object-Oriented Programming

San Diego Room
Tuesday, 11:00, 30 minutes

 


 
7·8·9·10·11·12·13·14·15·16·17·18·19·20·21

Andrew Kennedy, Microsoft Research Ltd
Claudio Russo, Microsoft Research Ltd

Generalized algebraic data types (GADTs) have received much attention recently in the functional programming community. They generalize the type-parameterized datatypes of ML and Haskell by permitting constructors to produce different type-instantiations of the same datatype. GADTs have a number of applications, including strongly typed evaluators, generic pretty-printing, generic traversals and queries, and typed LR parsing. We show that existing object-oriented programming languages such as Java and C# can express GADT definitions, and a large class of GADT-manipulating programs, through the use of generics, subclassing, and virtual dispatch. However, some programs can be written only through the use of redundant run-time 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.

Keywords: generalised algebraic data types, patterns, generics, C#, Java, virtual methods, constraints, polymorphism, existential types

 
.