(Not) Finally Tagless in Rust

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.

	// http://okmij.org/ftp/tagless-final/JFP.pdf
	// Self is not HKT so cannot enforce term types
	trait Symantics {
	fn int(v: i64) -> Self;
	fn bool(v: bool) -> Self;
	// Cannot enforce that add takes int
	fn add(x: Self, y: Self) -> Self;
	// Cannot enforce that leq takes int and returns bool
	fn leq(x: Self, y: Self) -> Self;
	// Cannot enforce that cond is bool
	// Cannot enforce that term type in two branches are the same
	fn if_(cond: Self, x: Box<dyn Fn() -> Self>, y: Box<dyn Fn() -> Self>) -> Self;
	}
	#[derive(Debug)]
	struct P(String);
	impl Symantics for P {
	fn int(v: i64) -> Self {
	P(v.to_string())
	}
	fn bool(v: bool) -> Self {
	P(v.to_string())
	}
	fn add(x: Self, y: Self) -> Self {
	P(format!("{} + {}", x.0, y.0))
	}
	fn leq(x: Self, y: Self) -> Self {
	P(format!("{} <= {}", x.0, y.0))
	}
	fn if_<'a>(cond: Self, x: Box<dyn Fn() -> Self>, y: Box<dyn Fn() -> Self>) -> Self {
	P(format!("if {} {{ {} }} else {{ {} }}", cond.0, x().0, y().0))
	}
	}
	#[derive(Debug)]
	enum R {
	Int(i64),
	Bool(bool),
	}
	impl Symantics for R {
	fn int(v: i64) -> Self {
	R::Int(v)
	}
	fn bool(v: bool) -> Self {
	R::Bool(v)
	}
	fn add(x: Self, y: Self) -> Self {
	if let (R::Int(x), R::Int(y)) = (x, y) {
	R::Int(x + y)
	} else {
	panic!() // Have to panic since Int not enforced by HKT
	}
	}
	fn leq(x: Self, y: Self) -> Self {
	if let (R::Int(x), R::Int(y)) = (x, y) {
	R::Bool(x < y)
	} else {
	panic!() // Have to panic since Bool not enforced by HKT
	}
	}
	fn if_(cond: Self, x: Box<dyn Fn() -> Self>, y: Box<dyn Fn() -> Self>) -> Self {
	if let R::Bool(cond) = cond {
	if cond {
	(*x)()
	} else {
	(*y)()
	}
	} else {
	panic!()
	}
	}
	}
	fn prog<S>() -> S
	where
	S: Symantics
	{
	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)))
	}
	fn main() {
	println!("{:?}", prog::<P>());
	println!("{:?}", prog::<R>());
	}

view raw not_tagless_final.rs hosted with ❤ by GitHub

	#![allow(dead_code)]
	#![allow(non_snake_case)]
	/*
	let varZ env = fst env
	let varS vp env = vp (snd env)
	let b (bv:bool) env = bv
	let lam e env = fun x -> e (x,env)
	let app e1 e2 env = (e1 env) (e2 env)
	*/
	type Func<T, O> = Box<dyn FnOnce(T) -> O>;
	fn varZ<A, B>() -> Func<(A, B), A> {
	Box::new(|env| env.0)
	}
	fn varS<A, T1: 'static, T2: 'static>(vp: Func<T1, T2>) -> Func<(A, T1), T2> {
	Box::new(move |env| vp(env.1))
	}
	fn b<P>(bv: bool) -> Func<P, bool> {
	Box::new(move |_env| bv)
	}
	fn lam<A: 'static, B: 'static, T: 'static>(e: Func<(A, B), T>) -> Func<B, Func<A, T>> {
	Box::new(|env| Box::new(|x| e((x, env))))
	}
	fn app<T1: 'static + Copy, T2: 'static, T3: 'static>(
	e1: Func<T1, Func<T2, T3>>,
	e2: Func<T1, T2>,
	) -> Func<T1, T3> {
	Box::new(|env| e1(env)(e2(env)))
	}
	fn main() {
	let testf1 = app(lam(varZ()), b(true));
	println!("{}", testf1(()));
	let testf3 = app(lam(varS(varZ())), b(true));
	println!("{}", testf3((1, (2))));
	}

view raw not_tagless_final_take2.rs hosted with ❤ by GitHub

	#![allow(dead_code)]
	#![allow(non_snake_case)]
	#![allow(incomplete_features)]
	#![feature(generic_associated_types)]
	/*
	let b (bv:bool) env = bv
	let int (iv:int) env = iv
	let and b1 b2 env = b1 & b2
	*/
	type Func<T, O> = Box<dyn FnOnce(T) -> O>;
	trait Lang {
	type Repr<T>;
	fn b(bv: bool) -> Self::Repr<bool>;
	fn int(iv: i64) -> Self::Repr<i64>;
	fn and(b1: Self::Repr<bool>, b2: Self::Repr<bool>) -> Self::Repr<bool>;
	}
	use core::marker::PhantomData;
	struct B<P>(PhantomData<P>);
	impl<P: 'static + Copy> Lang for B<P> {
	type Repr<T> = Func<P, T>;
	fn b(bv: bool) -> Self::Repr<bool> {
	Box::new(move |_env| bv)
	}
	fn int(iv: i64) -> Self::Repr<i64> {
	Box::new(move |_env| iv)
	}
	fn and(b1: Func<P, bool>, b2: Func<P, bool>) -> Func<P, bool> {
	Box::new(move |env| b1(env) & b2(env))
	}
	}
	struct P;
	impl Lang for P {
	type Repr<T> = String;
	fn b(bv: bool) -> String {
	bv.to_string()
	}
	fn int(iv: i64) -> Self::Repr<i64> {
	iv.to_string()
	}
	fn and(b1: String, b2: String) -> String {
	format!("{} & {}", b1, b2)
	}
	}
	fn prog1<L>() -> L::Repr<bool>
	where
	L: Lang,
	{
	L::and(L::b(false), L::b(true))
	}
	// fn prog_with_error<L>() -> L::Repr<bool>
	// where
	// L: Lang,
	// {
	// L::and(L::int(3), L::b(true))
	// }
	fn main() {
	let test1_p = prog1::<P>();
	println!("{:?}", test1_p);
	let test1_b = prog1::<B<()>>()(());
	println!("{:?}", test1_b);
	}
	// TODO: De Brujin Indices

view raw not_tagless_final_take3.rs hosted with ❤ by GitHub