The tagless-final approach is particularly attractive if the DSL to embed is also typed. One can then represent in the host language not only DSL terms but also the DSL type system (i.e., type derivations): Only well-typed DSL terms become embeddable. Therefore, the type checker of the host language checks -- and even infers for us -- DSL types. Even DSLs with resource-sensitive (affine, linear) types are thus embeddable. The approach ensures by its very construction that all interpretations -- in particular, various transformations and optimizations -- are type-preserving.
The characteristic feature of the tagless-final approach is extensibility: a DSL expression, once written, can be interpreted in a variety of ways -- to evaluate, to pretty-print, to analyze, to transform or compile. At any time one may add more interpreters, more optimization passes, and even more expression forms to the DSL while re-using the earlier written DSL programs and interpreters as they are. Perhaps counter-intuitively, the tagless-final style supports DSL transformations: from reduction, constant propagation and partial evaluation to CPS transformations and loop interchange.
We have used the approach to implement extensible DSLs in the domains of language-integrated queries, non-deterministic and probabilistic programming, delimited continuations, computability theory, stream processing, hardware description languages, generation of specialized numerical kernels, and natural language semantics.
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.
Our principal technique is to encode De Bruijn or higher-order abstract syntax using combinator functions rather than data constructors. In other words, we represent object terms not in an initial algebra but using the coalgebraic structure of the lambda-calculus. Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformations. Our encoding of an object term abstracts uniformly over the family of ways to interpret it, yet statically assures that the interpreters never get stuck. This family of interpreters thus demonstrates again that it is useful to abstract over higher-kinded types.
Joint work with Jacques Carette and Chung-chieh Shan.
Although the paper itself does not use the name `tagless-final', it gives a hint about its origins, which by now may be regarded as historical accidents. The name `tagless-final' seems to have arose spontaneously, and stuck.
Lecture notes from the course on typed tagless-final embeddings
of domain-specific languages
with mode details and more examples
README.txt [3K]
Commented code accompanying the JFP paper,
with the complete implementations of all interpreters.
The code files are in the same directory as the README.txt file.
In the so-labeled initial approach, typed terms are represented by GADTs. The absence of type-tag mismatch errors is the central property of GADT. The absence of unbound variable reference errors is assured either by higher-order abstract syntax (Xi et al., POPL 2003) or De Bruijn indices and dependent types (Pasalic et al., ICFP 2002). This page has described the final tagless approach. Type-tag mismatch errors are patently absent because there are simply no type tags and hence no possibility of type errors during interpretation. The absence of the second sort of errors can likewise be assured by higher-order abstract syntax (used here) or De Bruijn indices.
We demonstrate that the final and initial typed tagless representations are related by bijection. We use the higher-order language of the Tagless Final paper (APLAS 2007), which is the superset of the language introduced in Xi et al (POPL 2003). In the latter paper, the tagless interpretation of the language was the motivation for GADT. In a bit abbreviated form, the final and the initial representations of our DSL in Haskell are defined as follows:
class Symantics repr where
int :: Int -> repr Int
lam :: (repr a -> repr b) -> repr (a->b)
app :: repr (a->b) -> repr a -> repr b
fix :: (repr a -> repr a) -> repr a
add :: repr Int -> repr Int -> repr Int
data IR h t where
Var :: h t -> IR h t
INT :: Int -> IR h Int
Lam :: (IR h t1 -> IR h t2) -> IR h (t1->t2)
App :: IR h (t1->t2) -> IR h t1 -> IR h t2
Fix :: (IR h t -> IR h t) -> IR h t
Add :: IR h Int -> IR h Int -> IR h Int
The data constructor Var of the initial representation
corresponds to HOASLift of Xi et al. The initial
representation is parameterized by the type of the hypothetical
environment h: that is, h t is the type of
an environment `cell' holding a value of the type t.
The relation between the two representations is established as follows:
instance Symantics (IR h) where
int = INT
lam = Lam
app = App
fix = Fix
add = Add
itf :: Symantics repr => IR repr t -> repr t
itf (Var v) = v
itf (INT n) = int n
itf (Lam b) = lam(\x -> itf (b (Var x)))
itf (App e1 e2) = app (itf e1) (itf e2)
itf (Fix b) = fix(\x -> itf (b (Var x)))
itf (Add e1 e2) = add (itf e1) (itf e2)
The mapping from the final to the initial and its converse are both total; composing one mapping with the other preserves interpretations. The code below gives concrete examples of that preservation. The totality is especially easy to see for the mapping from the final to the initial, since the mapping even looks like the identity.
InFin.hs [8K]
Haskell code with the complete definitions of both representations,
several sample interpreters, complete bijections and their compositions.
The code includes several concrete examples.
Formatted IO as an embedded DSL: the initial view
Formatted IO as an embedded DSL: the final view
An example of initial and final embeddings of a DSL of formatting
patterns
Chung-chieh Shan: Translations. Blog post, August 17, 2007
<http://conway.rutgers.edu/~ccshan/wiki/blog/posts/Translations/>
class Eval gamma exp result | gamma exp -> result where
eval :: exp -> gamma -> result
Our code has been greatly inspired by the ICFP 2002 paper by
Pasalic, Taha, and Sheard on staged tagless interpreters. The paper
gives the most lucid explanation of the tagging problem in typed
interpretations. Although the paper develops a dependently typed
language Meta-D for writing typed tagless interpreters, the paper
itself gives hints that dependent types are not really necessary.
The key phrase is about indexing types by singleton types
rather than by terms. The former is easily implementable in Haskell
as it is. The introduction section gives the other hint: the apparent
problem with the eval function is that it should
yield an Int when evaluating the literal constant expression
B 1 and yield a function when evaluating the term
L "x" (Var "x"). Indeed no ordinary function
can return values of different types. But an overloaded function can,
e.g., Haskell's read.
With the help of Template Haskell, we stage our tagless code to remove its interpretative overhead. Because expressions in Template Haskell are untyped, we add a newtype wrapper to maintain their types. Our staged interpreter deals exclusively with these typed code expressions, to be faithful to the Pasalic et al. paper. Template Haskell can print code values, so we can see the staged result: the `compiled' code. In particular, here is the running example of the paper and the result of its evaluation with our staged interpreter:
stest4 = show_tcode $ seval (L (TArr TInt TInt) (V Z)) HNil
*Staged> stest4
\x_0 -> x_0
There are indeed no tags. Here is another test:
stest3 = show_tcode $ seval (A (L TInt (V Z)) (B 2)) HNil
*Staged> stest3
(\x_0 -> x_0) 2#
If we change TInt above to TArr TInt TInt, we get a type error
before running stest3: The typing is indeed done at the
meta-level.
The present code was the first attempt to define tagless interpreters in a language without (overt) dependent types. This work has continued in cooperation with Jacques Carette and Chung-chieh Shan. We showed that writing typed interpreters becomes significantly simpler if we change the building blocks of object language terms, from data constructors to constructor functions.
Interp.hs [3K]
The tagless typed interpreter for the the typed language of the
above paper, viz. simply-typed lambda-calculus with De Bruijn indices.
The interpreter is deliberately patterned after the one in the paper,
including the type-level function TypEval. The code almost literally
implements the Meta-D interpreter from Fig.3 of the paper and the
typing rules from Fig.1 -- without any dependent types.
Staged.hs [3K]
The staged tagless typed interpreter
Implicit configurations -- or, type classes reflect the values of types
(Haskell Workshop 2004. Joint work with Chung-chieh Shan)
The paper demonstrates how easy it is to introduce type families
indexed by singleton types in Haskell as it was in 2003: Haskell98
extended with multi-parameter type classes with functional
dependencies.