A continuation for Object Algebra.

# Final Tagless

Still the expression problem, without stronger type system, this is as far as we can go. But what if we have some extra bonus ? We will show it with Haskell below.

## Initial

“Initial” is from initial algebra, which is an initial object of F-Algebra category of a given endofunctor-F. Here the initial approach is to encode the expression as values of an ADT :

An instance of this `Exp` can be :

We can implement its evaluator and printer as

But we can not add new variants to it like the naïve implementation we mentioned above.

## Final

The final approach is quite different. If all we ever need is the value of an expression, we can represent the term in our arithmetic language by its value, or by a Haskell expression that computes that value.

A typeclass is perfect for the situation:

and the same example can be expressed with a different type signature

What we need now is just different `ExpSYM` instance :

and their evaluator :

`eval tf1` gets `5` and `view tf1` gets `(8 + (- (1 + 2)))`

### Extensibility of final embedding

Like object algebra, final embedding can extend easily for data variants :

and the following expression will have another restriction on its polymorphic type

## Pattern match in final embedding

Consider an operation of pushing `Neg` down to the leaf in the initial embedding:

but we can not match such structure directly in final approach, we need to find another way.

The former instances we implemented in final approach have something in common, is that all the information it needs is inside itself, which is , in other words , compositional. But `push_neg` is not, it needs extra information from above. So here we offer such information explicitly :

and finally :

## Relation between initial and final

We can find the isomorphism between `Exp` and `ExpSYM a`

With these two morphisms, we can build `push_neg'` in another way :

## Why Tagless ?

Type tag may leads to problem. Here is an example of a simple typed lambda calculi :

`Var` is De Bruijn index representing the parameter of lambda expression.

And here is an example

If we try to write an evaluator, we will see that the evaluator may raise runtime error (or inexhaustive pattern-match). At least we should write a type checker and use universe type to get the result of an `Exp` .

But are we able to use type-system to restrict `Exp` and ensure the polymorphism of the result, without using dependent type ? Fortunately, there is such a way.

## Initial and Final Tagless Interpreter

Algebraic data type is too loose to ensure the result of `Exp` is safe, so like what we do in “Theorem Proving in Haskell”, we can use Genialized Algebraic Data Types (GADTs) to remove ill-typed expressions.

As usual, we start with the initial embedding :

Now we have :

And this time a straight-forward evaluator will work fine :

Initial solution is based on GADTs, which is a “lightweight dependent types”. But is that really necessary for a tagless interpreter ?

Here comes the final approach.

## Finally Tagless Interpreter

We write `tf1 = a (l vz) (b True)` as our final embedded expression. As we have found the isomorphism between initial and final, we can try to write the final interpreter just as the initial one :

With the definition above, giving `tf1` an environment `()` and it will get the result `True` as expected.

These five lines are the entire final interpreter with no type tags. It associates the type of the language with Haskell type system. The signature of these functions can be inferred as :

Now we rebuild a typeclass `Symantics` to describe the typed lambda calculi with integer addition :

`repr` here is a higher-order type `* -> * -> *` , the first type is the environment and the second is the result type of the expression.

Now we can implement the instance for `(->)`

## Replace De Bruijn index with native lambda

De Bruijn index is very abstract and actually it is not necessary. Haskell built-in type system is strong enough to construct legal lambda terms.

Instead of retrieve parameters from environment, we can store a Haskell lambda term in it :

Now we can implement something more :

Instance is trivial for most of them but the fix, we will need `fix :: (a -> a) -> a` in Haskell

## Conclusion

Final tagless or object algebra solves the problem of polymorphism of an ADT, allowing easily extension without modification on the legacy code by encoding the object language term into the host language term in a composition way.