# Tagless Final: Haskell & Python

###### tags: `study`

## What is Tagless Final?

Tagless final is a representation of embedded DSLs, usually used within a typed metalanguage like Haskell or OCaml. It was introduced in the following paper: https://okmij.org/ftp/tagless-final/JFP.pdf.

## Which Problems Does It Solve?

For a basic representation of a typed DSL in a typed metalanguage, we fail to implement a simple interpreter:

-- De-Bruijn-indexed (numbered) variable type
data Var = VZ | VS Var

-- Algebraic data type for expressions
-- For Pythonists: this is like a typing.Union
data Expression = Variable Var | Literal Bool | Lambda Exp | Apply Exp Exp

-- Basic expression
test1 = Apply (Lambda (Variable VZ)) (Literal true)

-- Symbol value lookup
symLookup :: [a] -> Var -> a
symLookup (x:env) VZ = x
symLookup (_:env) (VS v) = symLookup env v 

-- This simple eval fails as the return type depends on the input
-- eval0 :: [Bool] -> Expression -> ???
eval0 env (Variable v) = symLookup env v
eval0 env (Literal b) = b
eval0 env (Lambda e) = \x -> eval0 (x:env) e
eval0 env (Apply e1 e2) = (eval0 env e1) (eval0 env e2)

A common solution is to introduce a parametrized universal type. E.g. in this case

data Universal = UniLiteral Bool | UniFunc (Universal -> Universal)

This allows to write the following interpreter

eval :: [Universal] -> Expression -> Universal
eval env (Variable v) = symLookup env v
eval env (Literal b) = UniLiteral b
eval env (Lambda e) = UniFunc (\x -> eval (x:env) e)
eval env (Apply e1 e2) = case eval env e1 of UniFunc f -> f (eval env e2)

Now `eval [] test1` works, however it returns `UniLiteral True`, that is a _tagged_ value. Further, we can give the interpreter invalid representations like `Apply (Literal True) (Literal False)` which fails with a non-exhaustive pattern matching error. Also open terms like `Apply (Lambda (Variable (VS VZ))) (Literal True)` fail with an error during variable lookup. This situation, that is, missing type information, possible representation of invalid terms and late failure (at interpretation time), is unsatisfactory. As a last concern, the AST definition by a algebraic data type is not extensible. We can not extend the language without modifying the original AST definition.

## How Does It Work (in Haskell)?

Instead of representing the program in an abstract syntax tree (called _initial_ encoding for whatever reason), the program is represented by functions (called _final_ encoding for whatever reason). E.g.

varZ env = fst env
varS vp env = vp (snd env)
-- Limit literals to Bool
literal :: Bool -> a -> Bool
literal v env = v
lambda e env = \x -> e (x, env)
apply e1 e2 env = (e1 env) (e2 env)

-- Return type is correctly derived as Bool
testf1 = apply (lambda varZ) (literal True)

Evaluation using `testf1 ()` correctly returns an _untagged_ `True`. Further, this approach fails at compilation time for invalid expressions and allows for correct partial evaluation. For example, `apply (literal True) (literal False)` fails to compile due to a type error and the evaluation of `lambda varZ`, `(lambda varZ) ()`, correctly returns a function.

The tricky part is now to generalize this approach, such that the same representation can be evaluated or transformed using different interpreters.
The solution in Haskell is based on type classes (modules in OCaml). The definition of the language syntax and looks as follows:

class Symantics repr where
    literal :: Bool -> repr Bool
    lambda :: (repr a -> repr b) -> repr (a -> b)
    apply :: repr (a -> b) -> repr a -> repr b

-- Definition of an expression
testf1 = apply (lambda (\x -> x)) (literal True)

An interpreter is then defined as an instance of this type class:

-- The interpreter type
data R a = R { eval :: a }

-- Definition of the interpreter functionality
instance Symantics R where
    literal = R
    lambda f = R $ eval . f . R
    apply f x = R $ (eval f) (eval x)

-- Example evaluation
testf1ev = eval testf1

Similarly, interpreters can be written that return text representation of the program. Slightly more involved, transformations can be implemented as interpreters that “return” another interpreter. A dummy transformer looks for example like this:

-- Data type of our dummy transformer, just keeps what was there before
data T0 repr a = T0 { t0 :: repr a }

-- Implementation of the transforation, note that the function names on the left and on the right are NOT referencing the same functions/overloads!
instance Symantics repr => Symantics (T0 repr) where
    -- Type signatures for improved clarity (not required)
    literal x :: Bool -> T0 repr Bool
    literal x = T0 $ literal x
    
    lambda :: (T0 repr a -> T0 repr b) -> T0 repr (a -> b)
    lambda f = T0 $ lambda $ t0 . f . T0
    
    apply :: T0 repr (a -> b) -> T0 repr a -> T0 repr b
    apply f x = T0 $ apply (t0 f) (t0 x)
    
-- Transform `testf1` by t0 and then evaluate
testf1t0ev = eval $ t0 testf1

So this interpreter is in the type class `Symantics` and thus can interpret any valid program. The type system of the metalanguage (Haskell) ensures that all our transformations return correct representation in our defined language! Of course we still can implement transformations that return rubbish, but only rubbish that is valid in our language.

The system further allows for great extensibility. For example, we can easily add symbols to our language without touching any existing code:

class Symantics repr => SymanticsWithSymbols repr where
    sym :: String -> repr Bool

All our transformations have just to be updated to work with the newly added entity, but then just work fine. The update for our dummy transform for example is just:

instance SymanticsWithSymbols repr => SymanticsWithSymbols (T0 repr) where
    sym x = T0 $ sym x

Note that this code can be put anywhere, _we do not need to touch any existing code_. That is, we can also easily extend a language that is defined within a library without touching the library code. All existing library functionality still works when we tell it to work with our extended language. So something like that works:

-- Import eval function from basic DSL
import SomeLib.BasicDSL (eval)
-- Load boolean `and` functionality from extension
import ExtendedLib.ExtendedDSL (and)

-- Some expression using the extensions
ex = apply (lambda (\x -> and x True))) True
-- Can still be evaluated with the `eval` function from the base language!
res = eval ex

The only disadvantage is probably that the code is not easily understandable if you are not used to the common patterns. Implementing common transformations requires a different approach than the common AST-based “tagged initial” representations.

If you would like to see a full and slightly more complex example including working transformations, see https://github.com/fthaler/lambda-calculus-dsl-haskell.

## Does It Work in Python?

Yes and no. Of course, programs can also be represented as functions instead of AST nodes, e.g.

def test(s):
    return s.apply(s.lambda_(lambda x: x),  s.literal(True))

which then can be interpreted by any class/instance/module `s` that provides the required functions. Note that this explicit passing of the interpreter `s` was not required in Haskell. It is also possible to define an abstract base class, similar to the Haskell type class:

class Symantics(ABC):
   @abstractmethod
   def literal(self, x): ...
   @abstractmethod
   def lambda_(self, f): ...
   @abstractmethod
   def apply(self, f, x): ...

But obviously, we loose the type safety that we have in typed functional languages like Haskell or OCaml. To recover this, we would require something like

class Symantics(Generic[Repr]):
    @abstractmethod
    def literal(self, x: int) -> Repr[int]: ...
    @abstractmethod
    def lambda_(self, x: Callable[[Repr[A]], Repr[B]]) -> Repr[Callable[[A], B]]: ...
    @abstractmethod
    def apply(self, f: Repr[Callable[[A], B]], x: Repr[A]) -> Repr[B]: ...

But Currently, there is no support of higher-kinded type variables (that is `Repr`, `Repr[A]`) in Python (see https://github.com/python/typing/issues/548). So we loose the type safety as an argument for the tagless final representation. Also, the very first example of a simple AST-based interpreter that fails in typed functional languages where each function has to have a single return type, works well in Python. We can easily define functions that return values of different types depending on the input.

The initial example that fails in Haskell, works better in Python:

@dataclass
class Var: ...

@dataclass
class VZ(Var): ...

@dataclass
class VS(Var):
    var: Var

@dataclass
class Expression: ...

@dataclass
class Variable(Expression):
    var: Var

@dataclass
class Literal(Expression):
    val: bool

@dataclass
class Lambda(Expression):
    val: Expression

@dataclass
class Apply(Expression):
    # Note: we can use `Lambda` for f, which allows type checkers (like mypy)
    # to fail on some expressions that only throw a late error in Haskell
    f: Lambda
    x: Expression

def sym_lookup(env: list[bool], v: Var) -> bool:
    assert env
    if isinstance(v, VZ):
        return env[0]
    assert isinstance(v, VS)
    return sym_lookup(env[1:], v.var)

def eval0(env: list[bool], e: Expression):
    if isinstance(e, Variable):
        return sym_lookup(env, e.var)
    if isinstance(e, Literal):
        return e.val
    if isinstance(e, Lambda):
        return lambda x: eval0([x] + env, e.val)
    if isinstance(e, Apply):
        return eval0(env, e.f)(eval0(env, e.x))

test1 = Apply(Lambda(Variable(VZ())), Literal(True))
# Correctly returns an untagged bool!
test1ev = eval0([], test1)
# This invalid expression is correctly catched by a type checker!
test2 = Apply(Literal(True), Literal(False))
# This one still fails during evaluation...
test3 = Apply(Lambda(Variable(VS(VZ()))), Literal(True))

So what about extensibility? In contrast to a non-extensible algebraic data type of a typed functional language, we can easily extend our language by just defining new AST nodes deriving from the base class (`Expression`).
Further, the extension mechanism of a tagless final implementation is less flexible than in Haskell. To make the example from above work in Python, e.g.

# Import eval function from basic DSL
from some_lib.basic_dsl import eval_
# Load boolean `and` functionality from extension
from extended_lib.extended_dsl import and_

# Some expression using the extensions
def ex(s):
    return apply(lambda_(lambda x: and_(x, True)), True)

# This is only possible with some monkey-patching of eval!
res = eval_(ex)

our extension would have to monkey-patch the `eval_` function provided by the base library. This is of course a bad idea, as it breaks as soon as we have multiple extensions. But if each extension brings its own evaluation function, the composability of these extensions is limited. So in summary, Python lacks the mechanisms available in Haskell that allow for great extensibility. Probably similar mechanisms could be implemented manually (like auto-registering extensions etc.), but there is no direct language support and there is no advantage of the tagless final approach over the AST approach here.

Additionally, the functional representation of programs in Python makes debugging and visualization more tedious and is probably not familiar to the average Python developer. Transformations in tagless final form in Python are probably much harder to grasp, due to the high-order functional style that is not so common in Python. Further, due to the missing type safety, it is easy to generate complete nonsense, which is impossible in the functional metalanguages as there only valid programs can be represented. A Python implementation of a basic DSL, closely following the Haskell implementation above can be found here: https://github.com/fthaler/lambda-calculus-dsl-python. Also note the additional complexity of the transformations compared to Haskell, which stem from the explicit passing of the interpreter classes to the expressions as required in Python.

## Summary

To my understanding, the tagless final representations of programs in typed functional metalanguages like Haskell and OCaml is pretty awesome: it restricts representable programs to all valid programs, it catches all type errors at compile time and it allows for great extensibility and composability of extensions.

On the other hand, the representation looses all its benefit on the Python side: missing higher-kinded generic types disallow a type-checkable implementation, extensibility is not improved over the AST-approach, debuggability is hindered by the functional representation and the implementation of transformations is less intuitive due to appearance of many higher-order functions. And last but not least, the time to get started on a tagless final DSL representation code is for sure much higher for the average Python developer than on an AST-based code.