Experiment with tagless final in Rust

not_tagless_final.rs

// 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>());
}

not_tagless_final_take2.rs

#![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))));
}

not_tagless_final_take3.rs

#![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