#lang scribble/doc

@begin[(require scribble/manual)
       (require scribble/basic)
       (require (for-label "main.ss"))]

@title[#:tag "top"]{@bold{Types}: Idioms for Typed Scheme}
@declare-exporting[(planet dherman/types:1)]

by Dave Herman (@tt{dherman at ccs dot neu dot edu})

This library provides some idioms for Typed Scheme.

@table-of-contents[]

@section[#:tag "started"]{Getting Started}

To use this library, simply require its @tt{main} module:

@defmodule[(planet dherman/types:1)]

@section[#:tag "singletons"]{Singleton Types}

A @deftech{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.

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

The following example defines a new constant @tt{nil} and defines its
corresponding singleton type @tt{Nil}:

@schemeblock[(define-constant [nil : Nil])]

@section[#:tag "variant"]{Variant Types}

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

@defform/subs[#:id define-datatype (define-datatype type-id variant-clause ...)
              ([clause [variant-id #:constant const-id]
                       [variant-id ([field-id : field-type] ...)]])]

The following example defines an expression grammar with one constant variant
and three structure variants:

@schemeblock[(define-datatype Expr
               [Nil #:constant nil]
               [Var ([name : Symbol])]
               [Abs ([var : Symbol] [body : Expr])]
               [App ([rator : Expr] [rand : Expr])])]