Examples of ML implementations of ADTs

ADTs specified with Algebraic semantics, Guttag's hueristic, can be directly implemented in ML... almost a syntactic transformation.

The canonical methods of your specs are expressed in an ML "datatype" definition
Each non-canonical method is defined as a "fun" definition using the pattern matching facilities of ML. Create one alternative per axiom.

Stack of Int

Bounded Stack of Int

A more complicated stack of int defined to have a max size; push is defined to do nothing is it is applied to a full stack

Bubble Top Stack of Int

A stack (of int) where elements in the stack are unique... like a set... if you push an element on the stack that is already in the stack, the element "bubbles" to the top