Reigning in large where clauses

[TheNeikos]

I'm currently experimenting with using typenum to statically calculate memory sizes of buffers. The problem is that my calculation roughly equates to:

type TotalLen<L> = op!(((((min(L, U20) * U8) + U24) * U3) - U320) / U16 + U16)

And this requires from L 2 where-clause lines per operation, as each subsequent operation result cannot be proven to be 'available' for the next one on its own.

So with L: Unsigned Sum<L, U2>::Output is not constrained in any way as far as I can tell, so the compiler wants me to prove it all.

The question for me now is, am I missing something that would allow to simplify the where clause so that I only have to require that L: Unsigned?

For example, could I create a special trait that is only implemented for UInt/UTerm (L can be ~ 0) that is only true if the above calculation is 'allowed'?

All uses I see of typenum are one or two operations at most, so their clauses are fairly simple. So I am wondering if this is just asking too much with current Rust and I should move to nightly with const. (Which I'd rather not do)

[kgullion]

type TotalLen<L> = op!(((((min(L, U20) * U8) + U24) * U3) - U320) / U16 + U16)
should get by with
where L: Min<U20, Output: Mul<U8, Output: Add<U24, Output: Mul<U3, Output: Sub<U320, Output: Shr<4, Output: Add<U16>>>>>>>
it gets hairy when the operations aren't "pipelined" like this.

I find it useful to think about this stuff in the same way as the Elixir pipe operator where instead of L |> min(20) |> mul(8) |> add(24) |> mul(3) |> sub(320) |> div(16) |> add(16) it's <<<<<<<<L as Min<U20>>::Output as Mul<U8>>::Output as Add<U24>>::Output as Mul<U3>>::Output as Sub<U320>>::Output as <Div<U16>>::Output as Add<U16>>::Output (which is equivalent to your op! expression). Thinking about it this way makes it a bit easier to see where the where clause is coming from.

[TheNeikos]

Huh, I didn’t think of stacking them like that. That’s nice!

thank you

[paholg]

That's pretty neat, @kgullion!

I wonder how feasable a proc macro would be that creates these where clauses for you based on use of e.g. the op! macro.

[kgullion]

Haven't really used the op! macro myself tbh, only picked up Rust a couple weeks ago 😅.

But I'd guess you could probably have something like trop!(TraitFn, L, ((((min(L, U20) * U8) + U24) * U3) - U320) / U16 + U16) expand to

type TraitFn<L> = <L as TraitFnDef>::Output;
trait TraitFnDef { type Output; }
impl TraitFnDef for L
where L: Min<U20, Output: Mul<U8, Output: Add<U24, Output: Mul<U3, Output: Sub<U320, Output: Shr<4, Output: Add<U16>>>>>>>
{
    type Output = <<<<<<<<L as Min<U20>>::Output as Mul<U8>>::Output as Add<U24>>::Output as Mul<U3>>::Output as Sub<U320>>::Output;
}

Been calling those "trait functionals" in my code (no idea if that's correct). To use it, you just need where L: TraitFnDef and TraitFn<L> instead of having to list out the bounds every time.

You could also do multiple "params" if you want to get really fancy, something like:

tr_fn!(TraitFn(A, B, C, D) << op! statement >>);

would expand to

type TraitFn<A, B, C, D> = <A as TraitFnDef<B, C, D>>::Output;
trait TraitFnDef<B, C, D> { type Output; }
impl TraitFnDef<B, C, D> for A
where << macro generated trait bounds >>
{
    type Output = << macro generated output >>;
}

[Ben-PH]

I'm working on an experimental approaches to type-eval here: https://github.com/Ben-PH/type_eval

the idea is that you can encode the AST of the type-level evaluation directly into the type-system itself, rather than having to constrain implementations manually: the constraints are evaluated by the compiler itself.

as a brief illustration, these are some tests that are passing:

#[cfg(test)]
mod test {
    use crate::{Formula, U0, U1, U2, U3, U4, U5};
    use super::Add;
    const fn _eval_2<F: Formula<FOutput = U2>>() {}
    const fn _eval_3<F: Formula<FOutput = U3>>() {}
    const fn _eval_4<F: Formula<FOutput = U4>>() {}
    const fn _eval_5<F: Formula<FOutput = U5>>() {}
    const fn _eval_add<F: Formula<FOutput = Add<U1, U1>>>() {}
    #[test]
    fn compile_basic_add() {
        const _ADD: () = _eval_2::<Add<U1, U1>>();
        const _ADD_3: () = _eval_3::<Add<U2, U1>>();
        const _ADD_4: () = _eval_4::<Add<U3, U1>>();
    }
    #[test]
    fn chain_add() {
        const _ADD_2: () = _eval_2::<Add<Add<U1, U0>, U1>>();
        const _ADD_3: () = _eval_3::<Add<Add<U1, U1>, U1>>();
        const _ADD_4: () = _eval_3::<Add<Add<U1, U1>, U1>>();
    }
    #[test]
    fn uint_add_uint() {
        const _ADD_2: () = _eval_2::<Add<Add<U1, U0>, U1>>();
        const _ADD_3: () = _eval_3::<Add<Add<U1, U1>, U1>>();
        const _ADD_2_2: () = _eval_4::<Add<U2, U2>>();
        const _ADD_1_2: () = _eval_3::<Add<U1, U2>>();
        const _ADD_2_1: () = _eval_3::<Add<U2, U1>>();
        const _ADD_3_2: () = _eval_5::<Add<U3, U2>>();
        const _ADD_2_3: () = _eval_5::<Add<U2, U3>>();
    }
}

...the idea being is that instead of somthing like this:

fn foo<L>()
where
    L: Min<
        U20,
        Output: Mul<
            U8,
            Output: Add<U24, Output: Mul<U3, Output: Sub<U320, Output: Shr<4, Output: Add<U16>>>>>,
        >,
    >, 

...the system instead automagically does all those implementations, so you can do away with the where-clauses.

It's far from having even the bare features, and I'm not even sure if it's technically possible, but it's an interesting process.

...I'm also happy to take any help and collaboration.