Computational Theology Gilad Bracha's Sun Weblog

Pluggable Types

A few ideas on type systems have been proposed by people who commented on my last entry.

The way to handle these issues is through the notion of pluggable types. Briefly, the idea is that the language is dynamically typed, and various type systems/static analyses can be added as plug-ins.

I wrote a brief position paper on this for a workshop last year. My website contains a presentation on the topic as well.

I'll go over the basics here. Most people are familiar with two approaches to types in programming:

There are endless religious arguments over the merits of one approach or the other. These debates are often pointless, because the split between the mandatory and dynamic type religions is a false dichotomy.

An alternative is to view typechecking as an optional tool, like lint. Now, I define an optional type system very strictly. There are two requirements:

1. The dynamic semantics must not depend on the type system.

2. Type annotations are syntactically optional.

The first requirement is the really important one. The second requirement is obvious to many people, but in fact it's not that significant. People often get hung up on things like type inference to address (2), when in fact that is exactly the wrong thing to focus on.

A few optional type systems have been built, but less than you think. The definition above excludes quite a few efforts. I built such as a system for Smalltalk. Phil Wadler did some work on Erlang.

If your language doesn't depend on the type system, you can in principle have multiple type systems that can check different properties; you can evolve these systems independently, as tools. The type systems can be viewed as plug-ins, hence the notion of pluggable types.

At this point, all the good or bad type checking ideas anyone cares to come up with are up to them to implement. People would not need to appeal to the keepers of the language to consider their favorite idea.

How to actually do pluggable types in a clean way is still subject to some research. I'm sure it can be done with good IDE support.

Read the position paper if you're interested.

Posted at 01:56PM Sep 10, 2005 by gbracha in Java  |  Comments[10]