#lambda-calculus #type #cursed

lambda-types

Puts the lambda calculus in Rust...'s type system

6 releases

0.2.1 Sep 6, 2024
0.2.0 Sep 6, 2024
0.1.3 Sep 6, 2024

#489 in Math

40 downloads per month

MIT license

180KB
256 lines

lambda-rs

"Lambda calculus? In my type system?" (It's more likely than you think.)

An implementation of the Lambda Calculus in Rust, only using ZSTs, traits, and generics.

use lambda_types::prelude::*;

type Two = call! { Successor, Successor, Zero  };
type Three = call! { Successor, Two  };
type Six = call! { Multiply, Three, Two };
type Seven = call! { Successor, Six };

static THE_MEANING_OF_LIFE: call! {
    ToNumber { Multiply, Six, Seven }
} = ConstNumber::<{b'*' as u64}>; // 42


lib.rs:

lambda-types


Implements the Lambda Calculus in Rust's type system.

There is zero runtime functionality or procedural macros in this crate - it's all done using generics, traits, and associated types.

If you want to toy around with this, check out the prelude.

If you want to write your own function types, check out the Macros.

The Y combinator is left unimplemented, as Rust evaluates types greedily, making it unusable.

Dependencies