Thread by @bblfish

Looking around for how finally tagless might be different on #Dotty I found this talk that shows a number of applications of implicit function types.
slideslive.com/38908156/appli… #Scala3

He has written a post on this too that goes into greater detail "Revisiting Tagless Final Interpreters" gist.github.com/OlivierBlanvil…

A nice easy to read overview of Tagless Final in the context of a number of other technologies - ZIO, FreeMonads, ... - by @adamwarski
blog.softwaremill.com/final-tagless-…

@adamwarski A very readable article by @jdegoes that gives the advantages of Final Tagless. Advantages:
* effect type indirection
* program to interfaces which leads to testability (with a nice example)
* effect parametric reasoning
dzone.com/articles/the-f…

@adamwarski @jdegoes One criticism of final tagless is that as used, it is not really used as the final encoding of ADTs - see "Revisiting Tagless Final Interpreters" above. Are there any laws for a Console trait? No.
(But can any programming language provide one?)
dzone.com/articles/the-f…

@adamwarski @jdegoes "Code to the interface" does have a Category Theoretic background, but it comes not from algebras, but from coalgebras.
Colgebras help model state, and processes.
An early article that shows this with a bank account example, with equations on state
citeseerx.ist.psu.edu/viewdoc/downlo…

@adamwarski @jdegoes "inheritance ... will be understood dually to parametrization in algebraic specification"
"cofree constructions are 'best' restrictions, like free constructions are best extensions".
As #Scala combines FP and OO, one has to know of algebras and coalgebras.
citeseerx.ist.psu.edu/viewdoc/downlo…

@adamwarski @jdegoes I wonder how much confusion arises from this: When #typelevel Cats extends Applicative with Monad, it is increasing the number of models that fit. Whereas when we model a stateful system like a bank account to supersaver account, inheritance reduces the number of models. #scala

@adamwarski @jdegoes If you look at this definition of a cofree construction it looks a bit daunting.

https://twitter.com/bblfish/status/1172451762072117248

But, as object oriented programmers we use cofree constructions all the time when we extend subclasses with new methods and attributes. #Java #Scala

@adamwarski @jdegoes The Forgetful Functor F from a class to its superclass (considered as 2 categories of coalgebras) forgets the structure of the subclass. This F induces a cofree subclass functor going the other way.
OO folks you are doing CT everyday too :-)
#Java #Scala

@adamwarski @jdegoes * The Forgetful Functor between Monoids and Set has as left adjoint the Free Monoids: Lists.
* The Forgetful Functor between a class C and its superclass S (qua coalgebras) has as right adjoint the coFree Functor that takes any implementation of S to the minimal one in C.