← Back to context

Comment by quotemstr

2 days ago

I've been thinking for a while now about using dependant typing to enforce good numerics in numerics kernels. Wouldn't it be nice if we could propagate value bounds and make catastrophic cancellation a type error?

Have you worked much with SAL and MIDL from Microsoft? Using SAL (an aesthetically hideous but conceptually beautiful macro based gradual typing system for C and C++) overlay guarantees about not only reference safety but also sign comparison restriction, maximum buffer sizes, and so on.

9 comments

quotemstr

Reply
Yoric  1 day ago

Dependent types in well-behaved, well-defined snippets of C++ dedicated to numeric kernels?

While I think it's a great idea, this also sounds like it would require fairly major rewrites (and possibly specialized libraries?), which suggests that it would be hard to get much buy-in.

zevets  2 days ago

Please do this.

But first: we need to take step-zero and introduce a type "r64": a "f64" that is not nan/inf.

Rust has its uint-thats-not-zero - why not the same for floating point numbers??

  • tialaramex  2 days ago

    You can write your "r64" type today. You would need a perma-unstable compiler-only feature to give your type a huge niche where the missing bit patterns would go, but otherwise there's no problem that I can see, so if you don't care about the niche it's just another crate - there is something similar called noisy_float

    • zevets  2 days ago

      I can do it, and I do similar such things in C++ - but the biggest benefit of "safe defaults" is the standardization of such behaviors, and the resultant expectations/ecosystem.

  • 1718627440  2 days ago

    > Rust has its uint-thats-not-zero

    Why do we need to single out a specific value. It would be way better if we also could use uint-without-5-and-42. What I would wish for is type attributes that really belong to the type.

        typedef unsigned int __attribute__ ((constraint (X != 5 && X != 42))) my_type;

    • int_19h  2 days ago

      Proper union types would get you there. If you have them, then each specific integer constant is basically its own type, and e.g. uint8 is just (0|1|2|...|255). So long as your type algebra has an operator that excludes one of the variants from the union to produce a new one, it's trivial to exclude whatever, and it's still easy for the compiler to reason about such types and to provide syntactic sugar for them like 0..255 etc.