| Crates.io | type_eval |
| lib.rs | type_eval |
| version | 0.0.1-alpha |
| created_at | 2024-12-30 14:30:03.135041+00 |
| updated_at | 2024-12-30 14:30:03.135041+00 |
| description | Type level evaluation and proof-carrying |
| homepage | |
| repository | https://github.com/Ben-PH/type_eval |
| max_upload_size | |
| id | 1499207 |
| size | 72,598 |
An R&D project that explores adding evaluation as a first-class-citizen to the typenum crate.
Typenum treats constant values and evaluation the way it ought to be treated:
fn foo<F: IsGreater<U8>())The shortfall of typenum, is that evaluation is not provided. The operation ((x + 4) * Y) / Z must be expressed like so:
fn thing<X, Y>()
where
X: Add<U4>,
op!(X + U4): Mul<Y>,
op!((X + U4) * Y): Div<Z>,
op!(((X + U4) * Y) / Z): Unsigned,
{
type ResHelper = op!(((X + U4) * Y) / Z);
println!("the value evaluated to {}", ResHelper::USIZE)
// Use `ResHelper` as the final type-system evaluation
}
fn main() {
thing::<X, U4>();
}
This process of saying "the type-values passed in must be able to perform this arithmetic" is now done internally through the *Expr traits (Num/Bool/Ord/other expression traits):
fn thing<E: NumExpr>() {
// TODO: extract an execution-time value from the type
println!("the value evaluated to {}", E::Ret)
}
fn main() {
// todo: actually impl the op! macro:
// do_thing::<op!(((X + 4) * Y) / Z)>();
// ...which would expand to:
do_thing::<Div<Mul<Add<X, U4>, Y>, Z>>();
}
Currently negative numbers are not yet implemented.
The strategy for implementing division requires type-resolution capabilities made available in nightly-2024-10-17. This should be improved in the near future.
The following operations are implemented: if, +, -, *, /, <<, >>, <, >, <=, >=, ==, cmp
The error output is in a messy binary form. The plan is to make this more readable.
In very approximate order of priority:
op macro (replace IF<LT<X, Y>, Add<Div<X, U2>, Y>, Z> with op!(if X < Y {(X + 2)/ Y} else {Z}))struct U238... instead of type U238 = ...usize type in declaring array lengths.match expression impl