<p>Final Algebra semantics was introduced by Mitch Wand in his paper "Final Algebra Semantics and Data Type Extensions", see this freely available tech report: <a href="https://www.cs.indiana.edu/ftp/techreports/TR65.pdf" rel="noreferrer">https://www.cs.indiana.edu/ftp/techreports/TR65.pdf</a> .</p>

<p>It does not mean final coalgebra semantics, which is a very different idea. The wrinkle is that the algebra is <em>not</em> final in the same category that the initial algebra is initial, because then the final algebra would just be given by the unit type/terminal object as carrier. Instead, Wand defines a category of <em>adequate</em> extensions of an algebra, which basically say you want the algebras in question to not equate basic values. An example of this is that the signature may contain numbers and you only want to consider algebras where the interpretations of distinct integers are unequal. This rules out the trivial terminal object as carrier because it would equate all numbers. I wrote a blog post about this a while ago in an attempt to understand the same question: <a href="http://prl.ccs.neu.edu/blog/2017/09/27/final-algebra-semantics-is-observational-equivalence/" rel="noreferrer">http://prl.ccs.neu.edu/blog/2017/09/27/final-algebra-semantics-is-observational-equivalence/</a> .</p>

CC BY-SA 4.0
2019-09-21T04:03:16.620Z
These final algebras are actually different than the "finally tagless" stuff mentioned in the question. The latter are actually initial algebras, just encoded in a different way than data declarations, whereas the `Integer -> Integer` bag example is not, as desired. There are characterizations of the 'finally tagless' stuff as 'final' things. For instance, initial algebras are limits of the underlying functor from the category of algebras. But this is true of any initial algebra, including representation by datatype.
Dan Doel
CC BY-SA 4.0
2019-09-21T08:21:03.637Z
I'll need to think through this before I select an answer.
Henry Story
CC BY-SA 4.0
2019-09-21T21:26:29.400Z
Max New's emphasis on "observational equivalence" is very intriguing, as it is associated with Coalgebras. A recent paper [Codata in Action](https://twitter.com/bblfish/status/1173269815802441728) shows how one can move between data and codata via the observer pattern, which is what is used by Object Algebras. Furthermore finally tagless in Scala is represented by interfaces which allow for multiple implementations as explained by coalgebras. Finally cats of coalgebras do have final objects. Could it be that what is occurring is a mapping between initial algebras and final coalgebras?
Henry Story
CC BY-SA 4.0
2019-09-23T06:25:17.050Z
The recent lecture notes by Andrej Bauer [What is Algebraic about Effects and Handlers](https://arxiv.org/pdf/1807.05923.pdf) described what Algebras, interpretations and models are, what initial models are and how by parameterizing them one gets effects. Then in ¶4 "What is Coalgebraic about Algebraic Effects and Handlers?" he looks at the dual, and finds cooperations, cointerpretations, comodels. I note that we also have parameters in final tagless...
Henry Story
CC BY-SA 4.0
2019-09-20T14:15:15.403Z
2019-09-20T14:15:15.403Z
Max New
<p>I took a brief look at the first paper you cite, and I think Max New's answer does have some relevance to it. The purpose of this answer is to explain how I think the 'finally tagless' stuff gets a bit confused itself about the idea.</p>

<p>The paper starts with a simple algebraic signature for a language with literal numbers, addition and negation. It says that the initial algebra is:</p>

<pre><code>data Expr = Lit Int | Add Expr Expr | Neg Expr
</code></pre>

<p>and that the final algebra is just <code>Int</code>. This is using "final algebra" in the same sense as Max New's answer, I think. <code>Int</code> is the final algebra that does not crush distinct literals to the same thing.</p>

<p>However, the paper proceeds to introduce the idea of abstracting over a choice of 'semantic domain' for the 'final algebra.' However, when you do this, you no longer have the final algebra, even though the paper still calls it the 'final encoding' and whatnot. The idea in the paper is to introduce a type class like:</p>

<pre><code>class ExprC r where
  lit :: Int -&gt; r
  add :: r -&gt; r -&gt; r
  neg :: r -&gt; r
</code></pre>

<p>But what this actually is is a specification of an algebra structure on <code>r</code>. If we define:</p>

<pre><code>data ExprF r = LitF Int | AddF r r | NegF r
</code></pre>

<p>Then an instance <code>ExprC r</code> is equivalent to a function <code>ExprF r -&gt; r</code>. And a polymorphic expression with type <code>ExprC r =&gt; r</code> is equivalent to an expression with type <code>(ExprF r -&gt; r) -&gt; r</code>. But this polymorphic type is an encoding of the initial algebra. We can give an instance for the final algebra <code>Int</code>, but this is equivalent to recognizing that this final algebra is an algebra in the same category that the initial algebra is initial in, and the instantiation of the polymorphic expression with type <code>ExprC r =&gt; r</code> to <code>r = Int</code> is equivalent to using the mapping from the initial algebra.</p>

<p>A way of thinking about this with respect to Max's answer is as follows: An algebra is only final with respect to some other theory's inclusion. To get <code>Int</code> we use an inclusion that prevents us from identifying distinct literals. However, the abstraction that the 'finally tagless' stuff does abstracts over the choice of inclusion, and demands that we must not crush anything that <em>any</em> choice of inclusion would require us to distinguish. However, this is exactly what the initial algebra does. In particular, we could choose the identity theory inclusion, which I think would make the initial and final algebra coincide.</p>

CC BY-SA 4.0
2019-09-21T19:47:49.190Z
2019-09-21T19:47:49.190Z
Dan Doel
<p>The Haskell and Scala community have been very enamored recently with what they call tagless <strong>final</strong> 'pattern' of programming. These are referenced as dual to initial free algebras, so I was wondering what Tagless Final was final of. On ncatlab one only finds talk of final coalgebras, not final algebras. </p>

<p>A few references:</p>

<ul>
<li>The influential Haskell <a href="http://okmij.org/ftp/tagless-final/course/lecture.pdf" rel="noreferrer">Typed Tagless Final Interpreters</a> lecture notes</li>
<li>A translation of that article for Scala (Dotty) <a href="https://gist.github.com/OlivierBlanvillain/48bb5c66dbb0557da50465809564ee80" rel="noreferrer">Revisiting Tagless Final Interpreters</a></li>
<li>A blog post <a href="https://oleksandrmanzyuk.wordpress.com/2014/06/18/from-object-algebras-to-finally-tagless-interpreters-2/" rel="noreferrer">From Object Algebras to Finally Tagless Interpreters</a> makes the case that Object algebras are equivalent to Tagless Final.</li>
<li>It cites the paper <a href="https://www.cs.utexas.edu/~wcook/Drafts/2012/ecoop2012.pdf" rel="noreferrer">Extensibility for the Masses, practical extensibility with Object Algebras</a>.</li>
</ul>

<p>The example used by these are clearly Algebras, which in category theory are expressed with endofunctors <code>F</code> as maps of the form <code>F(X) -&gt; X</code>. Coalgebras are dual maps <code>X -&gt; F(X)</code>, and represent processes.</p>

<p>The follow up question is more about use of final tagless in programming circles which seems to be more related to final coalgebras. 
See the question <a href="https://stackoverflow.com/questions/58025604/are-tagless-final-object-algebras-and-codata-essentially-the-same">on stackoverflow here</a>.</p>

CC BY-SA 4.0
2019-09-20T21:17:11.120Z
The 'final' in 'finally tagless, partially evaluated' (the original paper that you skipped over) is an adjective qualifying 'tagless', and is a pun on partial evaluation's tagging-untagging problem. It does *allude* to final semantics (since 'final tagless' is really specifying an algebra via its polymorphic fold in a way that prevents 'peeking', unlike all initial algebra based methods) because all you can do is to call the fold. But it's still not 'final' in any reasonable way, even though there's dualities galore lurking around the corner.
Jacques Carette
<functional-programming><algebra><ct.category-theory><object-oriented>
What category are Tagless Final Algebras final In?
Henry Story
# What category are Tagless Final Algebras final In?

(Asked by: username_0 on 2019-09-20)

The Haskell and Scala community have been very enamored recently with what they call tagless **final** 'pattern' of programming. These are referenced as dual to initial free algebras, so I was wondering what Tagless Final was final of. On ncatlab one only finds talk of final coalgebras, not final algebras.

A few references:

* The influential Haskell [Typed Tagless Final Interpreters](http://okmij.org/ftp/tagless-final/course/lecture.pdf) lecture notes
* A translation of that article for Scala (Dotty) [Revisiting Tagless Final Interpreters](https://gist.github.com/OlivierBlanvillain/48bb5c66dbb0557da50465809564ee80)
* A blog post [From Object Algebras to Finally Tagless Interpreters](https://oleksandrmanzyuk.wordpress.com/2014/06/18/from-object-algebras-to-finally-tagless-interpreters-2/) makes the case that Object algebras are equivalent to Tagless Final.
* It cites the paper [Extensibility for the Masses, practical extensibility with Object Algebras](https://www.cs.utexas.edu/~wcook/Drafts/2012/ecoop2012.pdf).

The example used by these are clearly Algebras, which in category theory are expressed with endofunctors `F` as maps of the form `F(X) -> X`. Coalgebras are dual maps `X -> F(X)`, and represent processes.

The follow up question is more about use of final tagless in programming circles which seems to be more related to final coalgebras.
See the question [on stackoverflow here](https://stackoverflow.com/questions/58025604/are-tagless-final-object-algebras-and-codata-essentially-the-same).

**Tags:** functional-programming, algebra, ct.category-theory, object-oriented
> **Comments:**
> **username_1**: The 'final' in 'finally tagless, partially evaluated' (the original paper that you skipped over) is an adjective qualifying 'tagless', and is a pun on partial evaluation's tagging-untagging problem. It does *allude* to final semantics (since 'final tagless' is really specifying an algebra via its polymorphic fold in a way that prevents 'peeking', unlike all initial algebra based methods) because all you can do is to call the fold. But it's still not 'final' in any reasonable way, even though there's dualities galore lurking around the corner.  

---

## 2 answers

### Answer by username_2 on 2019-09-20. Score: 5

Final Algebra semantics was introduced by Mitch Wand in his paper "Final Algebra Semantics and Data Type Extensions", see this freely available tech report: <https://www.cs.indiana.edu/ftp/techreports/TR65.pdf> .

It does not mean final coalgebra semantics, which is a very different idea. The wrinkle is that the algebra is *not* final in the same category that the initial algebra is initial, because then the final algebra would just be given by the unit type/terminal object as carrier. Instead, Wand defines a category of *adequate* extensions of an algebra, which basically say you want the algebras in question to not equate basic values. An example of this is that the signature may contain numbers and you only want to consider algebras where the interpretations of distinct integers are unequal. This rules out the trivial terminal object as carrier because it would equate all numbers. I wrote a blog post about this a while ago in an attempt to understand the same question: <http://prl.ccs.neu.edu/blog/2017/09/27/final-algebra-semantics-is-observational-equivalence/> .

> **Comments:**
> **username_3**: These final algebras are actually different than the "finally tagless" stuff mentioned in the question. The latter are actually initial algebras, just encoded in a different way than data declarations, whereas the `Integer -> Integer` bag example is not, as desired. There are characterizations of the 'finally tagless' stuff as 'final' things. For instance, initial algebras are limits of the underlying functor from the category of algebras. But this is true of any initial algebra, including representation by datatype.  
> **username_0**: I'll need to think through this before I select an answer.  
> **username_0**: Max New's emphasis on "observational equivalence" is very intriguing, as it is associated with Coalgebras. A recent paper [Codata in Action](https://twitter.com/bblfish/status/1173269815802441728) shows how one can move between data and codata via the observer pattern, which is what is used by Object Algebras. Furthermore finally tagless in Scala is represented by interfaces which allow for multiple implementations as explained by coalgebras. Finally cats of coalgebras do have final objects. Could it be that what is occurring is a mapping between initial algebras and final coalgebras?  
> **username_0**: The recent lecture notes by Andrej Bauer [What is Algebraic about Effects and Handlers](https://arxiv.org/pdf/1807.05923.pdf) described what Algebras, interpretations and models are, what initial models are and how by parameterizing them one gets effects. Then in ¶4 "What is Coalgebraic about Algebraic Effects and Handlers?" he looks at the dual, and finds cooperations, cointerpretations, comodels. I note that we also have parameters in final tagless...  

---

### Answer by username_3 on 2019-09-21. Score: 1

I took a brief look at the first paper you cite, and I think Max New's answer does have some relevance to it. The purpose of this answer is to explain how I think the 'finally tagless' stuff gets a bit confused itself about the idea.
The paper starts with a simple algebraic signature for a language with literal numbers, addition and negation. It says that the initial algebra is:
data Expr = Lit Int | Add Expr Expr | Neg Expr

and that the final algebra is just Int. This is using "final algebra" in the same sense as Max New's answer, I think. Int is the final algebra that does not crush distinct literals to the same thing.
However, the paper proceeds to introduce the idea of abstracting over a choice of 'semantic domain' for the 'final algebra.' However, when you do this, you no longer have the final algebra, even though the paper still calls it the 'final encoding' and whatnot. The idea in the paper is to introduce a type class like:
class ExprC r where
  lit :: Int -> r
  add :: r -> r -> r
  neg :: r -> r

But what this actually is is a specification of an algebra structure on r. If we define:
data ExprF r = LitF Int | AddF r r | NegF r

Then an instance ExprC r is equivalent to a function ExprF r -> r. And a polymorphic expression with type ExprC r => r is equivalent to an expression with type (ExprF r -> r) -> r. But this polymorphic type is an encoding of the initial algebra. We can give an instance for the final algebra Int, but this is equivalent to recognizing that this final algebra is an algebra in the same category that the initial algebra is initial in, and the instantiation of the polymorphic expression with type ExprC r => r to r = Int is equivalent to using the mapping from the initial algebra.
A way of thinking about this with respect to Max's answer is as follows: An algebra is only final with respect to some other theory's inclusion. To get Int we use an inclusion that prevents us from identifying distinct literals. However, the abstraction that the 'finally tagless' stuff does abstracts over the choice of inclusion, and demands that we must not crush anything that any choice of inclusion would require us to distinguish. However, this is exactly what the initial algebra does. In particular, we could choose the identity theory inclusion, which I think would make the initial and final algebra coincide.


---

