Examples of ML implementations of ADTs

ADTs specified with Algebraic semantics, Guttag's hueristic, can be directly implemented in ML... almost a syntactic transformation.
  1. The canonical methods of your specs are expressed in an ML "datatype" definition
  2. Each non-canonical method is defined as a "fun" definition using the pattern matching facilities of ML. Create one alternative per axiom.