Gradually-Typed Lambda Calculus in type-level Rust

gistfile1.rs

mod gradual_types {
    use std::marker::PhantomData;

    use syntax::GroundType;

    pub mod syntax {
        use std::marker::PhantomData;

        pub trait Variable {}

        pub struct VarBox<V>(V);
        pub struct ConstBox<C>(C);

        impl<V> Variable for VarBox<V> where V: Variable {}

        pub trait GroundType {}
        pub trait Constant {}

        impl<C> Constant for ConstBox<C> where C: Constant {}

        pub trait Type {}
        pub struct Unknown;
        pub struct Fun<A, B> {
            _a: PhantomData<(A, B)>,
        }

        pub trait Expr {}

        impl<C> Expr for ConstBox<C> {}

        impl<X> Expr for VarBox<X> {}

        pub struct Apply<F, A> {
            _t: PhantomData<(F, A)>,
        }

        impl<F, A> Expr for Apply<F, A>
        where
            F: Expr,
            A: Expr,
        {
        }

        pub struct Lambda<X, T, E> {
            _t: PhantomData<(X, T, E)>,
        }

        impl<X, T, E> Expr for Lambda<X, T, E>
        where
            X: Variable,
            T: Type,
            E: Expr,
        {
        }

        impl<T: GroundType> Type for T {}
        impl Type for Unknown {}

        impl<A, B> Type for Fun<A, B>
        where
            A: Type,
            B: Type,
        {
        }
    }

    mod standard_lib {
        use super::syntax::{Constant, GroundType};

        pub struct BoolType;
        pub struct NatType;

        impl GroundType for BoolType {}
        impl GroundType for NatType {}

        pub trait Bool {}
        pub struct True;
        pub struct False;

        impl Bool for True {}
        impl Bool for False {}

        impl Constant for True {}
        impl Constant for False {}
    }

    pub mod type_consistency {
        use std::marker::PhantomData;

        use super::syntax::{Fun, Unknown};

        pub trait TypeConsistent<A, B> {}

        pub struct CRefl<T> {
            _t: PhantomData<T>,
        }

        impl<T> TypeConsistent<T, T> for CRefl<T> {}

        pub struct CUnR<T> {
            _t: PhantomData<T>,
        }

        impl<T> TypeConsistent<T, Unknown> for CUnR<T> {}

        pub struct CUnL<T> {
            _t: PhantomData<T>,
        }

        impl<T> TypeConsistent<Unknown, T> for CUnL<T> {}

        pub struct CFun<S1T1, S2T2, S1, T1, S2, T2> {
            _t: PhantomData<(S1T1, S2T2, S1, T1, S2, T2)>,
        }

        impl<S1T1, S2T2, S1, T1, S2, T2> TypeConsistent<Fun<S1, S2>, Fun<T1, T2>>
            for CFun<S1T1, S2T2, S1, T1, S2, T2>
        where
            S1T1: TypeConsistent<S1, T1>,
            S2T2: TypeConsistent<S2, T2>,
        {
        }

        mod tests {
            use std::default;

            use crate::lambda_calculus::gradual_types::{
                standard_lib::NatType,
                syntax::{Fun, Unknown},
            };

            use super::{CFun, CRefl, CUnR, TypeConsistent};

            fn check_consistency<Proof, A, B>()
            where
                Proof: TypeConsistent<A, B>,
            {
                println!(
                    "{} ~ {}",
                    std::any::type_name::<A>(),
                    std::any::type_name::<B>()
                );
            }

            #[test]
            fn return_type_erased() {
                check_consistency::<
                    CFun<CRefl<NatType>, CUnR<NatType>, NatType, NatType, NatType, Unknown>,
                    Fun<NatType, NatType>,
                    Fun<NatType, Unknown>,
                >();
            }
        }
    }

    mod clean_type_checking {
        use std::marker::PhantomData;

        use crate::lambda_calculus::{
            gradual_types::syntax::Type,
            type_set::{Cons, Contains, Set},
        };

        use super::{
            syntax::{Apply, ConstBox, Constant, Expr, Fun, Lambda, Unknown, VarBox, Variable},
            type_consistency::TypeConsistent,
        };

        pub trait TypeContext: Set {}

        impl<T> TypeContext for T where T: Set {}

        pub trait VarHasType<G, X, T> {}

