Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Parse, Don't Validate and Type-Driven Design in Rust

harudagondi.space

Post reply on HN
Print view View original

71–80 of 89 posts

Re: Parse, Don't Validate and Type-Driven Design in Rust

#71

Post by fph »

alfons_foobar wrote: post #36
MaulingMonkey wrote: post #30

Earlier quoted context omitted.

> Would have to be F32, no? Generally yes. `NonZeroU32::saturating_add(self, other: u32)` is able to return `NonZeroU32` though! ( https://doc.rust-lang.org/std/num/type.NonZeroU32.html#metho... ) > I cannot think of any way to enforce "non-zero-ness" of the result without making it return an optional Result , and at that point we are basically back to square one... `NonZeroU32::checked_add(self, other: u32)` basical…

> `NonZeroU32::saturating_add(self, other: u32)` is able to return `NonZeroU32` though! I was confused at first how that could work, but then I realized that of course, with _unsigned_ integers this works fine because you cannot add a negative number...

You'd still have to check for overflow, I imagine.

And there are other gotchas, for instance it seems natural to assume that NonZeroF32 * NonZeroF32 can return a NonZeroF32, but 1e-25 * 1e-25 = 0 because of underflow.

Re: Parse, Don't Validate and Type-Driven Design in Rust

#72

Post by satvikpendem »

hmry wrote: post #51
satvikpendem wrote: post #29

Earlier quoted context omitted.

Rust has some libraries that can do dependent typing too, based on macros. For example: https://youtube.com/watch?v=JtYyhXs4t6w Which refers to https://docs.rs/anodized/latest/anodized/

Very cool and practical, but specs aren't dependent typing. (I actually think specs are probably more useful than dependent types for most people) Dependent typing requires: - Generic types that can take runtime values as parameters, e.g. [u8; user_input] - Functions where the type of one parameter depends on the runtime value of another parameter, e.g. fn f(len: usize, data: [u8; len]) - Structs/tuples where the typ…

Sadly I'm not sure Rust will ever get those sorts of features.

Re: Parse, Don't Validate and Type-Driven Design in Rust

#73

Post by kibwen »

fspeech wrote: post #70
hutao wrote: post #23

Note that the division-by-zero example used in this article is not the best example to demonstrate "Parse, Don't Validate," because it relies on encapsulation. The principle of "Parse, Don't Validate" is best embodied by functions that transform untrusted data into some data type which is correct by construction . Alexis King, the author of the original "Parse, Don't Validate" article, also published a follow-up, "Na…

Yes division is a poor example. It's a poor separation of concerns to try to wrap at this level without usage context. To see the point try to wrap overflows on arithmetic functions.

> To see the point try to wrap overflows on arithmetic functions.

The invariant is less obvious, but you could still do this if you really wanted. The observation is that addition of two fixed-size nonnegative integers cannot overflow unless at least one is greater than half the range. So your `non_overflowing_addition` function would need take two inputs of type `NonNegativeLessThanHalfMaxValue`, where the constructor for the latter type enforces the invariant. Multiplication is similar, but with the square root of the range (and I suppose `NonNegativeLessThanSqrtMaxValue` could be a subtype of `NonNegativeLessThanHalfMaxValue` if you want to be fancy).

Re: Parse, Don't Validate and Type-Driven Design in Rust

#74

Post by hmry »

satvikpendem wrote: post #72
hmry wrote: post #51

Earlier quoted context omitted.

Very cool and practical, but specs aren't dependent typing. (I actually think specs are probably more useful than dependent types for most people) Dependent typing requires: - Generic types that can take runtime values as parameters, e.g. [u8; user_input] - Functions where the type of one parameter depends on the runtime value of another parameter, e.g. fn f(len: usize, data: [u8; len]) - Structs/tuples where the typ…

Sadly I'm not sure Rust will ever get those sorts of features.

They've gone the Haskell route of adding a billion features to a non-dependent type system instead.

Not that I blame them, nobody has figured out practical dependent typing yet. (Idris is making good progress in the field though)

Re: Parse, Don't Validate and Type-Driven Design in Rust

#75

Post by kibwen »

cmovq wrote: post #4

Dividing a float by zero is usually perfectly valid. It has predictable outputs, and for some algorithms like collision detection this property is used to remove branches.

The problem is that "division" in the context of computation refers to multiple different operations, so that we all end up talking past each other. Some people want a `division_where_zero_is_an_illegal_denominator`, some people want `division_but_return_zero_if_denominator_is_zero`, and I'm sure other people want weirder things. Honestly, I'm coming around to the idea that for any precise and reliable system, the fact that we only have a single "operator" (+ - * / etc) that we arbitrarily assign to one of the many possible operations that we want to do does more harm than good. Consider how many different ways there are just to add a number (panic on overflow, error value on overflow, saturate on overflow, wrap on overflow, return tuple with optional carry flag on overflow...).

Re: Parse, Don't Validate and Type-Driven Design in Rust

#76

Post by hutao »

kibwen wrote: post #73
fspeech wrote: post #70

Earlier quoted context omitted.

Yes division is a poor example. It's a poor separation of concerns to try to wrap at this level without usage context. To see the point try to wrap overflows on arithmetic functions.

> To see the point try to wrap overflows on arithmetic functions. The invariant is less obvious, but you could still do this if you really wanted. The observation is that addition of two fixed-size nonnegative integers cannot overflow unless at least one is greater than half the range. So your `non_overflowing_addition` function would need take two inputs of type `NonNegativeLessThanHalfMaxValue`, where the construct…

Note that addition also won't overflow if one addend is greater than half the range, but the other addend is still small enough (e.g. for the range -128 to 127, adding 65 + 12 will not overflow, even though 65 is greater than half of 127).

Your intention of having the restricted domain "NonNegativeLessThanHalfMaxValue" is probably so that both addends have the same domain. If you go down that route, perhaps you'll also want the closure property, meaning that the range should also belong to the same set. However, then you have to deal with the overflow problem all over again...

The real point is that when adding two N-bit integers, the range must be N+1 bits, because the "carry bit" is also part of the output. I think this is a scenario where "Parse, Don't Validate" can't easily help, because the validity of the addition is intrinsically a function of both inputs together.

Re: Parse, Don't Validate and Type-Driven Design in Rust

#77

Post by cadamsdotcom »

Parsing over validation, and newtypes for everything, fall over when you don’t know the full range of possibilities that can occur in the wild.

It is a handy way to prevent divide by zero as in the article, or to have fun with lambda calculus by asking the type system if 3 + 4 == 8. You can reason about the full range of inputs. Same for file format parsing - making as many failure modes as possible fail as early as possible!

But be VERY wary of using them to represent business logic or state machines that allow only the transitions you believe can exist at this point in time. You just don’t know what wild things people will want to do in business logic, and if your software can’t handle those scenarios, people will just work around it and your stuff no longer matches reality.

Re: Parse, Don't Validate and Type-Driven Design in Rust

#78

Post by spockz »

doctor_phil wrote: post #54
spockz wrote: post #53

Earlier quoted context omitted.

Coming from Haskell, I loved Agda 2 as a dependent type language. Is there any newer or more mainstream language that has added dependent types?

Idris is slightly more mainstream I would say, but not wildy so. If you like the Haskell interop then I'd recommend staying with Agda. Scala 3 is much more mainstream and has path dependent types. I've only used Scala 2, and there the boilerplate for dependent types was frustrating imo, but I've heard its better in 3.

Ah yes Idris rings a bell. I’ll try that one again.

Scala 3 indeed is more mainstream but it seems also on the way out. At least here in corporate world it is replaced by Kotlin and Java 21+ for a large part.

Re: Parse, Don't Validate and Type-Driven Design in Rust

#79

Post by instig007 »

spockz wrote: post #53
Sharlin wrote: post #32

Earlier quoted context omitted.

Even the newtype-based "parse, don't validate" is tremendously useful in practice, though. The big thing is that if you have a bare string, you don't know "where it's been". It doesn't carry with it information whether it's already been validated. Even if a newtype can't provide you full correctness by construction, it's vastly easier to be convinced of the validity of an encapsulated value compared to a naked one. F…

Coming from Haskell, I loved Agda 2 as a dependent type language. Is there any newer or more mainstream language that has added dependent types?

You can have range-constrained numeric types and collections in Haskell via Liquid Haskell, which has almost seamless integration with the compiler starting from GHC-9.12+

Re: Parse, Don't Validate and Type-Driven Design in Rust

#80

Post by instig007 »

qsera wrote: post #69
mrkeen wrote: post #65

Earlier quoted context omitted.

Was the original blog post wrong?

were you validating during parsing before?

Validating during parsing is still parsing, there's a reason why `Alternative f` exists after all: you have to choose between branches of possibilities and falsehoods. Now consider that there's another kind of validation that happens outside of program boundaries (where broader-than-needed data is being constrained in a callee rather than the calling site) that should've been expresed as `Alternative f` during parsing instead. That's the main point of the article, but you seem to only focus on the literal occurence of the word "validation" here and there.
Post reply on HN