Types: Idioms for Typed Scheme

by Dave Herman (dherman at ccs dot neu dot edu)

This library provides some idioms for Typed Scheme.

1 Getting Started

To use this library, simply require its main module:

(require (planet dherman/types:2))

2 Singleton Types

A singleton type is a type that corresponds to a single value. The following form defines a new distinct value and simultaneously binds a variable to that value and a type variable to its singleton type.

(define-constant [const-id : type-id] ...+)

The following example defines a new constant nil and defines its corresponding singleton type Nil:

  (define-constant [nil : Nil])

3 Variant Types

A variant type or disjoint union type is a type defined as the union of a fixed set of disjoint subtypes. This is analogous to ML’s datatype and Haskell’s data. Each variant is either a constant or a structure type.

(define-datatype type-id variant-clause ...)

(define-datatype (type-id type-param-id ...) variant-clause ...)

clause   =   [variant-id #:constant const-id]     |   [variant-id ([field-id : field-type] ...)]

The first form defines a monomorphic variant type, and the second form defines a polymorphic variant type with type variables type-param-id ....

The following example defines the type of abstract syntax nodes for an expression grammar with one constant variant and three structure variants:

(define-datatype Expr

[Nil #:constant nil]

[Var ([name : Symbol])]

[Abs ([var : Symbol] [body : Expr])]

[App ([rator : Expr] [rand : Expr])])

The following example defines a polymorphic tree datatype.

(define-datatype (Tree a)

[Empty #:constant empty]

[Node ([value : a] [left : (Tree a)] [right : (Tree a)])])