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:1)) |
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.
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.
| ||||||||||
|
The following example defines 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])]) |