        impl<Proof, G, X, T> VarHasType<G, X, T> for Proof
        where
            G: Set,
            X: Variable,
            T: Type,
            Proof: Contains<G, (X, T)>,
        {
        }

        pub trait ConstHasType<D, C, T> {}

        impl<Proof, D, C, T> ConstHasType<D, C, T> for Proof
        where
            D: Set,
            C: Constant,
            T: Type,
            Proof: Contains<D, (C, T)>,
        {
        }

        pub trait ExprHasType<G, E, T>
        where
            G: TypeContext,
            E: Expr,
            T: Type,
        {
        }

        pub struct GVar<VarProof, G, X, T> {
            _t: PhantomData<(VarProof, G, X, T)>,
        }

        impl<VarProof, G, X, T> ExprHasType<G, VarBox<X>, T> for GVar<VarProof, G, X, T>
        where
            X: Variable,
            T: Type,
            G: TypeContext,
            VarProof: VarHasType<G, X, T>,
        {
        }

        pub struct GConst<ConstProof, D, G, C, T> {
            _t: PhantomData<(ConstProof, D, G, C, T)>,
        }

        impl<CProof, D, G, C, T> ExprHasType<G, ConstBox<C>, T> for GConst<CProof, D, G, C, T>
        where
            C: Constant,
            T: Type,
            G: TypeContext,
            D: TypeContext,
            CProof: ConstHasType<D, C, T>,
        {
        }

        pub struct GLam<EProof, G, X, S, E, T> {
            _t: PhantomData<(EProof, G, X, S, E, T)>,
        }

        impl<EProof, G, X, S, E, T> ExprHasType<G, Lambda<VarBox<X>, S, E>, Fun<S, T>>
            for GLam<EProof, G, X, S, E, T>
        where
            G: TypeContext,
            X: Variable,
            S: Type,
            E: Expr,
            T: Type,
            EProof: ExprHasType<Cons<(X, S), G>, E, T>,
        {
        }

        pub struct GApp1<Proof1, Proof2, G, E1, E2, T2> {
            _t: PhantomData<(Proof1, Proof2, G, E1, E2, T2)>,
        }

        impl<Proof1, Proof2, G, E1, E2, T2> ExprHasType<G, Apply<E1, E2>, Unknown>
            for GApp1<Proof1, Proof2, G, E1, E2, T2>
        where
            G: TypeContext,
            E1: Expr,
            E2: Expr,
            T2: Type,
            Proof1: ExprHasType<G, E1, Unknown>,
            Proof2: ExprHasType<G, E2, T2>,
        {
        }

        pub struct GApp2<ProofE1, ProofE2, ProofT, G, E1, T, TT, E2, T2> {
            _t: PhantomData<(ProofE1, ProofE2, ProofT, G, E1, T, TT, E2, T2)>,
        }

        impl<ProofE1, ProofE2, ProofT, G, E1, T, TT, E2, T2> ExprHasType<G, Apply<E1, E2>, TT>
            for GApp2<ProofE1, ProofE2, ProofT, G, E1, T, TT, E2, T2>
        where
            G: TypeContext,
            E1: Expr,
            T: Type,
            TT: Type,
            E2: Expr,
            T2: Type,
            ProofE1: ExprHasType<G, E1, Fun<T, TT>>,
            ProofE2: ExprHasType<G, E2, T2>,
            ProofT: TypeConsistent<T2, T>,
        {
        }

        pub fn check_type<Proof, G: TypeContext, E: Expr, T: Type>()
        where
            Proof: ExprHasType<G, E, T>,
        {
        }

        mod tests {
            use std::marker::PhantomData;

            use crate::lambda_calculus::{
                gradual_types::{
                    standard_lib::{BoolType, NatType, True},
                    syntax::{
                        Apply, ConstBox, Constant, Expr, Fun, Lambda, Type, Unknown, VarBox,
                        Variable,
                    },
                    type_consistency::{CRefl, CUnL, CUnR, TypeConsistent},
                },
                type_set::{Cons, Empty, InHead, InTail},
            };

            use super::{
                check_type, ConstHasType, ExprHasType, GApp2, GConst, GLam, GVar, TypeContext,
                VarHasType,
            };

            struct Succ;
            impl Constant for Succ {}

            struct VarX;
            impl Variable for VarX {}

