#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:2)]

@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 ...)
                (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 @scheme[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:

@schemeblock[(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.

@schemeblock[(define-datatype (Tree a)
               [Empty #:constant empty]
               [Node ([value : a] [left : (Tree a)] [right : (Tree a)])])]