By Jacob Neumann, June 2021
This page collects the documentation of the Auxiliary Library. The purpose of this library & its documentation is to serve as sample code, proofs, and worked examples for students learning functional programming and/or SML for the first time. Accordingly, this documentation also includes explicit mathematical definitions, proofs by induction, asymptotic analyses, and evaluation traces, as appropriate.
Unless otherwise stated, the documentation assumes SMLNJ v110.99. Some features (e.g. modifications of the pretty printer) might not work in other versions of SMLNJ.
All the documents & code here should be considered "work-in-progress". If you spot an error in either, you can report it here.
Provides polymorphic binary trees in a structure
Tree, with a couple basic methods for working with them.
In particular, this includes the functions
foldr, which are used in the
OrdTreeSet functor (see Sets below) and critical to the associated representation independence result.
Timing module includes types for encoding years, months, days, times, time zones, etc., as well as numerous utilities for working with them. This module primarily serves as an extended example of how to use custom SML
datatypes to encode data, and how to take advantage of pattern matching to write elegant code. This module includes some imperative features (achieved utilizing basis modules unique to SMLNJ), such as stopwatches, countdown timers, and functions which obtain the current time.
Permute module contains utilities for permutating and sorting lists. The functions in this module are polymorphic, and some of the sorting functions furthermore serve as examples of currying.
CPSIterate module allows for imperative-programming-esque loops, but defined entirely functionally and entirely in continuation passing style.
Language module provides combinators for working with "languages": lists of values of some equality type
Sigma. Connects to some of the classic theory of computation, as well as providing sufficient combinators to capture a fragment of the logic of regular expressions. Good showcase of Higher-Order Functions & Combinators.
Regexp module implements regular expressions in Standard ML. Parametrizes over an "alphabet" (equality) type
Sigma, and implements a type
''Sigma regexp with a CPS/Exn-control-flow function
match which performs regular expression matching. Includes a method for obtaining the language of a regular expression, implemented using the
Language module (above).
An implementation of sets in Standard ML. Includes
ORD typeclasses, the
SET signature, and three implementations:
ListSet (sets are unordered, duplicate free lists),
OrdListSet (sorted, duplicate-free lists), and
OrdTreeSet (sorted, duplicate-free trees). The latter two are equivalent (as proven by a representation independence proof), but the superior time bounds of
OrdTreeSet are not realized unless we can maintain a balance invariant -- providing motivation for red-black trees.