1 Getting Started
2 Singleton Types
3 Variant Types

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

    2 Singleton Types

    3 Variant Types

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)])])