Home

Generalized Algebraic Data Types and Object-Oriented Programming

Generalized Algebraic Data Types and Object-Oriented 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 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.

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 2005-11-24 20:47 | OOP | Software Engineering | Type Theory | other blogs | 63804 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

It's always great to see rece

It's always great to see recent research advances from Haskell and elsewhere make their way into mainstream languages like this.

C# generic constraints have always seemed somewhat strange in their operation. How does the typechecker work, exactly? When you're typechecking an expression in a context, do you go off and search all of the constraints visible to that context in order to find a match?

In implementing these things elsewhere, it has always seemed more convenient to introduce intersection types and union types and require explicit binding of variables to them, to avoid the go-search-the-environment-for-constraints voodoo. You really want typechecking to be context-free, in the sense that grammars are context-free: a term should have an interpretation independent of the context in which it exists.

By Tim Sweeney at Thu, 2005-11-24 21:47 | login or register to post comments

You beat me!

I was going to post this paper last week, but I felt like I'd been posting too much, so I decided to wait... Obviously that was a mistake...

Actually, I stumbled across the abstract when I heard that the next version of Scala will have GADTs. Martin has been quiet about it, so I was trying to get an idea of what that might look like.

It's a good paper, and it's always interesting to see how the same idioms are expressed in OO vs. functional styles. I feel pretty comfortable with the OO code, and in some cases find it preferable, but I admit that with the full machinery of generics, I'm starting to find it pretty hard to read. In this paper, for example, I know what code to expect in each of the examples, but it still takes a fair bit of effort to verify that it's really what I expected. I don't recall having that problem with the wobbly types paper, for instance.

I think Anton's comment about Lichtenstein was spot on. When I step back a bit, the C# examples here look flexible and elegant, but when I get too close, I start to feel a little dizzy.

All that aside, these are really cool features, and they solve some long-standing problems in a really satisfying way (just like GADTs everywhere). I look forward to actually using this stuff, and I really agree with Tim that it's nice to see new features "trickling down"...

By Matt Hellige at Fri, 2005-11-25 01:55 | login or register to post comments

What became of GADTs in Scala?

Sorry to resurrect a long-dead thread, but this discussion is linked from wp GADT, so I thought I would save others the time I just spent tracking this down.

IIUC, Scala did indeed get GADTs; we call them "case classes." Please feel free to correct me if I'm wrong.

By Alex Cruise at Wed, 2008-10-22 22:22 | login or register to post comments

Indeed

The paper mentioned in this article has an example expression GADT and its corresponding evaluator in GHC Haskell. A fairly direct translation to Scala looks like 

sealed abstract class Exp[T]
case class Lit(i : Int) extends Exp[Int]
case class Plus(e1 : Exp[Int], e2 : Exp[Int]) extends Exp[Int]
case class Equals(e1 : Exp[Int], e2 : Exp[Int]) extends Exp[Boolean]
case class Cond(e1 : Exp[Boolean], e2 : Exp[Int], e3 : Exp[Int]) extends Exp[Int]
case class Tuple[A,B](e1 : Exp[A], e2 : Exp[B]) extends Exp[(A,B)]
case class Fst[A](e : Exp[(A,_)]) extends Exp[A]
case class Snd[B](e : Exp[(_, B)]) extends Exp[B]

def eval[T](exp : Exp[T]) : T = exp match {
  case Lit(i) => i
  case Plus(e1, e2) => eval(e1) + eval(e2)
  case Equals(e1, e2) => eval(e1) == eval(e2)
  case Cond(e1, e2, e3) => if(eval(e1)) eval(e2) else eval(e3)
  case Tuple(e1, e2) => (eval(e1), eval(e2))
  case Fst(e) => eval(e)._1
  case Snd(e) => eval(e)._2 
}

By James Iry at Wed, 2008-10-22 23:20 | login or register to post comments

Come on, guys!

I've been really, really, really busy...

But I'm really disappointed that this didn't get more attention, especially from the professional Java/C# programmers. Like I said, I'm really excited about some of these features becoming available to us working programmers, but most discussion about Java/C# these days seems to revolve around whether they're getting too sophisticated...

Should I assume that the silence means that most of the Java people just don't care about this stuff, or think it's just more unnecessary complexity? Or is it just not a big deal?

Did anybody around here go to OOPSLA? Was this paper well-received?

By Matt Hellige at Mon, 2005-12-12 00:02 | login or register to post comments

But I'm really disappointed t

But I'm really disappointed that this didn't get more attention

I second that.

By Ehud Lamm at Mon, 2005-12-12 11:03 | login or register to post comments

well,

i think maybe i (also) learned that GADTs in regular ML aren't so possible, at least, from what they said. dunno about O'Caml.

By raould at Fri, 2008-10-24 22:08 | login or register to post comments