title: Is it ok to use Tagless Final (Object Algebras) on coalgebras?
body: <h2>Background</h2>
  
  <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>Asking the Question <a href="https://cstheory.stackexchange.com/questions/45565/what-category-are-tagless-final-algebras-final-in/45566">What Category are Tagless Final Algebras Final In</a> on CS-Theory Stack Exchange I got a very good answer pointing to this blog post <a href="http://prl.ccs.neu.edu/blog/2017/09/27/final-algebra-semantics-is-observational-equivalence/" rel="nofollow noreferrer">Final Algebra Semantics is Observational Equivalence</a>. So these are indeed final algebras, but not in the same category of algebras as the initial one....</p>
  
  <h2>Question</h2>
  
  <p>Yet, when we look at how <em>final tagless</em> is <strong>used</strong>, we find that it is very often applied for things that look like coalgebras. See for example the two examples of a <code>Console</code> or a <code>UserRepository</code> in part 1 of <a href="https://dzone.com/articles/the-false-hope-of-managing-effects-with-tagless-fi" rel="nofollow noreferrer">The False Hope of Managing Effects with Tagless-Final in Scala</a>. </p>
  
  <p>So instead of having Algebras which in category theory are expressed with endofunctors <code>F</code> as maps of the form <code>F(X) ⟹ X</code>, it looks like many use <code>final tagless</code> with Coalgebras which are maps <code>X ⟹ F(X)</code>, and represent processes. Are these really the same thing? Or is something else going on here?</p>
  
  <h2>ADTs and Final Tagless</h2>
  
  <h3>On Algebras</h3>
  
  <p>Let's start by the explanations of final tagless given by Olivier Blanvillain's <a href="https://gist.github.com/OlivierBlanvillain/48bb5c66dbb0557da50465809564ee80" rel="nofollow noreferrer">Scala translation of examples taken from coursework on  in Haskell</a>. One notices that this starts with an Algebraic Data Type that is indeed the archetype of an Algebraic structure: a Group.</p>
  
  <p>In category a group can be built out of a the Polynomial Functor 
  <code>F[X] = X×X + X + 1</code> 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 <code>F[A] ⟹ A</code>. The most widely known group is the set of positive and negative natural numbers and 0 denoted ℤ, and so our algebra is:</p>
  
  <pre><code>ℤ×ℤ + ℤ + 1 ⟹ ℤ 
  </code></pre>
  
  <p>The algebra can be decomposed into 3 function <code>+: ℤ×ℤ ⟹ ℤ</code>, <code>-: ℤ ⟹ ℤ</code> and the constant <code>zero: 1 ⟹ ℤ</code>. 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.</p>
  
  <p>The initial algebra is the free one  which allows one to build all the structure without ever loosing any information. In <a href="https://dotty.epfl.ch/docs/reference/enums/adts.html" rel="nofollow noreferrer">Scala 3</a> we can build the initial algebra for a group like this: </p>
  
  <pre class="lang-scala prettyprint-override"><code>enum IExp {
     case Lit(i: Int)
     case Neg(e: IExp)
     case Add(r: IExp, l: IExp)
  }
  </code></pre>
  
  <p>And we can build a simple structure using it:</p>
  
  <pre><code>import IExp._
  val fe: IExp = Add(Lit(8), Neg(Add(Lit(1), Lit(2))))
  </code></pre>
  
  <p>The <code>fe</code> structure can then be interpreted by creating functions <code>IExp =&gt; Int</code> or <code>IExp =&gt; String</code>, 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 <code>String</code> or <code>Int</code>). This morphism is known as a fold. (See the 1997 book <a href="https://themattchan.com/docs/algprog.pdf" rel="nofollow noreferrer">The Algebra of Programming, by Richard Bird and Oege de Moor</a>)</p>
  
  <p>In Tagless final this is transformed into the trait</p>
  
  <pre class="lang-scala prettyprint-override"><code>trait Exp[T] {
    def lit(i: Int): T
    def neg(t: T): T
    def add(l: T, r: T): T
  }
  </code></pre>
  
  <p>As is a set of three functions all returning the same type.
  Expressions are function applications</p>
  
  <pre class="lang-scala prettyprint-override"><code>def tf0[T] given (e: Exp[T]): T =
      import e._
      add(lit(8), neg(add(lit(1), lit(2))))
  </code></pre>
  
  <p>and these can be interpreted with a given instance</p>
  
  <pre><code>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
  </code></pre>
  
  <p>Essentially the interpretation is the implementation of the interface
  <code>Exp</code> that is <code>given</code> (or in Scala 2 <code>implicit</code>) in the context.</p>
  
  <p>So here we are moving from an algebraic structure expressed from an initial ADT to a final tagless version. (See the discussion on <a href="https://cstheory.stackexchange.com/questions/45565/what-category-are-tagless-final-algebras-final-in">cstheory on what that is</a>).</p>
  
  <h3>On Coalgebras</h3>
  
  <p>Now if we take the <code>UserRepository</code> example from <a href="https://dzone.com/articles/the-false-hope-of-managing-effects-with-tagless-fi" rel="nofollow noreferrer">The False Hope of Managing Effects with Tagless-Final in Scala</a>, we have</p>
  
  <pre class="lang-scala prettyprint-override"><code>trait UserRepository {
    def getUserById(id: UserID): User
    def getUserProfile(user: User): UserProfile
    def updateUserProfile(user: User, profile: UserProfile): Unit
  }
  </code></pre>
  
  <p>this is clearly (for anyone who has read some of Bart Jacobs' work starting with <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.54.7619&amp;rep=rep1&amp;type=pdf" rel="nofollow noreferrer">Objects and Classes Coalgebraically</a>) a coalgebra on the state S of <code>UserRepository</code>.
  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 <code>S ⟹ F[S]</code></p>
  
  <p>In the case of a user repository we can see this to be </p>
  
  <pre><code>S ⟹ (Uid → User) × (User → Profile) × (User × Profile → S) 
  </code></pre>
  
  <p>Here the functor <code>F(X)</code> takes any type <code>X</code> to a 3-tuple of functions. 
  The coalgebra is such a functor F, a set of states S, and
  a transition morphism <code>S ⟹ F(S)</code>.  We have 2 observational methods <code>getUserById</code> and <code>getUserProfile</code> and one state changing one <code>updateUserProfile</code> 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.</p>
  
  <p>For more info on coalgebras and their relation to OO see the work by Bart Jacobs such as his <a href="https://pdfs.semanticscholar.org/40bb/e9978e2c4080740f55634ac58033bfb37d36.pdf" rel="nofollow noreferrer">Tutorial on (co)Algebras and (co)Induction</a> or <a href="https://twitter.com/bblfish/status/1172265457153392640" rel="nofollow noreferrer">this Twitter thread</a>.</p>
  
  <p>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.</p>
  
  <p>Now it is true that in the Tagless Final example of UserRepository it is Genericised by a Functor <code>F[_]</code>, like this:</p>
  
  <pre class="lang-scala prettyprint-override"><code>trait UserRepository[F[_]] {
    def getUserById(id: UserID): F[User]
    def getUserProfile(user: User): F[UserProfile]
    def updateUserProfile(user: User, profile: UserProfile): F[Unit]
  }
  </code></pre>
  
  <p>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.</p>
  
  <p>Going the other way, from Final Tagless to an ADT, one should ask what would it be to have an ADT for <code>UserRepository</code>? 
  (I have written something like that myself to model commands to change <a href="https://github.com/read-write-web/rww-play/blob/dev/app/rww/ldp/LDPCommand.scala" rel="nofollow noreferrer">a remote RDF database</a> and found that really helpful, but I am not sure if this is correct mathematically.) </p>
  
  <h2>Further References</h2>
  
  <ul>
  <li>The influential Haskell <a href="http://okmij.org/ftp/tagless-final/course/lecture.pdf" rel="nofollow 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="nofollow 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="nofollow 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="nofollow noreferrer">Extensibility for the Masses, practical extensibility with Object Algebras</a>.</li>
  </ul>
  
  <p>Two advantages claimed of Tagless Final are</p>
  
  <ul>
  <li>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...</li>
  <li>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 <a href="https://oleksandrmanzyuk.wordpress.com/2014/06/18/from-object-algebras-to-finally-tagless-interpreters-2/" rel="nofollow noreferrer">From Object Algebras to Finally Tagless Interpreters</a>).</li>
  </ul>
  
  <p>The following looks like it could provide a clue:</p>
  
  <p>The recent article <a href="https://link.springer.com/chapter/10.1007/978-3-030-17184-1_5" rel="nofollow noreferrer">Codata in Action</a> claims that codata (a coalgebraic concept) is the bridge between functional and OO programming, and actually uses the visitor pattern described (also used in <a href="https://www.cs.utexas.edu/~wcook/Drafts/2012/ecoop2012.pdf" rel="nofollow noreferrer">Extensibility for the Masses</a>) to map between data and codata. <a href="https://twitter.com/bblfish/status/1173269815802441728" rel="nofollow noreferrer">see illustration</a>. 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.</p>