Levitation
Introduction
Stahl uses levitation [The Gentle Art of Levitation] to define datatypes and generic operations on them. The basic idea is that one can avoid making datatype definitions built-in if they have a few built-in values. Datatypes are then described rather than defined -- there's a type Desc that directly mirrors the syntax of datatype declarations. An operator (Data) then turns a description into a type, by induction on the Desc.
This might seem a bit roundabout, since whatever "axiomness" exists in the built-in datatype definitions still exists in these new built-ins, but this also enables generic programming. Arbitrary other functions that induct over descriptions can be defined too, for example a function that takes a description, and returns a function that converts a value of the corresponding type to a string. New descriptions can be computed as well, for example a recursive datatype that represents expressions in a programming language can be transformed to add location annotations.