8
$\begingroup$

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 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.

Improve this question
$\endgroup$
1
  • 2
    $\begingroup$ 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. $\endgroup$
    – Jacques Carette
    Sep 20, 2019 at 21:17

2 Answers 2

Reset to default
5
$\begingroup$

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/ .

Improve this answer
$\endgroup$
4
  • $\begingroup$ 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. $\endgroup$
    – Dan Doel
    Sep 21, 2019 at 4:03
  • $\begingroup$ I'll need to think through this before I select an answer. $\endgroup$
    – Henry Story
    Sep 21, 2019 at 8:21
  • $\begingroup$ Max New's emphasis on "observational equivalence" is very intriguing, as it is associated with Coalgebras. A recent paper Codata in Action 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? $\endgroup$
    – Henry Story
    Sep 21, 2019 at 21:26
  • $\begingroup$ The recent lecture notes by Andrej Bauer What is Algebraic about Effects and Handlers 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... $\endgroup$
    – Henry Story
    Sep 23, 2019 at 6:25
1
$\begingroup$

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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.