Tagless Final is a style of programming derived first by Oleg Kiselyov to be used in ML for embedding domain specific languages (DSL), but from ML point of view every API is a DSL so really it is a style to write APIs ergonomically.

The name "Tagless Final" is probably foreign to most programmers. "Tagless" means without tag, which is usually an allocation to store the abstract syntax tree of the language. Without this allocation means less overhead. To do so, instead of constructors, which is theorized by the "initial" algebra of the λ-calculus, this style uses functions, which is theorized by the coalgebra of the λ-calculus, and thus named "final". No, I do not understand what I just wrote.

What is fun with this style is that it achieves the best separation of specification and implementation bar none. In Rust each part of the specification is a trait, like so:

trait Prim {
    fn int(v: i64) -> Self;
    fn bool(v: bool) -> Self;
}
trait AddOp {
    fn add(x: Self, y: Self) -> Self;
}
trait IfOp {
    fn leq(x: Self, y: Self) -> Self;
    fn if_<'a>(cond: Self, x: Box<dyn Fn() -> Self>, y: Box<dyn Fn() -> Self>) -> Self;
}

The program is then written only in terms of the traits:

fn prog<S>() -> S
where
    S: Prim + AddOp + IfOp
{
    S::if_(
        S::leq(S::int(5), S::int(9)),
        Box::new(|| S::add(S::int(3), S::int(8))),
        Box::new(|| S::int(7)),
    )
}

When executing the program, you just supply the implementation as the type parameter:

fn main() {
    println!("{:?}", prog::<P>());
    println!("{:?}", prog::<R>());
}

Here I implemented P as a pretty printer and R as a simple evaluator. The printed results are:

P("if 5 <= 9 { 3 + 8 } else { 7 }")
Int(11)

This style also is claimed to have solved "the Expression Problem", a dilemma created by module boundaries and orphan rules which have forced us to trade-off between a closed set of operators for stricter checks or an open set of operators for easier extensions. With this style, sets of operators and interpreters can be defined at will, while the set of operators is closed by the trait bounds attached to the program. Best of both worlds! Hopefully.

Unfortunately when used in Rust, this style cannot reach its full potential. In an ML with higher kinded type (HKT), Tagless Final can do the following things that in Rust I have not found a way to do:

• Enforce the types of the operators
• Enforce the parametricity of the operators
• No tags for primitive types in the implementation

If you are curious, the code is in the gist below.