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.