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.
"Generalized Algebraic Data Structures" have become a a hot new topic. They have recently been added to the GHC compiler. They support the construction, maintenance, and propagation of semantic properties of programs using powerful old ideas about types (the Curry-Howard Isomorphism) in surprisingly easy to understand new ways. The language Omega was designed and implemented to demonstrate their utility. Here a a few talks I gave that explains how they work. Also class lectures
Broadly, defunctionalization is transforming a program to eliminate higher-order functions. Rather than focus on its use for compilation (see this H Cejtin, S Jagannathan, S Weeks paper on MLTon) or analyses (see Firstify from N Mitchell and C Runciman). I wanted to emphasize its use in understanding your own program, along the lines of Wand's Continuation-Based Program Transformation Strategies (JACM 1980).
demonstrates that sprintf and sscanf can indeed use exactly the same formatting specification, which is a first-class value. We demonstrate typed sprintf and typed sscanf sharing the same formatting specification. Our solution is surprisingly trivial: it defines a simple embedded domain-specific language of formatting patterns. The functions sprintf and sscanf are two interpreters of the language, to build or parse a string according to the given pattern. Our solution relies only on GADTs. We demonstrate that lambda-abstractions at the type level are expressible already in the Hindley-Milner type system; GADT with the included polymorphic recursion help us use the abstractions.
Extensible and Modular Generics for the Masses (EMGM) applies concepts of datatype-generic programming to define generic functions for supported datatypes using type classes.
for 6.10 We show how to build a quasiquoter for a simple mathematical expression language. Although the example is small, it demonstrates all aspects of building a quasiquoter. We do not mean to suggest that one gains much from a quasiquoter for such a small language relative to using abstract syntax directly except from a pedagogical point of view---this is just a tutorial!