[tel]

Note that there's a bit of a pun here. "Finally" tagless isn't really any less initial than free monads are. The final encoding would give us something codata like, not just described via a typeclass. That said, both are still "initial" as in "initial algebra".

[eru]

Interesting. Could you expand on that, please?

[tel]

"Initial" usually means "the initial algebra over a functor". This means that for some functor f the algebra `i : f (Initial f) -> Initial f` is initial in the category of f algebras. This means that for any X and `g : f X -> X` there's a universal function `universal g : Initial f -> X` such that `g . fmap (universal g) = universal g . i` at type `f (Initial f) -> X`. Or, we have a function

    universal : (f x -> x) -> (Initial f -> x)

and we can actually define Initial in this way

    universal' : Initial f -> (f x -> x) -> x

    newtype Initial f = Initial { universal' :: forall x . (f x -> x) -> x }

In "strict Haskell" where we can act only finitely, we construct values of `Initial f` only by slapping finitely many layers of `f` on top of one another. For instance, when `f` is `data ConsF x = NilF | ConsF Int x` we can make a list [1, 2, 3] like

    Initial $ \join -> 
      let nil   = join NilF
          a : x = join (ConsF a x)
      in 1 : 2 : 3 : nil

In other words, Initial things are described by their construction.

Clearly, this relates directly to initial objects constructed via, e.g., Free, since it does roughly the same thing. Free emphasizes the notion of layering things atop one another. In Lazy Haskell we can still use this layering to construct non-initial objects (more to come below) but if Free were transported to Strict Haskell it would clearly only construct initial things.

---

So what about Finally Tagless?

    class List l where
      nil :: l
      cons :: Int -> l -> l

We're still going to be constructing values of `List l => l` by application of finite layers! If anything, we're more stuck to this process now.

    cons 1 (cons 2 (cons 3 nil))) :: List l => l

If we swap this out for explicit dictionary passing we can see that we're missing an argument like

    data ListD l = ListD { nil :: l, cons :: Int -> l -> l }

    \d -> cons d 1 (cons d 2 (cons d 3 nil)) :: ListD l -> l

and also that `ListD l` is equivalent to `ConsF l -> l`. It's really the same thing as the free method and is again operating initially.

---

So what does it take to make something "final"? A final coalgebra of `f` would be an object `i : Final f -> f (Final f)` such that for any X and coalgebra `g : X -> f X` we have `universal g : X -> Final f` such that `i . universal g = fmap (universal g) . g` at type `X -> f (Final f)`. Or,

     universal : (x -> f x) -> x -> Final f

which again can be used to define `Final f`

    data Final f where
      Final :: (x, x -> f x) -> Final f

No longer can we define things by how they are constructed, now we must define them by how they are viewed. This opens up the doors to new kinds of structures, even in "Strict Haskell"

    natsFrom :: Int -> Final ConsF
    natsFrom n0 = Final (n0, \n -> ConsF n (natsFrom (n + 1)))

[eru]

Thanks!