GADTs In EHC

Date: 2008-05-22

Time: 11:00

Room: BBL room 471

Speaker: Arie Middelkoop

Title: GADTs in EHC

Abstract

N.B. The presentation consists of two parts. A typical "Haskell" part about some language feature, and an "Object Oriented Programming" part where this language feature is used in the context of C#. This first part is what I am going to present at the Trends in Functional Programming symposium next week, so I'd appreciate feedback. The second part is based on an OOPSLA'05 paper by two people of Microsoft Research.

With Generalized Algebraic Data Types (GADTs) you are allowed to make more specific assumptions about types after having pattern matched against certain constructors. It is a popular extension of normal data types in a functional language like Haskell; it is typically used when embedding domain specific languages with typed abstract syntax.

We have an experimental implementation of GADTs in EHC, the Haskell compiler we develop here in Utrecht. During this talk, I explain how we implemented GADTs in EHC as a minor extension to the infrastructure we have for qualified types.

After this, you'll have an understanding of what GADTs are and how to add support for them to a compiler. Then we switch to C# and take a look at typed Abstract Syntax Trees in C# with generics. Then we will see that certain GADT-like concepts are needed to properly deal with these typed ASTs without having to resort to casts.