Lambda the Ultimate

A nice post from Oleg on the Haskell mailing list shows how to implement high order modules, and more specifically translucent applicative functors in idiomatic Haskell.

Thus different instantiations of the functor with respect to type-compatible arguments are type-compatible; and yet the functor hides the representation details behind the unbreakable abstraction barrier.

The work is inspired by (our own) Ken Shan's work that can be found here.

Oleg concludes,

The example illustrates that Haskell already has a higher-order module language integrated with the core language and with the module checking being a part of the regular typechecking.

Oleg posted this pertinent message on the Haskell mailing list. It's always nice to see cool examples such as this.

Having saiod that, I must also say that I agree with Conor McBride who wrote that anyone who would argue (and I'm not saying you do) that work to try to make more advanced type systems and stronger static guarantees more convenient and well-supported is not necessary because it happens to be possible to bang out this or that example in Haskell as it stands if you think about it hard enough, is adopting the position of the ostrich.

Making type systems more expressive is a worthy goal. You want them to remain decidable (i.e., static), of course. Can we at least agree on that? ;-)

TyPiCal is a type-based static analyzer for the pi-calculus. The current version of TyPiCal provides four kinds of program analyses or program transformations: lock-freedom analysis, deadlock-freedom analysis, useless-code elimination, and information flow analysis.

Type system is an ordinary type system extended so that channel types carry precise information about how each channel is used. This allows a type inferencer to obtain information about the behavior of a process.

Wobbly types: type inference for generalised algebraic data types

Simon Peyton Jones, Geoffrey Washburn, and Stephanie Weirich.
July 2004
Postscript

Generalised algebraic data types (GADTs), sometimes known as "guarded recursive data types" or "first-class phantom types", are a simple but powerful generalisation of the data types of Haskell and ML. Recent works have given compelling examples of the utility of GADTs, although type inference is known to be difficult.

It is time to pluck the fruit. Can GADTs be added to Haskell, without losing type inference, or requiring unacceptably heavy type annotations? Can this be done without completely rewriting the already-complex Haskell type-inference engine, and without complex interactions with (say) type classes? We answer these questions in the affirmative, giving a type system that explains just what type annotations are required, and a prototype implementation that implements it. Our main technical innovation is wobbly types, which express in a declarative way the uncertainty caused by the incremental nature of typical type-inference algorithms.

Edit: Made the title into a hyperlink, as the "Postscript" link could easily get lost in a sea of blue text...

Edit 2:Quoted the article with a plain-ol' <blockquote> instead. Better?

Constraint-Based Type Inference for Guarded Algebraic Data Types. Vincent Simonet and Francois Pottier.

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 typing assumptions. 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.

Seems rather interesting.