Wobbly types

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?

Cw

C-omega, Microsoft Research's experimental language featuring asynchronous concurrency (formerly, Polyphonic C#) and XML data types (Xen), is now available for download.

I think this is an interesting project. It was discussed here several times in the past.

I think that the integration of the new features with the core language is quite nice (e.g., XML types and the type system), so I suggest taking a look even if you are not particularly in favor of embedding XML in programming language.

The Cw home page includes links to relevant papers. And here's a LtU discussion of Xen and a discussion of Polyphonic C#.

The ongoing LtU discussion.

JDeveloperAOP

This project's goal is to provide integrated support for Aspect Orientated Programming in Oracle's JDeveloper IDE. Where possible we hope to make use of, and reuse code from, projects that have solved similar problems for other IDEs. The initial focus of the project is to integrate ADJT, the AspectJ design time environment, into JDeveloper.

It would be interesting to see whether projects such as this will help get AOP accepted by industry.

New CLR Language: Boo

This project is very interesting: a CLR-based language with Python-esque syntax, optional type declarations, open compilation pipeline, and some interesting ideas about generators and class attributes. There are some unique ideas about running a dynamic language atop the CLR, as well, like syntax to declare "duck" typing for individual objects, which lets you use them as dynamic proxies for COM objects, web services, etc.

It's definitely a bit green, but if even a significant fraction of the features discussed in the "manifesto" are there, it looks like an impressive effort, regardless.

Snowball: A language for stemming algorithms

Snowball is a small string processing language designed for creating stemming algorithms for use in Information Retrieval.

And here's a sample program.

I am not sure just how exciting this language is, but it has been a while since we discussed a DSL.

Crash-Only Software

(via Val Henson's weblog)

This paper (from HotOS IX) describes a software design approach which seems very close to the design techniques erlang tries to encourage.

ll-discuss's new home

For all those (like me) who didn't get the memo, I just found out that the seemingly defunct ll1-discuss mailing list has in fact found a new home at:

http://lists.csail.mit.edu/pipermail/ll-discuss/

An Interview with Donald Knuth

A very pleasant 1996 interview with Donald Knuth by Jack Woehr of Dr. Dobb's Journal.

Theoretical Pearl: Church numerals, twice!

Ralf Hinze. Theoretical Pearl: Church numerals, twice! Journal of Functional Programming, 2004. To appear.

This pearl explains Church numerals, twice. The first explanation links Church numerals to Peano numerals via the well-known encoding of data types in the polymorphic LC. This view suggests that Church numerals are folds in disguise. The second explanation, which is more elaborate, but also more insightful, derives Church numerals from first principles, that is, from an algebraic specification of addition and multiplication. Additionally, we illustrate the use of the parametricity theorem by proving exponentiation as reverse application correct.

A simple concept is used to demonstrate several interesting and useful techniques.

Functional programming in Java

(Link)

Vadim Nasardinov pointed out this article, which although pitched at an introductory level, provides a reasonably thorough overview of functional programming possibilities in Java. It focuses on the use of closures and higher-order functions, via Java's anonymous inner classes, and works its way up to "using closures to implement business rules" as one of its concrete examples.

Perhaps a little too introductory for LtU, but articles like this can be a useful starting point when talking to Java programmers who've had little or no previous exposure to FP, or who need some hints about useful ways to apply FP concepts in Java. Using anonymous inner classes to implement e.g. GUI event listeners in Java is common practice, but often, more advanced and useful possibilities are overlooked.