Type-checker for Simply Typed Lambda Calculus

stlc.rs

use std::boxed::Box;

/// Simply typed lambda calculus is based on untyped lambda calculus, but
/// added a simple type. (Which is the function type A -> B)
#[derive(PartialEq, Eq, Debug)]
enum Type {
    /// Base type
    BuiltIn(&'static str), Var(String),
    /// Function type (Type * Type)
    Lambda(Box<Type>, Box<Type>),
}

// Some helper here
const TInt : Type = Type::BuiltIn("Int");
const TStr : Type = Type::BuiltIn("String");
fn tvar (s: &str) -> Type {
    Type::Var(s.to_owned())
}
fn tlam (arg: Type, ret: Type) -> Type {
    Type::Lambda(Box::new(arg), Box::new(ret))
}

/// (T)Expression is a collection of expressions
/// here it is prefix with a uppercase T is because we are not
/// going to write a evaluator here, so it is only dealing with
/// types.
enum TExpression {
    /// Apply(Type::Lambda, Type)
    Apply(Type, Type),
    /// Lambda(Type::Lambda)
    Lambda(Type),
}

impl TExpression {
    fn apply(t1: Type, t2: Type) -> Type {
        let (arg, ret) = match t1 {
            Type::Lambda(arg, ret) => (*arg, *ret),
            _ => panic!("Cannot apply a non-lambda")
        };

        if t2 == arg { ret } else {
            panic!("Type error, lambda argument type mismatch")
        }
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    #[test]
    fn apply_lambda() {
        assert_eq!(
            TInt,
            TExpression::apply(tlam(TStr, TInt), TStr)
        );
    }

    #[test]
    fn apply_return_lambda() {
        assert_eq!(
            tlam(TStr, TInt),
            TExpression::apply(tlam(TInt, tlam(TStr, TInt)), TInt)
        )
    }
}