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.
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.
Lecture notes from the course on typed tagless-final embeddings of domain-specific languages
with mode details and more examples
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 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 IntThe data constructor
Varof the initial representation corresponds to
HOASLiftof Xi et al. The initial representation is parameterized by the type of the hypothetical environment
h tis the type of an environment `cell' holding a value of the type
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.
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/ >
Lambda: the ultimate syntax-semantics interface
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_0There 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
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 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.
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.
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML