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 FAlgebra category of a given endofunctorF. Here the initial approach is to encode the expression as values of an ADT :
1  data Exp 
An instance of this Exp
can be :
1  ti1 :: Exp 
We can implement its evaluator and printer as
1  eval :: Exp > Int 
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:
1  class ExpSYM repr where 
and the same example can be expressed with a different type signature
1  tf1 :: ExpSYM a => a 
What we need now is just different ExpSYM
instance :
1  instance ExpSYM Int where 
and their evaluator :
1  view :: String > String 
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 :
1  class MulSYM exp where 
and the following expression will have another restriction on its polymorphic type
1  tfm1 :: (MulSYM a, ExpSYM a) => a 
Pattern match in final embedding
Consider an operation of pushing Neg
down to the leaf in the initial embedding:
1  push_neg :: Exp > Exp 
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 :
1  data Context = Positive  Negative 
and finally :
1  push_neg' :: ExpSYM a => a 
Relation between initial and final
We can find the isomorphism between Exp
and ExpSYM a
1  instance ExpSYM Exp where 
With these two morphisms, we can build push_neg'
in another way :
1  push_neg' = finalize . push_neg . initialize 
Why Tagless ?
Type tag may leads to problem. Here is an example of a simple typed lambda calculi :
1  data Exp 
Var
is De Bruijn index representing the parameter of lambda expression.
And here is an example
1  ti1 :: Exp 
If we try to write an evaluator, we will see that the evaluator may raise runtime error (or inexhaustive patternmatch). 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 typesystem 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 illtyped expressions.
As usual, we start with the initial embedding :
1 

Now we have :
1  ti1 :: Exp env Bool 
And this time a straightforward evaluator will work fine :
1  eval :: env > Exp env t > t 
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 :
1  vz (t, _) = t 
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 :
1  b :: t > env > t 
Now we rebuild a typeclass Symantics
to describe the typed lambda calculi with integer addition :
1  class Symantics repr where 
repr
here is a higherorder type * > * > *
, the first type is the environment and the second is the result type of the expression.
Now we can implement the instance for (>)
1  instance Symantics (>) where 
Replace De Bruijn index with native lambda
De Bruijn index is very abstract and actually it is not necessary. Haskell builtin 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 :
1  class Symantics repr where 
Now we can implement something more :
1  class MulSYM repr where 
Instance is trivial for most of them but the fix, we will need fix :: (a > a) > a
in Haskell
1  newtype Id a = Id {runId :: a} 
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.