            type Proof = GApp2<
                GLam<
                    GApp2<
                        GConst<
                            InHead<(Succ, Fun<NatType, NatType>), Cons<(True, BoolType), Empty>>,
                            Cons<(Succ, Fun<NatType, NatType>), Cons<(True, BoolType), Empty>>,
                            Cons<(VarX, Unknown), Empty>,
                            Succ,
                            Fun<NatType, NatType>,
                        >,
                        GVar<
                            InHead<(VarX, Unknown), Empty>,
                            Cons<(VarX, Unknown), Empty>,
                            VarX,
                            Unknown,
                        >,
                        CUnL<NatType>,
                        Cons<(VarX, Unknown), Empty>,
                        ConstBox<Succ>,
                        NatType,
                        NatType,
                        VarBox<VarX>,
                        Unknown,
                    >,
                    Empty,
                    VarX,
                    Unknown,
                    Apply<ConstBox<Succ>, VarBox<VarX>>,
                    NatType,
                >,
                GConst<
                    InTail<
                        InHead<(True, BoolType), Empty>,
                        (True, BoolType),
                        (Succ, Fun<NatType, NatType>),
                        Cons<(True, BoolType), Empty>,
                    >,
                    Cons<(Succ, Fun<NatType, NatType>), Cons<(True, BoolType), Empty>>,
                    Empty,
                    True,
                    BoolType,
                >,
                CUnR<BoolType>,
                Empty,
                Lambda<VarBox<VarX>, Unknown, Apply<ConstBox<Succ>, VarBox<VarX>>>,
                Unknown,
                NatType,
                ConstBox<True>,
                BoolType,
            >;

            fn add_one_to_true() {
                check_type::<
                    Proof,
                    Empty,
                    Apply<
                        Lambda<VarBox<VarX>, Unknown, Apply<ConstBox<Succ>, VarBox<VarX>>>,
                        ConstBox<True>,
                    >,
                    NatType,
                >()
            }
        }
    }
}

mod type_set {
    use std::{fmt::Debug, marker::PhantomData};

    use seal::SetSeal;

    mod seal {
        use super::{Cons, Empty};

        pub trait SetSeal {}
        impl SetSeal for Empty {}
        impl<Hd, Tl> SetSeal for Cons<Hd, Tl> {}
    }

    pub trait HasName {
        fn name() -> String;
    }

    pub trait ToVec {
        fn to_vec() -> Vec<String>;
    }

    pub struct Empty;

    impl ToVec for Empty {
        fn to_vec() -> Vec<String> {
            vec![]
        }
    }

    pub struct Cons<Hd, Tl> {
        _t: PhantomData<(Hd, Tl)>,
    }

    pub trait Set: SetSeal {
        type Insert<E>: Set;
    }

    impl Set for Empty {
        type Insert<E> = Cons<E, Self>;
    }

    impl<Hd, Tl> Set for Cons<Hd, Tl>
    where
        Tl: Set,
    {
        type Insert<E> = Cons<E, Self>;
    }

    impl<Hd, Tl> ToVec for Cons<Hd, Tl>
    where
        Hd: HasName,
        Tl: ToVec,
    {
        fn to_vec() -> Vec<String> {
            let mut v = vec![Hd::name()];
            v.extend(Tl::to_vec());
            v
        }
    }

    // Base trait to check for containment
    pub trait Contains<S, E>
    where
        S: Set,
    {
    }

    pub struct InHead<E, Tl> {
        _t: PhantomData<(E, Tl)>,
    }

    impl<E, Tl> Contains<Cons<E, Tl>, E> for InHead<E, Tl> where Tl: Set {}

    pub struct InTail<Proof, Target, Hd, Tl> {
        _t: PhantomData<(Target, Hd, Tl, Proof)>,
    }

    impl<Target, Hd, Tl, Proof> Contains<Cons<Hd, Tl>, Target> for InTail<Proof, Target, Hd, Tl>
    where
        Tl: Set,
        Proof: Contains<Tl, Target>,
    {
    }

    pub fn check_contains<S: Set, E, Proof>()
    where
        Proof: Contains<S, E>,
    {
    }

    mod test {
        use super::{check_contains, Cons, Empty, InHead, InTail, Set};

        #[test]
        fn f() {
            check_contains::<Cons<i32, Empty>, i32, InHead<_, _>>();
            check_contains::<
                <<Empty as Set>::Insert<u32> as Set>::Insert<i32>,
                u32,
                InTail<InHead<_, _>, _, _, _>,
            >();
        }
    }
}