Live data from Hacker News

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

harudagondi.space

11–20 of 89 posts

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

#11
The alternative is one type, with many functions that can operate on that type.

Like how clojure basically uses maps everywhere and the whole standard library allows you to manipulate them in various ways.

The main problem with the many type approach is several same it worse similar types, all incompatible.

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

#12

You can go even further with this in other languages, with things like dependent typing - which can assert (among other interesting properties) that, for example, something like get_elem_at_index(array, index) cannot ever have index outside the bounds of the array, but checked statically at compilation time - and this is the key, without knowing a priori what the length of array is. "In Idris, a length-indexed vector…

How does that work? If the length of the array is read from stdin for example, it would be impossible to know it at compile time. Presumably this is limited somehow?

One option is dependent pairs, where one value of the pair (in this example) would be the length of the array and the other value is a type which depends on that same value (such as Vector n T instead of List T).

Type-Driven Development with Idris[1] is a great introduction for dependently typed languages and covers methods such as these if you're interested (and Edwin Brady is a great teacher).

[1] https://www.manning.com/books/type-driven-development-with-i...

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

#13

The alternative is one type, with many functions that can operate on that type. Like how clojure basically uses maps everywhere and the whole standard library allows you to manipulate them in various ways. The main problem with the many type approach is several same it worse similar types, all incompatible.

I don't really get why this is getting flagged, I've found this to be true but more of a trade off than a pure benefit. It also is sort of besides the point: you always need to parse inputs from external, usually untrusted, sources.

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

#15

The alternative is one type, with many functions that can operate on that type. Like how clojure basically uses maps everywhere and the whole standard library allows you to manipulate them in various ways. The main problem with the many type approach is several same it worse similar types, all incompatible.

I don't really get why this is getting flagged, I've found this to be true but more of a trade off than a pure benefit. It also is sort of besides the point: you always need to parse inputs from external, usually untrusted, sources.

Agree with this. Mismatching types are generally an indicator of an underlying issue with the code, not the language itself. These are areas AI can be helpful flagging potential problems.

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

#16

The alternative is one type, with many functions that can operate on that type. Like how clojure basically uses maps everywhere and the whole standard library allows you to manipulate them in various ways. The main problem with the many type approach is several same it worse similar types, all incompatible.

Yeah, there's something of a tension between the Perlis quote "It is better to have 100 functions operate on one data structure than 10 functions on 10 data structures" and Parse, don't validate.

The way I've thought about it, though, is that it's possible to design a program well either by encoding your important invariants in your types or in your functions (especially simple functions). In dynamically typed languages like Clojure, my experience is that there's a set of design practices that have a lot of the same effects as "Parse, Don't Validate" without statically enforced types. And, ultimately, it's a question of mindset which style you prefer.

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

#17

The alternative is one type, with many functions that can operate on that type. Like how clojure basically uses maps everywhere and the whole standard library allows you to manipulate them in various ways. The main problem with the many type approach is several same it worse similar types, all incompatible.

There are more than two alternatives, since functions can operate in more than one type.

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

#18

You can go even further with this in other languages, with things like dependent typing - which can assert (among other interesting properties) that, for example, something like get_elem_at_index(array, index) cannot ever have index outside the bounds of the array, but checked statically at compilation time - and this is the key, without knowing a priori what the length of array is. "In Idris, a length-indexed vector…

How does that work? If the length of the array is read from stdin for example, it would be impossible to know it at compile time. Presumably this is limited somehow?

If you check that the value is inside the range, and execute some different code if it's not, then congratulations, you now know at compile time that the number you will read from stdin is in the right range.

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

#19

You can go even further with this in other languages, with things like dependent typing - which can assert (among other interesting properties) that, for example, something like get_elem_at_index(array, index) cannot ever have index outside the bounds of the array, but checked statically at compilation time - and this is the key, without knowing a priori what the length of array is. "In Idris, a length-indexed vector…

How does that work? If the length of the array is read from stdin for example, it would be impossible to know it at compile time. Presumably this is limited somehow?

Not sure about Idris, but in Lean `Fin n` is a struct that contains a value `i` and a proof that `i < n`. You can read in the value `n` from stdin and then you can do `if h : i < n` to have a compile-time proof `h` that you can use to construct a `Fin n` instance.

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

#20
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.

I think “has predictable outputs” is less valuable than “has expected outputs” for most workloads. Dividing by zero almost always reflects an unintended state, so proceeding with the operation means compounding the error state. (This isn’t to say it’s always wrong, but that having it be an error state by default seems very reasonable to me.)

[deleted]
Post reply on HN