Lambda the Ultimate

The January release of Franz's Allegro Common LISP 8.0 puts developers on notice that "exotic" programming tools, long relegated to research environments, are becoming more viable options for mainstream applications. LISP, PROLOG, genetic programming and neural nets are among the technologies increasingly ready for Web-facing roles.

I'll let you draw your own conclusions about this article...

A new release of Shriram Krishnamurthi's programming languages book is available.

Constraint-based type inference for guarded algebraic data types

Guarded algebraic data types subsume the concepts known in the literature as indexed types, guarded recursive datatype constructors, and first-class phantom types, and are closely related to inductive types. They have the distinguishing feature that, when typechecking a function defined by cases, every branch may be checked under different assumptions about the type variables in scope. This mechanism allows exploiting the presence of dynamic tests in the code to produce extra static type information.

We propose an extension of the constraint-based type system HM(X) with deep pattern matching, guarded algebraic data types, and polymorphic recursion. We prove that the type system is sound and that, provided recursive function definitions carry a type annotation, type inference may be reduced to constraint solving. Then, because solving arbitrary constraints is expensive, we further restrict the form of type annotations and prove that this allows producing so-called tractable constraints. Last, in the specific setting of equality, we explain how to solve tractable constraints.

To the best of our knowledge, this is the first generic and comprehensive account of type inference in the presence of guarded algebraic data types.

A constraint-based approach to guarded algebraic data types

We study HMG(X), an extension of the constraint-based type system HM(X) with deep pattern matching, polymorphic recursion, and guarded algebraic data types. Guarded algebraic data types subsume the concepts known in the literature as indexed types, guarded recursive datatype constructors, (first-class) phantom types, and equality qualified types, and are closely related to inductive types. Their characteristic property is to allow every branch of a case construct to be typechecked under different assumptions about the type variables in scope. We prove that HMG(X) is sound and that, provided recursive definitions carry a type annotation, type inference can be reduced to constraint solving. Constraint solving is decidable, at least for some instances of X, but prohibitively expensive. Effective type inference for guarded algebraic data types is left as an issue for future research.

GADTs are obviously currently a hot topic in functional programming research. Most of the papers focus only on the GADT mechanism (how type checking works etc.). The only example that one usually sees is the "typed evaluator".

I am not an expert on this topic, and I'd like to know more about how they would actually be useful in practical programming.

For example, I wonder how a parser would look like if it is impossible to construct "wrong" ASTs. Would type checking then effectively take place during parsing? How would a type error in the parsed program be detected and thrown?

What other interesting applications exist? In general, how do GADTs change the programming model?