08-16-2017, 09:08 PM
This article is presented by:
Andrew Kennedy
Claudio V. Russo
Generalized Algebraic Data Types
and ObjectOriented
Programming
and ObjectOriented
Programming
ABSTRACT
Generalized algebraic data types (GADTs) have received much attention recently in the functional programming com- munity. They generalize the (type) parameterized algebraic datatypes (PADTs) of ML and Haskell by permitting value constructors to return speci_c, rather than parametric, type- instantiations of their own 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 program- ming languages such as Java and C] can express GADT de_- nitions, and a large class of GADT-manipulating programs, through the use of generics, subclassing, and virtual dis- patch. However, some programs can be written only through the use of redundant runtime casts. Moreover, instantiation- speci_c, yet safe, operations on ordinary PADTs only admit indirect cast-free implementations, via higher-order encod- ings. We propose a generalization of the type constraint mechanisms of C] and Java to both avoid the need for casts in GADT programs and higher-order contortions in PADT programs; we present a Visitor pattern for GADTs, and de- scribe a re_ned switch construct as an alternative to virtual dispatch on datatypes. We formalize both extensions and prove type soundness.
INTRODUCTION
Consider implementing a little language using an object- oriented programming language such as Java or C]. Ab- stract syntax trees in the language would typically be repre- sented using an abstract class of expressions, with a concrete subclass for each node type. An interpreter for the language can be implemented by an abstract evaluator' method in the expression class, overridden for each node type. This is an instance of the Interpreter design pattern [6]. For example, take a language of integer, boolean and bi- nary tuple expressions: exp ::= con j exp + exp j exp - exp j exp == exp j exp && exp j exp exp j exp ? exp : exp j (exp; exp) j fst(exp) j snd(exp) C] code to implement this abstract syntax and its interpreter is shown in Figure 1. Note in particular two points. First, the result of the eval method has the universal type object, as expressions can evaluate to integers, booleans or pairs. Second, evaluation can fail due to type errors: adding an integer to a boolean throws InvalidCastException. Now suppose that we decide to add static type-checking to the language, for example checking that arithmetic op- erations are applied only to integer expressions and that conditional expressions take a boolean expression as condi- tion and two expressions of the same type for the branches. We could easily add a method that checks the type of an expression. This would then assure us that evaluation can- not fail with a type error; however, the runtime casts in the evaluator code (e.g. (int) in Plus.Eval) are still necessary to convince C] of the safety of the evaluator. Now consider building types into the AST representation itself, using the generics feature recently added to C] and Java to parameterize the Exp class by the type of expressions that it represents. Then we can: _ de_ne Exp<T> and its subclasses to represent expres- sions of type T that are type correct by construction; _ give Eval the result type T and guarantee absence of type errors during evaluation. Figure 2 lists C] code that does just this. Observe how the type parameter of Exp is re_ned in subclasses; moreover, this re_nement is reected in the signature and code of the overridden Eval methods. For example, Plus.Eval has re- sult type int and requires no runtime casts in its calls to e1.Eval() and e2.Eval(). Not only is this a clever use of static typing, it is also more e_cient than the dynamically typed version, particularly in an implementation that per- forms code specialization to avoid the cost of boxing integers and booleans
For more information about this article,please follow the link
http://research.microsoften-us/um/people/akenn/generics/gadtoop.pdf