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.

▲ zevets 2 days ago | parent | next [-]

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 | parent | next [-]

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 \| parent [-]
		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 | parent | prev [-]

> 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 | parent | next [-]

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.

▲

steveklabnik 2 days ago | parent | prev [-]

Those are the unstable attributes that your sibling is talking about.

▲

1718627440 2 days ago | parent [-]

Yeah of course I can put what I want in my toy compiler. My statement was about standard C. I think that's what Contracts really are and hope this will be included in C.

	▲	steveklabnik 2 days ago \| parent [-]
		Oh sure, I wouldn’t call rustc a “toy compiler” but yeah, they’d be cool in C as well.

▲ Yoric 2 days ago | parent | prev [-]

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.