These lecture notes introduce the final approach slowly and in detail, highlighting extensibility, the solution to the expression problem, and the seemingly impossible pattern-matching. We develop the approach further, to type-safe cast, run-time-type representation, Dynamics, and type reconstruction. We finish with telling examples of type-directed partial evaluation and encodings of type-and-effect systems and linear lambda-calculus.
Symantics: parameterization of terms by interpreters
Initial and Final, Deep and Shallow, First-class
Algebraic data types are indeed not extensible
Adding a new expression form to the final view: solving the expression problem
Serialization and de-serialization
De-serializing the extended language
Tagless-final embedding using modules
Tagless-final embedding with objects emulating type-class dictionaries. Both the language and the set of its interpretations are extensible.
Pushing the negation down: the `final' implementation
Pushing the negation down for extended tagless-final terms
Flattening of additions, the initial and the final implementations
The final-initial isomorphism, and its use for implementing arbitrary pattern-matching operations on tagless-final terms.
`Initial' and `Final' as isomorphic initial algebras
Ralf Hinze, in Part 7 of his Spring School course, has derived this `initial-final' isomorphism rigorously, generally and elegantly from the point of view of Category Theory. In the first-order case, both `initial' and `final' are the left and the right views to the same Initial Algebra. The `final' view is, in the first-order case, the ordinary Boehm-Berarducci encoding.
Modular, composable, typed
Tagless-final optimizations, algebraically and semantically
General, systematic approach that supports arbitrary transformations on tagless-final terms.
Shin-Cheng Mu: Typed Lambda-Calculus Interpreter in Agda. September 24, 2008
Shin-Cheng Mu solves the problem of the type-preserving tagless interpretation of simply-typed lambda-calculus, relying on dependent types and type functions in full glory.
Tagless-initial and Tagless-final evaluators
Typed, tagless, final, with De Bruijn indices: Expressing the type system of simply-typed lambda-calculus in Haskell98. No dependent types are necessary after all. The types of methods in the Symantics type class read like the axioms and inference rules of the implication fragment of minimal logic.
Typed, tagless, final, in the higher order abstract syntax (HOAS). We illustrate extending the DSL with more constants, types, and expression forms.
Initial-final isomorphism, in the higher-order case TTFdBHO.hs [2K]
Converting from the De-Bruijn--based Symantics to the one based on the higher-order abstract syntax
This is the first example of a transformer, which translates from one Symantics to another. The transformer works as an interpreter, whose primitive operations are implemented in terms of another Symantics. In the tagless final approach, transformers are manifestly typed and type-preserving.
Type representation, equality and the type-safe generalized cast
We present an above-the-board version of
in the tagless-final style. Our implementation uses no GHC
internal operations, no questionable extensions, or even a hint
of unsafe operations.
Stephanie Weirich wrote a very similar type-checker, but using GADTs. The comparison with the tagless-final style here is illuminating.
Typed Type Checking