Starting with Typed Scheme

If you already know PLT Scheme, or even some other Scheme, it should be easy to start using Typed Scheme.

The following program defines the Fibonnaci function in PLT Scheme:

(module fib mzscheme (define (fib n) (cond [(= 0 n) 1] [(= 1 n) 1] [else (+ (fib (- n 1) (- n 2)))])))

This program defines the same program using Typed Scheme.

`(module fib ``(planet ``typed-scheme.ss'' (``samth'' ``typed-scheme.plt'' 1))`

(define: (fib [n : number]) : number
(cond [(= 0 n) 1]
[(= 1 n) 1]
[else (+ (fib (- n 1) (- n 2)))])))

There are three differences between these programs:

**The Language:**`mzscheme`

has been replaced in the language position by

.`(planet ``typed-scheme.ss'' (``samth'' ``typed-scheme.plt'' 1))`

**The Binding Form:**`define`

has been replaced by`define:`

as the top-level definition form.**The Type Annotations:**Both the argument`n`

and the result (appearing after the arguments) have been annotated with types, in this case`number`

.

In general, these are most of the changes that have to be made to a PLT Scheme
program to transform it into a Typed Scheme program.^{1}

Other typed binding forms are also available. For example, we could have rewritten our fibonacci program as follows:

`(module fib ``(planet ``typed-scheme.ss'' (``samth'' ``typed-scheme.plt'' 1))`

(define: (fib [n : number]) : number
(let: ([base? : boolean (or (= 0 n) (= 1 n))])
(if base? 1
(+ (fib (- n 1) (- n 2)))))))

This program uses the `let:`

binding form, which, like
`define:`

, allows types to be provided, as well as the
`boolean`

type.

We can also define mutually-recursive functions:

`(module even-odd ``(planet ``typed-scheme.ss'' (``samth'' ``typed-scheme.plt'' 1))`

(define: (my-odd? [n : number]) : boolean
(if (= 0 n) #f
(my-even? (- n 1))))
(define: (my-even? [n : number]) : boolean
(if (= 0 n) #t
(my-odd? (- n 1))))
(display (my-even? 12)))

As expected, this program prints `#t`

.

If our program requires anything more than atomic data, we must define
new datatypes. In Typed Scheme, structures can be defined, similarly
to PLT Scheme structures. The following program defines a date
structure and a function that formats a date as a string, using PLT
Scheme’s built-in `format`

function.

`(module date ``(planet ``typed-scheme.ss'' (``samth'' ``typed-scheme.plt'' 1))`

(define-typed-struct my-date ([day : number] [month : str] [year : number]))
(define: (format-date [d : my-date]) : str
(format "Today is day ~a of ~a in the year ~a" (my-date-day d) (my-date-month d) (my-date-year d)))
(display (format-date (make-my-date 28 "November" 2006)))

Here we see the new built-in type `str`

as well as a definition
of the new user-defined type `my-date`

. To define
`my-date`

, we provide all the information usually found in a
`define-struct`

, but added type annotations to the fields.
Then we can use the functions that this declaration creates, just as
we would have with `define-struct`

.

Many data structures involve multiple variants. In Typed Scheme, we
represent these using *union types*, written `(U t1 t2 ...)`

`(module tree ``(planet ``typed-scheme.ss'' (``samth'' ``typed-scheme.plt'' 1))`

(define-typed-struct leaf ([val : number]))
(define-typed-struct node ([left : (U node leaf)] [right : (U node leaf)]))
(define: (tree-height [t : (U node leaf)]) : number
(cond [(leaf? t) 1]
[else (max (tree-height (node-left t))
(tree-height (node-right t)))]))
(define: (tree-sum [t : (U node leaf)]) : number
(cond [(leaf? t) (leaf-val t)]
[else (+ (tree-sum (node-left t))
(tree-sum (node-right t)))])))

In this module, we have defined two new datatypes: `leaf`

and
`node`

. We’ve also used the type `(U node leaf)`

,
which represents a binary tree of numbers. In essence, we are saying
that the `tree-height`

function accepts either a `node`

or a `leaf`

and produces a number.

In order to calculate interesting facts about trees, we have to take
them apart and get at their contents. But since accessors such as
`node-left`

require a `node`

as input, not a
`(U node leaf)`

, we have to determine which kind of input we
were passed.

For this purpose, we use the predicates that come with each defined
structure. For example, the `leaf?`

predicate distinguishes
`leaf`

s from all other Typed Scheme values. Therefore, in the
first branch of the `cond`

clause in `tree-sum`

, we know
that `t`

is a `leaf`

, and therefore we can get its value
with the `leaf-val`

function.

In the else clauses of both functions, we know that `t`

is not
a `leaf`

, and since the type of `t`

was ```
(U node
leaf)
```

by process of elimination we can determine that `t`

must
be a `node`

. Therefore, we can use accessors such as
`node-left`

and `node-right`

with `t`

as input.

When a complex type is used repeatedly in a program, it can be helpful
to give it a short name. In Typed Scheme, this can be done with *type aliases*. For example, we could have used a type alias to
represent our tree datatype from the previous section.

`(module tree ``(planet ``typed-scheme.ss'' (``samth'' ``typed-scheme.plt'' 1))`

(define-typed-struct leaf ([val : number]))
(define-typed-struct node ([left : (U node leaf)] [right : (U node leaf)]))
(define-type-alias tree (U node leaf))
(define: (tree-height [t : tree]) : number
(cond [(leaf? t) 1]
[else (max (tree-height (node-left t))
(tree-height (node-right t)))]))
(define: (tree-sum [t : tree]) : number
(cond [(leaf? t) (leaf-val t)]
[else (+ (tree-sum (node-left t))
(tree-sum (node-right t)))])))

The defintion `(define-type-alias tree (U node leaf))`

creates
the type alias `tree`

, which is just another name for the type
`(U node leaf)`

. We can then use this type in subsequent
definitions such as `tree-sum`

.