Extending Typed Racket, Part 1

The Typed Racket team is pleased to announce a number of new additions to our system. We'll be writing a few blog posts about them, all of which you can read here.
This post begins with the core of the Typed Racket type system. The fundamental idea at the heart of Typed Racket is called occurrence typing. This is the technique that allows us to typecheck existing Racket programs without requiring rewrites. Here's a simple example:

(if (number? x) (add1 x) 0)

The typechecker can figure out from the use of number? that the second occurrence of x is always going to be a number. This simple form of occurrence typing is enough to take Typed Racket a long way. But because we want to be able to handle all the sophisticated reasoning that programmers are already using to write their Racket programs, we have been working on extending the system further.
The new design of our system is described in a paper, Logical Types for Untyped Languages, in the upcoming International Conference on Functional Programming. The introduction provides an overview that's acessible to any Racket programmer, but here's the key example:

(cond
  [(and (number? x) (string? y)) — 1 —]
  [(number? x)                   — 2 —]
  [else                          — 3 —])

In expression 1, we know that x is a number and y is a string. In 2, we know that x is a number and y is not a string, by the logical properties of and and cond. This form of logical reasoning is enabled by the new foundation of the system, and makes the entire system significantly more expressive.
All of these improvements are available in the current version of Racket.

Typed Scheme 2.0

Typed Scheme version 2.0 is now available from SVN.

One persistent limitation of Typed Scheme has been that while this expression works as expected:

(if (number? x) (add1 x) 7)

The simple transformation of making x a part of a structure breaks Typed Scheme's ability to reason about the code. So this expression doesn't typecheck:

(if (number? (car x)) (add1 (car x)) 7)

With the newest version of Typed Scheme, now available in SVN, both of these will now work. In general, Typed Scheme can now follow paths into arbitrary immutable structures, including pairs.

This is part of a more general reworking of underlying mechanisms of the Typed Scheme typechecker, which makes it both simpler and more flexible. I hope that it will be possible, sing this new foundation to add additional features that make more programs easy to express in Typed Scheme.

Of course, these changes mean that Typed Scheme may be more unstable, so if you notice any new bugs, please let us know.

Unfortunately, this won't be available in the upcoming 4.2 release, but it will be in the release after that.

If you have any questions or comments or feature requests for Typed Scheme, please let us know.

Call for Participation: Writing Typed Scheme wrapper modules

Typed Scheme is a language for writing PLT Scheme programs that are statically checked for type errors. Right now, Typed Scheme handles a large portion of the PLT Scheme language. However, to use Typed Scheme effectively, we need libraries that work with it. For this task, we're looking for help.

We'd like volunteers for writing wrapper modules that adapt untyped libraries to Typed Scheme. This task is very easy for the smallest libraries, but can be much more complicated for larger, complex libraries.

There's a preliminary guide for conversion here and a list of modules to adapt, and their current status is available here.

Questions about this project, and about developing with Typed Scheme in general, can be asked on plt-dev@list.cs.brown.edu , and questions or comments can be sent directly to me.

We hope to continue making Typed Scheme into a useful tool for PLT Scheme programmers.

Thanks,
Sam, Stevie, and Matthias

Looking for small Scheme scripts

As part of the Typed Scheme project, we are looking for small Scheme scripts that we can port from PLT Scheme to Typed Scheme. We would like to investigate if Typed Scheme is capable of checking idiomatic PLT Scheme code, as represented by scripts written by members of the PLT Scheme community.

Therefore, if you have a simple PLT Scheme program which handles a scripting/processing task, and you are willing to share it with us for the improvement of Typed Scheme, please let me know. Typed Scheme currently handles all of 'core' MzScheme, as well as many of the collections (the major exceptions are the class and unit systems).

In return, we will inform you of any bugs that we discover during the port.

More information about Typed Scheme is available from the webpage: http://www.ccs.neu.edu/~samth/typed-scheme.html