Typed tagless final interpreters

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

38 Citations (Scopus)


The so-called 'typed tagless final' approach of [6] 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.

Original languageEnglish
Title of host publicationGeneric and Indexed Programming -International Spring School, SSGIP 2010, Revised Lectures
Number of pages45
Publication statusPublished - 2012
EventInternational Spring School on Generic and Indexed Programming, SSGIP 2010 - Oxford, United Kingdom
Duration: 2012 Mar 222012 Mar 26

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7470 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceInternational Spring School on Generic and Indexed Programming, SSGIP 2010
Country/TerritoryUnited Kingdom


Dive into the research topics of 'Typed tagless final interpreters'. Together they form a unique fingerprint.

Cite this