Duration: 1:01:37

1,092 views

2

Generalized algebraic data types (GADTs) have received much attention recently in the functional programming community. They extend the datatypes of Haskell with constructors that produce specialized instantiations of their datatype. GADTs have a number of applications, including strongly-typed evaluators, custom runtime-type descriptors, polytypic programming, and strongly-typed LR parsing. I`ll show that C# and Java can already 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 by resorting to run-time casts in C#. Worse still, these casts are unsafe in Java. Andrew Kennedy and I have proposed a generalization of the type constraint mechanism of C# (and Java) to avoid the need for such casts. Interestingly, our work both exposes and repairs a flaw in the design of C# and Java Generics. I`ll give an introduction to GADTs in Haskell and C#, reveal the flaw in Generics, outline our proposed extension to C#, and present expressivity results relating functional to object-oriented GADTs. I`ll sketch how a generalization of our solution complements our separate proposal for adding variant subtyping to C# Generics. The talk covers material from three papers (joint with Andrew) accepted at OOPSLA05, ECOOP06 and submitted to POPL07.