The course on typed tagless-final embeddings of domain-specific languages has been presented at the Spring School on Generic and Indexed Programming (SSGIP) < http://www.comlab.ox.ac.uk/projects/gip/school.html > at Wadham College, Oxford, UK on 22nd to 26th March 2010. This page collects the notes for the course in the form of the extensively commented Haskell and OCaml code.
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.
We will be talking about ordinary data types and (generic) operations on them. The expression problem will make its appearance. The first-order case makes it easier to introduce de-serialization and seemingly non-compositional operations.
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
The traditional application of objects to represent extensible data types. Alas, the set of operations on these data types is not extensible.
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 initial implementation
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.
< http://www.comlab.ox.ac.uk/ralf.hinze/SSGIP10/Slides.pdf >
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, ordinary Church encoding.
Modular, composable, typed optimizations
General, systematic approach that supports arbitrary transformations on tagless-final terms.
Higher-order languages are data types with binding, so to speak. In the first part, only the interpreters were typed; we could get away with our object language being unityped. Now, the object language itself becomes typed, bringing the interesting issues of interpreting a typed language in a type language ensuring type preservation. It is this part that explains the attributes `typed' and 'tagless' in the title of the course.
The illustration of problems of embedding a typed DSL into a typed metalanguage
Either the Universal type (and hence spurious partiality, type tags and inefficiency), or fancy type systems seem inevitable. The problem stems from algebraic data types' being too broad: they express not only well-typed DSL terms but also ill-typed ones.
< http://www.iis.sinica.edu.tw/~scm/2008/typed-lambda-calculus-interprete/ >
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
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.
De-serialization: (Dynamic) Type Checking
In contrast to an earlier version of the type checker, we use De Bruijn indices and obtain a much clearer code. The code is quite similar to Baars and Swierstra's ``Typing Dynamic Typing'' (ICFP02). However, the result of our type-checking is an embedded DSL expression that can be interpreted many times and in many ways, rather than being merely evaluated. The set of possible interpretations is open. Also, our code is written to expose more properties of the type-checker for verification by the Haskell type-checker; for example, that closed source terms are de-serialized into closed target terms.
Type representation, equality and the type-safe generalized cast
We present an above-the-board version of
Data.Typeable , in the tagless-final style. Our implementation uses no GHC internal operations, no questionable extensions, or even a hint of unsafe operations.
< http://www.comlab.ox.ac.uk/projects/gip/school/tc.hs >
Stephanie Weirich wrote a very similar type-checker, but in the initial style, using GADTs. The comparison with the tagless-final style here is illuminating.
Typed Type Checking
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML