Lambda the Ultimate

I am trying to build a simple DSL in scheme. I would like this DSL to use type inference to constrain s-expressions to only those that are provably type correct. My type scheme is fairly simple. I would like to have the following basic polymorphic types (at least for starters. This will likely expand later):

datum
  number
    real
      int
  char
  bool

In addition, I would like to support functions (all curried to a single param), lists and intersections of types, so that types like (-> int char) and (intersection (list-of int) char) can be supported. Strings will be lists of char for my DSL.

I know the way to do this is to use a type unification algorithm. Unfortunately, all the docs I can find on this subject seem to be very much research oriented and way over my head since I do not grasp the basic concepts here. I am wondering if anyone has some pointers to some good type inference tutorial level stuff that I might be able to get a good grasp of the basic principles and algorithm from.

At the bottom of the comment input form, <quote> is mentioned as an allowed tag. Is it just my setup, or does it not work? I don't seem to see quotation marks nor a change of appearance of the enclosing text. Here's an example: The quick brown fox jumps over the lazy dog.

The Derivative of a Regular Type is its Type of One-Hole Contexts by Conor McBride was mentioned on LtU several times.

If you enjoyed it, try a new paper by the same author:
Clowns to the left of me, jokers to the right (Dissecting Data Structures).

More generic programming, more parallels between data types and calculus, more fun.

As usual for Conor's paper, it's short and full of (sometimes obscure) humor. Beware of typos, though.

Walter Bright's D programming language 1.0 was released today!

A sampling of its many great features:

Garbage collection
Scope expressions
Lazy expressions
Auto-type inference
Built in arrays/strings and associative arrays.
templates and mixins
Design by contract
RAII

http://www.digitalmars.com/d/changelog.html
http://ftp.digitalmars.com/dmd.1.00.zip

Cheers.