Typed Scheme

Typed Scheme is a Scheme-like language, with a type system that supports common Scheme programming idioms. Explicit type declarations are required – that is, there is no type inference. The language supports a number of features from previous work on type systems that make it easier to type Scheme programs, as well as a novel idea dubbed occurrence typing for case discrimination.

Typed Scheme is also designed to integrate with the rest of your PLT Scheme system. It is possible to convert a single module to Typed Scheme, while leaving the rest of the program unchanged. The typed module is protected from the untyped code base via automatically-synthesized contracts.

Further information on Typed Scheme is available from the homepage.

Installation

There is no need to specifically install Typed Scheme. Simply running one of the example programs described in this manual will automatically download and install the necessary software. However, it can also be installed from the MzScheme or DrScheme prompt with the following require statement:

  (require (planet "typed-scheme.ss" ("plt" "typed-scheme.plt" 2)))

In order to use the Typed Scheme language level in DrScheme, DrScheme must be restarted after installation.

1 Starting with Typed Scheme

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

1.1 A First Function

The following program defines the Fibonacci 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" 2))

(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 by (planet "typed-scheme.ss" ("plt" "typed-scheme.plt" 2)).

• 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.

Changes to uses of require may also be necessary - these are described later.

1.2 Adding more complexity

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

(module fib tlang

(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" 2))

(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.

1.3 Defining New Datatypes

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" 2))

(define-typed-struct my-date ([day : Number] [month : String] [year : Number]))

(define: (format-date [d : my-date]) : String

(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 String 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 using the define-typed-struct form. Then we can use the functions that this declaration creates, just as we would have with define-struct.

1.4 Recursive Datatypes and Unions

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" 2))

(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 leafs 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.

1.5 Giving Names to Types

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 tlang

(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.

2 Polymorphism

Virtually every Scheme program uses lists and sexpressions. Fortunately, Typed Scheme can handle these as well. A simple list processing program can be written like this:

(module add-list tlang

(define: (sum-list [l : (Listof Number)]) : Number

(cond [(null? l) 0]

[else (+ (car l) (sum-list (cdr l)))])))

This looks similar to our earlier programs – except for the type of l, which looks like a function application. In fact, it’s a use of the type constructor Listof, which takes another type as its input, here Number. We can use Listof to construct the type of any kind of list we might want.

We can define our own type constructors as well. For example, here is an analog of the Maybe type constructor from Haskell:

(module maybe "typed-lang.ss"

(define-typed-struct Nothing ())

(define-typed-struct (a) Just ([v : a]))

(define-type-alias (Maybe a) (U Nothing (Just a)))

(define: (find [v : Number] [l : (Listof Number)]) : (Maybe Number)

(cond [(null? l) (make-Nothing)]

[(= v (car l)) (make-Just v)]

[else (find v (cdr l))])))

The first define-typed-struct defines Nothing to be a structure with no contents.

The second definition

  (define-typed-struct (a) Just ([v : a]))

creates a parameterized type, Just, which is a structure with one element, whose type is that of the type argument to Just. Here the type parameters (only one, a, in this case) are written before the type name, and can be referred to in the types of the fields.

The type alias definiton

  (define-type-alias (Maybe a) (U Nothing (Just a)))

creates a parameterized alias – Maybe is a potential container for whatever type is supplied.

The find function takes a number v and list, and produces (make-Just v) when the number is found in the list, and (make-Nothing) otherwise. Therefore, it produces a (Maybe Number), just as the annotation specified.

3 Type Reference

Base Types

These types represent primitive Scheme data.

Number

Any number

Boolean

Either #t or #f

String

A string

Keyword

A PLT Scheme literal keyword

Symbol

A symbol

Any

Any value

Type Constructors

The following constructors are parameteric in their type arguments.

(Listof t)

Homogenous lists of t

(Vectorof t)

Homogenous vectors of t

(Option t)

Either t of #f

(Pair s t)

is the pair containing s as the car and t as the cdr

(dom ... -> rng)

is the type of functions from the (possibly-empty) sequence dom ... to the rng type.

(dom ... rst .. -> rng)

is the type of functions from the (possibly-empty) sequence dom ... to the rng type with an optional trailing sequence of rst type. Note: .. is a part of the syntax of these types.

(U t ...)

is the union of the types t ...

(case-lambda fun-ty ...)

is a function that behaves like all of the fun-tys. The fun-tys must all be function types constructed with ->.

(t t1 t2 ...)

is the instantiation of the parametric type t at types t1 t2 ...

(All (v ...) t)

is a parameterization of type t, with type variables v ...

(values t ...)

is the type of a sequence of multiple values, with types t .... This can only appear as the return type of a function.

v

where v is a number, boolean or string, is the singleton type containing only that value

i

where i is an identifier can be a reference to a type name or a type variable

(mu n t)

is a recursive type where n is bound to the recursive type in the body t

Other types cannot be written by the programmer, but are used internally and may appear in error messages.

(struct:n (t ...))

is the type of structures named n with field types t. There may be multiple such types with the same printed representation.

<n>

is the printed representation of a reference to the type variable n

4 Special Form Reference

Typed Scheme provides a variety of special forms above and beyond those in PLT Scheme. They are used for annotating variables with types, creating new types, and annotating expressions.

4.1 Binding Forms

loop, f, a, and v are names, t is a type. e is an expression and body is a block.

(define: (f [v : t] ...) : t body)

(define: v : t e)

(pdefine: (a ...) (f [v : t] ...) : t body)

(let: ([v : t e] ...) body)

(let: loop : t0 ([v : t e] ...) body)

where t0 is the type of the result of loop (and thus the result of the entire expression).

(letrec: ([v : t e] ...) body)

(let*: ([v : t e] ...) body)

(lambda: ([v : t] ...) body)

(lambda: ([v : t] ...    v : t)  body)

(plambda: (a ...) ([v : t] ...) body)

(plambda: (a ...) ([v : t] ...    v : t)  body)

(case-lambda: [formals body] ...)

where formals is like the second element of a lambda:

(pcase-lambda: (a ...) [formals body] ...)

where formals is like the third element of a plambda:

4.2 Structure Definitions

(define-typed-struct name ([f : t] ...))

(define-typed-struct (name parent) ([f : t] ...))

(define-typed-struct (v ...) name ([f : t] ...))

(define-typed-struct (v ...) (name parent) ([f : t] ...))

(define-type name [variant (f t) ...] ...)

4.3 Type Aliases

(define-type-alias name t)

(define-type-alias (name v ...) t)

4.4 Type Annotation

These annotations require the use of the following declaration before the beginning of the module:

#reader (planet "typed-reader.ss" ("plt" "typed-scheme.plt" 2))

This will not affect the reading or parsing of any other syntax.

#{v : t} This is legal only for binding occurences of v.

#{e :: t} This is legal only in expression contexts.

4.5 Require

Here, m is a module spec, pred is an identifier naming a predicate, and r is an optionally-renamed identifier.

(require/typed r t m)

(require/typed m [r t] ...)

(require/opaque-type t pred m)

(require-typed-struct name ([f : t] ...) m)

5 The Typed Scheme Language Level

In addition to providing a language to be used with PLT Scheme modules, Typed Scheme is also available as a language selection within DrScheme. To enable this language, simply choose it in the "Choose Language" dialog found in the "Language" menu of DrScheme. Typed Scheme programs can then be entered in the definitions window, and executed with the run button.