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.
Intro2.hs [3K]
Symantics: parameterization of terms by interpreters
Intro3.hs [2K]
Initial and Final, Deep and Shallow, First-class
ExtI.hs [<1K]
Algebraic data types are indeed not extensible
ExtF.hs [2K]
Adding a new expression form to the final view: solving the
expression problem
Serialize.hs [7K]
Serialization and de-serialization
SerializeExt.hs [4K]
De-serializing the extended language
final_mod.ml [3K]
Tagless-final embedding using modules
final_dic.ml [3K]
Tagless-final embedding with objects emulating type-class dictionaries.
Both the language and the set of its interpretations are extensible.
PushNegF.hs [3K]
Pushing the negation down: the `final' implementation
PushNegFExt.hs [4K]
Pushing the negation down for extended tagless-final terms
FlatI.hs [2K]
FlatF.hs [4K]
Flattening of additions, the initial and the final implementations
PushNegFI.hs [4K]
The final-initial isomorphism, and its use for implementing
arbitrary pattern-matching operations on tagless-final terms.
`Initial' and `Final' as isomorphic initial algebras
<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, the ordinary
Boehm-Berarducci encoding.
Modular, composable, typed
optimizations
Tagless-final optimizations, algebraically and semantically
General, systematic approach that supports arbitrary transformations
on tagless-final terms.
Term.agda [2K]
<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.
IntroHOIF.hs [6K]
Tagless-initial and Tagless-final evaluators
TTFdB.hs [7K]
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.
TTF.hs [7K]
Typed, tagless, final, in the higher order abstract syntax (HOAS).
We illustrate extending the DSL with more constants, types,
and expression forms.
TTIF.hs [8K]
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.
Typ.hs [8K]
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 using GADTs. The comparison with the
tagless-final style here is illuminating.