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)) (fib (- n 2)))])))
This program defines the same program using Typed Scheme.
(module fib (planet "typed-scheme.ss" ("plt" "typed-scheme.plt")
)
(define: (fib [n : number]) : number
(cond [(= 0 n) 1]
[(= 1 n) 1]
[else (+ (fib (- n 1)) (fib (- n 2)))])))
There are three differences between these programs:
The Language: mzscheme
has been replaced in the
language position by
.(planet "typed-scheme.ss"
("plt" "typed-scheme.plt")
)
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" ("plt" "typed-scheme.plt")
)
(define: (fib [n : number]) : number
(let: ([base? : boolean (or (= 0 n) (= 1 n))])
(if base? 1
(+ (fib (- n 1)) (fib (- 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" ("plt" "typed-scheme.plt")
)
(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" ("plt" "typed-scheme.plt")
)
(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" ("plt" "typed-scheme.plt")
)
(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" ("plt" "typed-scheme.plt")
)
(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
.
1 Changes
to uses of require
may also be necessary — these are
described later.