3 ms·
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 "wher
by Sharlin 8mo ago
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.
For full-on parse-don't-validate, you essentially need a dependent type system. As a more light-weight partial solution, Rust has been prototyping pattern types, which are types constrained by patterns. For instance a range-restricted integer type could be simply spelled `i8 is 0..100`, or a nonempty slice as `[T] is [_, ..]`. Such a feature would certainly make correctness-by-construction easier in many cases.
The non-empty list implemented as a (T, Vec<T>) is, btw, a nice example of the clash between practicality and theoretical purity. It can't offer you a slice (consecutive view) of its elements without storing the first element twice (which requires immutability and that T: Clone, unlike normal Vec<T>), which makes it fairly useless as a vector. It's okay if you consider it just an abstract list with a more restricted interface.
- deleted 8mo ago[deleted]
- rhdunn 8mo agoIt's also useful to wrap/tag IDs in structured types. That makes it easier to avoid errors when there are multiple type parameters such as in the Microsoft graph API.
- humkieufj 8mo ago[flagged]
- spockz 8mo agoComing from Haskell, I loved Agda 2 as a dependent type language. Is there any newer or more mainstream language that has added dependent types?
- doctor_phil 8mo agoIdris 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.
- spockz 8mo agoAh 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.
- throw_await 8mo agoTypescript has something that can be used as dependent types, but it wasn't intended as a language feature, so the Syntax is not as ergonomic as Agda: https://www.hacklewayne.com/dependent-types-in-typescript-seriously https://www.hacklewayne.com/dependent-types-in-typescript-se...
- codethief 8mo agoThat whole blog is one big and fascinating rabbit hole into type theory! Thanks for the link!
- instig007 8mo agoYou 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+
- yuppiemephisto 8mo agolean 4