Metamorphic programming is an approach to extend the structured recursive programming discipline, which favors the use of fold operations over general recursion, to abstract data types. The key idea is to represent an ADT by two parts, a constructorand a destructor,which are essentially functions to/from a common representation. Then a fold can work on an ADT by applying parameter functions to values that are delivered by the ADT's own destructor. Fold operations that use as a parameter the constructor of another ADT, called ADT transformers,play an important role and offer a concise programming style. Several laws for ADT folds and transformers exist that can be used for program optimization and verification.
Interpreting types as abstract values [The Abstract of the lecture notes] We expound a view of type checking as evaluation with `abstract values'. Whereas dynamic semantics, evaluation, deals with (dynamic) values like 0, 1, etc., static semantics, type checking, deals with approximations like int. A type system is sound if it correctly approximates the dynamic behavior and predicts its outcome: if the static semantics predicts that a term has the type int, the dynamic evaluation of the term, if it terminates, will yield an integer. As object language, we use simply-typed and let-polymorphic lambda calculi with integers and integer operations as constants. We use Haskell as a metalanguage in which to write evaluators, type checkers, type reconstructors and inferencers for the object language.