Background
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.
Asking the Question What Category are Tagless Final Algebras Final In on CS-Theory Stack Exchange I got a very good answer pointing to this blog post Final Algebra Semantics is Observational Equivalence. So these are indeed final algebras, but not in the same category of algebras as the initial one....
Question
Yet, when we look at how final tagless is used, we find that it is very often applied for things that look like coalgebras. See for example the two examples of a Console or a UserRepository in part 1 of The False Hope of Managing Effects with Tagless-Final in Scala.
So instead of having Algebras which in category theory are expressed with endofunctors F as maps of the form F(X) ⟹ X, it looks like many use final tagless with Coalgebras which are maps X ⟹ F(X), and represent processes. Are these really the same thing? Or is something else going on here?
ADTs and Final Tagless
On Algebras
Let's start by the explanations of final tagless given by Olivier Blanvillain's Scala translation of examples taken from coursework on in Haskell. One notices that this starts with an Algebraic Data Type that is indeed the archetype of an Algebraic structure: a Group.
In category a group can be built out of a the Polynomial Functor
F[X] = X×X + X + 1 which takes any type to the type that is either the pair of that type or that type or 1. Then selecting one specific type for X, say A an algebra is a function F[A] ⟹ A. The most widely known group is the set of positive and negative natural numbers and 0 denoted ℤ, and so our algebra is:
ℤ×ℤ + ℤ + 1 ⟹ ℤ
The algebra can be decomposed into 3 function +: ℤ×ℤ ⟹ ℤ, -: ℤ ⟹ ℤ and the constant zero: 1 ⟹ ℤ. If we vary the type X we get different algebras, and these form a category, with morphisms between them, where the most important one is the initial algebra.
The initial algebra is the free one which allows one to build all the structure without ever loosing any information. In Scala 3 we can build the initial algebra for a group like this:
enum IExp {
case Lit(i: Int)
case Neg(e: IExp)
case Add(r: IExp, l: IExp)
}
And we can build a simple structure using it:
import IExp._
val fe: IExp = Add(Lit(8), Neg(Add(Lit(1), Lit(2))))
The fe structure can then be interpreted by creating functions IExp => Int or IExp => String, which are morphisms in the category of algebras,
which one reaches by deconstructing the ADT, and recursively mapping these
to an algebra with for a specific X (eg String or Int). This morphism is known as a fold. (See the 1997 book The Algebra of Programming, by Richard Bird and Oege de Moor)
In Tagless final this is transformed into the trait
trait Exp[T] {
def lit(i: Int): T
def neg(t: T): T
def add(l: T, r: T): T
}
As is a set of three functions all returning the same type. Expressions are function applications
def tf0[T] given (e: Exp[T]): T =
import e._
add(lit(8), neg(add(lit(1), lit(2))))
and these can be interpreted with a given instance
given as Exp[Int] {
def lit(i: Int): Int = i
def neg(t: Int): Int = -t
def add(l: Int, r: Int): Int = l + r
}
tf0[Int] // 5
Essentially the interpretation is the implementation of the interface
Exp that is given (or in Scala 2 implicit) in the context.
So here we are moving from an algebraic structure expressed from an initial ADT to a final tagless version. (See the discussion on cstheory on what that is).
On Coalgebras
Now if we take the UserRepository example from The False Hope of Managing Effects with Tagless-Final in Scala, we have
trait UserRepository {
def getUserById(id: UserID): User
def getUserProfile(user: User): UserProfile
def updateUserProfile(user: User, profile: UserProfile): Unit
}
this is clearly (for anyone who has read some of Bart Jacobs' work starting with Objects and Classes Coalgebraically) a coalgebra on the state S of UserRepository.
A Coalgebra is the dual of an Algebra: the arrows are reversed.
Starting from a Functor F, and a specific type S an coalgebra
is a function S ⟹ F[S]
In the case of a user repository we can see this to be
S ⟹ (Uid → User) × (User → Profile) × (User × Profile → S)
Here the functor F(X) takes any type X to a 3-tuple of functions.
The coalgebra is such a functor F, a set of states S, and
a transition morphism S ⟹ F(S). We have 2 observational methods getUserById and getUserProfile and one state changing one updateUserProfile also known as a setter. By varying the type of states
we vary the coalgebra. If we look at all coalgebras on such a functor F, and the morphisms between them, we get a category of coalgebras. Of which the most important one is the final one which gives the structure of all observations on the coalgebras of that functor.
For more info on coalgebras and their relation to OO see the work by Bart Jacobs such as his Tutorial on (co)Algebras and (co)Induction or this Twitter thread.
Essentially we have a process such as a UserRepository or a Console that have state and can change state, whereas it does not make sense to think of change of state for a number.
Now it is true that in the Tagless Final example of UserRepository it is Genericised by a Functor F[_], like this:
trait UserRepository[F[_]] {
def getUserById(id: UserID): F[User]
def getUserProfile(user: User): F[UserProfile]
def updateUserProfile(user: User, profile: UserProfile): F[Unit]
}
Is that enough to change UserRepository into an algebra? It does in a way look like the functions all have the same range of type F[_], but does that really work? What if F is the Identity functor? Then we have the previous case.
Going the other way, from Final Tagless to an ADT, one should ask what would it be to have an ADT for UserRepository?
(I have written something like that myself to model commands to change a remote RDF database and found that really helpful, but I am not sure if this is correct mathematically.)
Further References
- The influential Haskell Typed Tagless Final Interpreters lecture notes
- A translation of that article for Scala (Dotty) Revisiting Tagless Final Interpreters
- A blog post From Object Algebras to Finally Tagless Interpreters makes the case that Object algebras are equivalent to Tagless Final.
- It cites the paper Extensibility for the Masses, practical extensibility with Object Algebras.
Two advantages claimed of Tagless Final are
- it makes testing easy: by moving to programming with interfaces one can easily create mock implementations of the interface to test code such as database access, IO, etc...
- it is extensible: one can easily extend an 'algebra' with new methods overcoming what is known as the expression problem. (The expression problem is nicely illustrated in the blog post From Object Algebras to Finally Tagless Interpreters).
The following looks like it could provide a clue:
The recent article Codata in Action claims that codata (a coalgebraic concept) is the bridge between functional and OO programming, and actually uses the visitor pattern described (also used in Extensibility for the Masses) to map between data and codata. see illustration. The claims for codata are the language agnostic representation of procedural abstraction (called modularity above), and the testability comes from the multiple implementations of an interface that Jacobs decribes with the category for a coalgebra.
F[A] => Ais about running your side effects, which is something you rarely want your generic library to do, as you want to do it yourself. It could be done viaCoalgebra, but why would you want to define abstraction and then use it only once at the end of the world? It doesn't refute usefulness of Coalgebra for F in general, just most common use cases don't need it, or simply uses some natural transformation instead. – Mateusz KubuszokF[A] => Athat define algebras is not the same thing as theunsafeRun:: IO => Aorgeton a future. I'll try to make that clearer. – Henry Story