previous   next   up   top

Typed final (tagless-final) style


Typed final (aka, ``tagless-final'') style is a general method of embedding domain-specific languages (DSL) in a typed functional language such as Haskell, OCaml, Scala or Coq. The approach is an alternative to the traditional encoding of an object language as a (generalized) algebraic data type. It is centered around interpreters: Evaluator, compiler, partial evaluator, pretty-printer, multi-pass optimizer are all interpreters of DSL expressions.

The typed final approach is particularly attractive if the DSL to embed is also typed. We can then represent in the host language not only terms but also the type system (type derivations) of the DSL. Only well-typed DSL terms are 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 also statically ensures that all interpretations -- in particular, various transformations and optimizations -- are type-preserving.

The characteristic feature of the tagless-final approach is extensibility: At any time one may add more interpreters, more optimization passes, and even more expression forms to the DSL while re-using the previous interpreters as they were. Perhaps counter-intuitively, the tagless-final style supports DSL transformations: from constant propagation and partial evaluation to CPS transformations and loop interchange.

Papers and Tutorials
Applications and Examples: Cookbook


Typed Tagless Final Interpreters: Lecture Notes

The so-called `typed tagless final' approach of Carette et al. has collected and polished a number of techniques for representing typed higher-order languages in a typed metalanguage, along with type-preserving interpretation, compilation and partial evaluation. The approach is an alternative to the traditional, or `initial' encoding of an object language as a (generalized) algebraic data type. Both approaches permit multiple interpretations of an expression, to evaluate it, pretty-print, etc. The final encoding represents all and only typed object terms without resorting to generalized algebraic data types, dependent or other fancy types. The final encoding lets us add new language forms and interpretations without breaking the existing terms and interpreters.

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.

The current version is August 2012.
lecture.pdf [275K]
Typed Tagless Final Interpreters
Generic and Indexed Programming: International Spring School, SSGIP 2010, Oxford, UK, March 22-26, 2010, Revised Lectures
Springer-Verlag Berlin Heidelberg, Lecture Notes in Computer Science 7470, 2012, pp. 130-174 doi:10.1007/978-3-642-32202-0_3

Course materials


Finally Tagless, Partially Evaluated: Tagless Staged Interpreters for Simpler Typed Languages

[The Abstract of the paper]
We have built the first family of tagless interpretations for a higher-order typed object language in a typed metalanguage (Haskell or ML) that require no dependent types, generalized algebraic data types, or postprocessing to eliminate tags. The statically type-preserving interpretations include an evaluator, a compiler (or staged evaluator), a partial evaluator, and call-by-name and call-by-value CPS transformers.

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.

The current version is 1.3, 2009.
JFP.pdf [217K]
Journal of Functional Programming 19(5):509-543, 2009

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.


Relating Final and Initial typed tagless representations

We have seen two approaches to typed tagless representation of an embedded DSL. Either representation can be interpreted with no errors due to type-tag mismatch, or due to a reference to an unbound variable. The absence of both sorts of errors is statically assured and patent to the metalanguage compiler.

In the 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 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: 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)

We note the properties of the mappings from the final to the initial and vice versa: both mappings are total and a composition of 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 looks like identity. The mapping is one of many possible interpretations of a term in the final tagless form.

The current version is 1.1, Jan 1, 2008.
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


Abstract Categorial Grammars: Tagless-Final style for natural languages

Typed tagless interpretations can relate form with meaning in natural languages. An abstract syntax expression may be interpreted either to yield an utterance or text, or to produce a semantic denotation. Types (in linguistics, categories) ensure the well-formedness of forms, expressions, and denotations. In that sense, typed tagless interpretation turns out to be closely related to Abstract Categorial Grammars (ACGs).
Abstract Categorial Grammar page
< >

Chung-chieh Shan: Translations. Blog post, August 17, 2007.
< >

Lambda: the ultimate syntax-semantics interface


Tagless (staged) interpreter typeclass for typed languages

We demonstrate a tagless (definitional) interpreter for a typed language implemented in a typed meta-language: Haskell with multi-parameter typeclasses and functional dependencies. The interpreter uses no universal type, no type tags, no pattern-matching. It is, in fact, total -- syntactically . The interpreter supports heterogeneous binding environment and the (functional) dependence of the type of the result on the structure of the source term. The interpreter is in fact a type class:
     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 interpretation. 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 was about indexing types by singleton types rather than by terms. The former is easily implementable in Haskell as it is. The introduction section gave 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.

The current version is 1.1, Aug 17, 2006.
Emir Pasalic, Walid Taha, Tim Sheard: Tagless Staged Interpreters for Typed Languages. ICFP 2002.

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.

Last updated August 19, 2016

This site's top page is
Your comments, problem reports, questions are very welcome!

Converted from HSXML by HSXML->HTML