Start on tagless final

build.sbt

@@ -133,6 +133,8 @@ lazy val pages = List(
   "indexed-types/codata.md",
   "indexed-types/data.md",
   "indexed-types/conclusions.md",
+  // Tagless Final
+  "tagless-final/index.md",
   // Interpreter optimization
   "adt-optimization/index.md",
   "adt-optimization/algebra.md",

src/pages/codata/extensibility.md

@@ -1,4 +1,4 @@
-## Data and Codata Extensibility
+## Data and Codata Extensibility {#sec:codata:extensibility}
 
 We have seen that codata can represent types with an infinite number of elements, such as `Stream`. This is one expressive difference from data, which must always be finite. We'll now look at another, which is the type of extensibility we get from data and from codata. Together these gives use guidelines to choose between the two.
 

src/pages/tagless-final/index.md

@@ -0,0 +1,13 @@
+# Tagless Final Interpreters
+
+We've seen the duality between data and codata in many places, starting in [@sec:codata], but we haven't yet explored interpreters that use the codata approach. In this chapter we'll do so, looking at a strategy known as **tagless final**.
+
+Tagless final is a little bit more than a straightforward application of the data-codata duality.
+In particular, it solves a problem around extensibility known as the **expression problem**.
+We first met this problem in [@sec:codata:extensibility].
+In the context of interpreters, solving the expression problem allowing extensibility of both the programs we write and the interpreters that run them.
+
+We'll start this chapter looking at codata interpreters.
+We'll see they have a shortcoming, which motivates the expression problem.
+
+Solving the expression problem allows for very expressive code, as the name suggests.