Skip to content

Instantly share code, notes, and snippets.

@louy2
Last active July 3, 2020 08:43
Show Gist options
  • Save louy2/d62c289679ffd85dc70e7e6abd81672f to your computer and use it in GitHub Desktop.
Save louy2/d62c289679ffd85dc70e7e6abd81672f to your computer and use it in GitHub Desktop.
Experiment with tagless final in Rust
// 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>());
}
#![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))));
}
#![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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment