5 ms·
It's not just about these limitations. In order to be useful, type systems need to be simple, but there's no such restrictions on rules that govern our expecta
by crabbone 4y ago
It's not just about these limitations.
In order to be useful, type systems need to be simple, but there's no such restrictions on rules that govern our expectations of data correctness.
OP is delusional if they think that their approach can be made practical. I mean, what if the expectation from the data that an value is a prime number? -- How are they going to encode this in their type systems? And this is just a trivial example.
There are plenty of useful constraints we routinely expect in message exchanges that aren't possible to implement using even very elaborate type systems. For example, if we want to ensure that all ids in XML nodes are unique. Or that the last digit of SSN is a checksum of the previous digits using some complex formula. I mean, every Web developer worth their salt knows that regular expressions are a bad idea for testing email addresses (which would be an example of parsing), and it's really preferable to validate emails by calling a number of predicates on them.
And, of course, these aren't the only examples: password validation (the annoying part that asks for capital letter, digit, special character? -- I want to see the author implement a parser to parse possible inputs to password field, while also giving helpful error messages s.a. "you forgot to use a digit"). Even though I don't doubt it's possible to do that, the resulting code would be an abomination compared to the code that does the usual stuff, i.e. just checks if a character is in a set of characters.
- flupe 4y agoBoth your examples (is my number prime, are my XML nodes unique) are easily expressed in a dependently-typed language. Dependent type checkers may be hard to implement, but the typing rules are fairly simple, and people have been using this correct by construction philosophy using dependently-typed languages for a while now. There's nothing delusional about that.
- crabbone 4y ago> dependently-typed language. Now, are there really tools to make type systems with dependent types simple to prove? In reasonable time? How about the effort developers would have to put into just trying to express such types and into verifying that such an expression is indeed accomplishing its stated goals? Just for a moment, imagine you filing a PR in a typical Web shop for the login form validation procedure, and sending a couple of screenfulls of Coq code or similar as a proof of your password validation procedure. How do you think your team will react to this? Again, I didn't say it's impossible. Quite the opposite, I said that it is possible, but will be so bad in practice that nobody will want to use it, unless they are batshit crazy.
- ollysb 4y agoYou can use opaque types to encode constraints that the type system isn't able to express. That way you can have factory functions that apply any logic that's required before allowing construction of the opaque type. Now whenever that opaque type is referred to there's a guarantee that the data it contains satisfies your desired constraint.
- crabbone 4y ago> You can use opaque types to encode constraints that the type system isn't able to express. You just admitted in this sentence that the use of opaque types achieves nothing of value. Which was my point all along: why use them if they are useless? Just to feel smart because I pulled out an academia-flavored ninety-pound dictionary word to describe it?
- chowells 4y agoOpaque types absolutely provide something of value. They're different types. You can't pass an Integer to a function that requires a PrimeNumber. It's a compile error.
- crabbone 4y agoNot in this context they don't. They are useless if you want to ensure that a given number is a prime number.
- ParetoOptimal 4y ago> Not in this context they don't. What context is it exactly where they don't matter? I can tell you in practice, in the real world, they very much do. > They are useless if you want to ensure that a given number is a prime number. It's not useless. The point is that once you have type `PrimeNumber` that can only be constructed after being validated, you then can write functions exist in a reality where only PrimeNumber exists.
- ParetoOptimal 4y ago
- ocharles 4y ago> OP is delusional if they think that their approach can be made practical. I mean, what if the expectation from the data that an value is a prime number? -- How are they going to encode this in their type systems? And this is just a trivial example. People get too caught up in thinking that the type _has_ to express intricate properties, it doesn't. How am I going to express the expectation that something is prime? With the following closed API: module Prime where data PrimeNumber parsePrime :: Int -> Maybe PrimeNumber toInt :: PrimeNumber -> Int Now the problem is that _leaving_ this API forgets information. Whether or not that is a problem is a different question, and very dependent on the context. The same applies to your comment about passwords. One can quite easily create a closed module that encapsulates a ValidPassword type that simply performs runtime character tests on a string. I want to stress that this approach is making a trade off (as I earlier mentioned about leaving the API forgetting information, forcing you to re-parse). However, this puts this design somewhere in the middle of the spectrum. At one extreme end we have primitive obsession and shotgun parsing everywhere, with this we push the parsing into a sane place and try and hold on to these parsed values as long as possible, and at the extreme end we need dependent types or sophisticated encodings where the value carries a lot more information (and here we get towards propositions as types)
- crabbone 4y agoYour type doesn't describe prime numbers. You just named it "prime number", but there's no proof or any other guarantee that it's a prime number. > People get too caught up in thinking that the type _has_ to express intricate properties Where do you get this from? Did you even read what you are replying to? I never said anything like that... What I'm saying is that the approach taken by OP is worthless when it comes to real-life uses of validation. So, continuing with your example: you will either end up doing validation instead of parsing (i.e. you will implement parsePrime validator function), or your will not actually validate that your input is a prime number... The whole point OP was trying to make is that they wanted to capture the constraints on data in a type describing those constraints, but outside of trivial examples s.a. non-empty list, that's used by OP, that leads to programs that are either impossible or are extremely complex. > One can quite easily create a closed module that encapsulates a ValidPassword And, again, that would be doing _validation_ not parsing. I'm not sure if you even understand what the conflict here is, or are you somehow agreeing with me w/o saying so?
- PartiallyTyped 4y ago> I mean, what if the expectation from the data that an value is a prime number? -- How are they going to encode this in their type systems? And this is just a trivial example. In TypeScript we can define type Prime = number function isPrime(value: number) value is Prime { // run sieve } From here, you may have e.g. function foo(value: Prime, ...) { } And it will be typed checked. function fooOrFail(v: number) { if (isPrime(v)) foo(v) else throw new TypeError() }
- teo_zero 4y agoIf foo() happily accepts a number instead of a Prime, then this is not robust enough: you can always forget the check! It's the compiler that should warn you about a wrong type.
- PartiallyTyped 4y agoAh, you are right, i was under the impression that the compiler made it more specific. My bad.
- crabbone 4y agoYou are doing validation! Your type has no properties of a type of prime numbers. You either didn't read the article in OP, or didn't understand what OP was arguing for. Yes, it's fine, if you want to validate your input in this way -- I have no problems with it. It's just that you are doing validation, not parsing, at least not in the terms OP used them.
- PartiallyTyped 4y agoThe argument of OP is that you should first construct your input such that it adheres to a very specific type that contains all the information that you require, e.g. nonEmpty, and then allow that to go through the rest of your code. Am I mistaken? My mistake in the above snippets is precisely that TypeScript can not make the type more specific, i.e. Number to Prime, because `type Prime=number` is only creating an alias. I am not creating a type that is a more specific version of number but an alias. Had I actually created a proper type, the parsing would have been correct. The parsing component is happening in the outer function because at some point I need to make the generic input more specific, and then allow it to flow through the rest of the program. Am I mistaken?
- thanatropism 4y agoThe spirit of "parse, don't validate" is -- do all those things (SSN checksums, whatever) at the point where data enters the system, not at the point where it's used.
- crabbone 4y agoThat's not how OP used it. OP wants to express constraints on data through ML-style type system. They didn't even consider obvious competition s.a. systems like SQL constraints or XSL. I have no problems with the way you want to interpret this claim. But, really, I'm responding to the article linked to this thread, which isn't about at which point in application to perform the said validation or parsing.
- lexi-lambda 4y agoThere is a fairly obvious difference between a dynamic enforcement mechanism like contracts or SQL constraints. Though I think it is a bit silly to suggest that I have “never even considered” such things given the blog post itself is rendered using Racket, a dynamically-typed language with a fairly sophisticated higher-order contract system. SQL constraints are certainly useful. But they don’t really solve the same problem. SQL constraints ensure integrity of your data store, which is swell, but they don’t provide the same guarantees about your program that static types do, nor do they say much at all about how to structure your code that interacts with the database. I also think it is sort of laughable to claim that XSL is a good tool for solving just about any data processing problem in 2023, but even if you disagree, the same points apply. Obviously, constructive data modeling is hardly a panacea. There are lots of problems it does not solve or that are more usefully solved in other ways. But I really have applied it to very good effect on many, many real engineering problems, not just toys, and I think the technique provides a nice framework for reasoning about data modeling in many scenarios. Your comments here seem almost bafflingly uncharitable given the article in question doesn’t make any absolutist claims and in fact discusses at some length that the technique isn’t always applicable. See also: my other comment about using encapsulation instead of constructive modeling (https://news.ycombinator.com/item?id=35059113 https://news.ycombinator.com/item?id=35059113) and my followup blog post about how more things can be encoded using constructive data modeling than perhaps you think (https://lexi-lambda.github.io/blog/2020/08/13/types-as-axioms-or-playing-god-with-static-types/ https://lexi-lambda.github.io/blog/2020/08/13/types-as-axiom...).
- cjfd 4y agoclass Prime { public: Prime(int p): p(p) { if (!is_prime(p)) throw std::runtime_error("Number was not a prime!"); } int get_value() const { return p; } private: int p; }
- asimpletune 4y agoJust wanted to add that in some languages you could have a makePrime function that takes an int and returns a maybe[Prime]. If you don't make the constructor public this works perfect, as there is essentially no way to get a Prime without going through the pathways that library author relies upon. This is a pattern that's used in Scala a lot anyways.
- crabbone 4y agoThat's validation, my man. Which was the whole point of this.
- cjfd 4y agoIt is not validation if you do it at parse time. Then you can pass a Prime around the whole time and never do the is_prime check again.
- crabbone 4y ago> It is not validation if you do it at parse time Who told you so? Definitely not OP. OP doesn't believe what you just wrote.
- rovolo 4y agoFrom the OP: > Still, perhaps you are skeptical of parseNonEmpty’s name. Is it really parsing anything, or is it merely validating its input and returning a result? While the precise definition of what it means to parse or validate something is debatable, I believe parseNonEmpty is a bona-fide parser (albeit a particularly simple one). > Consider: what is a parser? Really, a parser is just a function that consumes less-structured input and produces more-structured output. The OP is saying that a validator is a function which doesn't return anything, whereas parsing is a function which returns data. (Or in other words, validation is when you keep passing around the data in the old type, and parsing is when you pass around a new type). It is true that there is code inside the parser which you can call "validation", but the OP is labeling the function based on its signature. This is made more obvious towards the end of the article: > Use abstract datatypes to make validators "look like" parsers. Sometimes, making an illegal state truly unrepresentable is just plain impractical given the tools Haskell provides, such as ensuring an integer is in a particular range. In that case, use an abstract newtype with a smart constructor to "fake" a parser from a validator. They are talking about the interface, not the implementation. They are saying that you should pass around a parsed type, even if it's only wrapping a raw value, because it carries proof that this data has been validated. They are saying that you shouldn't be validating this data in lots of different places. > It may not be immediately apparent what shotgun parsing has to do with validation—after all, if you do all your validation up front, you mitigate the risk of shotgun parsing. The problem is that validation-based approaches make it extremely difficult or impossible to determine if everything was actually validated up front or if some of those so-called “impossible” cases might actually happen. The entire program must assume that raising an exception anywhere is not only possible, it’s regularly necessary.
- piaste 4y agoPassword validation is a degenerate case of parsing, where your parsed type does not contain any more information than your unparsed type - both are just opaque strings. (In fact you could use an invalid password just fine: unless you're doing something really weird, your code would not misbehave because it's too short or missing digits and symbols. It's only due to security reasons that you choose to reject that string.) But that doesn't mean that `string -> Password` isn't parsing! As long as you're outputting distinct types for ValidPassword and InvalidPassword, you are still following the advice of this article, because you can make all your internal code use ValidPassword as a type and you will not need to ever check for password validity again.* Compare that to e.g. adding a { IsValid = true } field to the object, which would require you to defensively sprinkle `if (user.Password.IsValid)` every time you try to actually use the password field. * One weakness arising from the fact that this is degenerate parsing, i.e. ValidPassword is just a string, is that a very stubborn fool could build a ValidPassword from any arbitrary string instead of using the proper parse function. Depending on your language, this can be prevented by e.g. hiding the constructor so that only parsePassword has access to it.
- crabbone 4y ago> Password validation is a degenerate case of parsing Really? How is that degenerate? Compared to what? My guess is that you just decided to use a dictionary word you don't fully understand. > In fact you could use an invalid password Where does this nonsense come from? No. I cannot use invalid password. That's the whole point of validation: making sure it doesn't happen. What kind of bs is this? > But that doesn't mean that `string -> Password` isn't parsing! It's doing nothing useful, and that's the whole point. You just patted yourself on the head in front of the mirror for using some programming technique that you believe makes you special, but accomplished nothing of value. That was the original point: if you want results, you will end up doing validation, there's no way around it. You renaming of types is only interesting to you and a group of people who are interested in types, but doesn't advance the cause of someone who wants their password validated.
- PhilipRoman 4y agoI think your comment was unfairly downvoted without objective reasons. This is a real issue with advanced type systems and the current solutions are not very good (although they can be practical in some cases) - you can either automatically decorate constructors with assertion code (slow) or trust external input (unsafe, something like __builtin_unreachable in C). And after you're done with that, good luck getting a deterministic and fast type checker which can verify proofs (which you have to write yourself) about arbitrary theorems in your program. Yes, I'm aware there exist languages that can do this to a degree but there is a good reason why they aren't used in mainstream software. I genuinely wonder how one would write a proof in something like Agda, that parseJson("{foo:"+encodeJson(someObject)+"}") always succeeds
- crabbone 4y agoI wish this was the first such case. But, what I see happen way too often is this: Some dude comes up with another data definition language (DDL) that uses ML-style types. Everyone jumps from their seats in standing ovation. And in the end we get another useless configuration language that cannot come anywhere close to the needs of application developers, and so they pedal away on their squared-wheel bicycles of hand-rolled very custom data validation procedures. This is even more disheartening because we already have created tools that made some very good progress into systematic input validation. And they were with us since the down of programming (well, almost, we had SQL since early 70's, then we also had Prolog, then we had various XML schema languages, and finally TLA+). It's amazing how people keep ignoring solutions that achieved so much compared to ensuring that a list isn't empty... and yet present it as the way forward...
- mrkeen 4y ago> password validation (the annoying part that asks for capital letter, digit, special character? -- I want to see the author implement a parser to parse possible inputs to password field, while also giving helpful error messages s.a. "you forgot to use a digit"). This is what Applicative Functors were born to do. Here's a good article on it: https://www.baeldung.com/vavr-validation-api https://www.baeldung.com/vavr-validation-api Check the types: public Validation<Seq<String>, User> validateUser(...) Even though it's called "validation", it's still the approach the OP recommends. It reads as "If you have a Seq of Strings, you might be able to construct a User, or get back validation errors instead". Contrast this with the wrong way of doing things: User user = new User(seqOfStrings); user.validate();
- crabbone 4y agoNo. it's not the approach OP recommends. And that's why it's called validation. I have no idea why would you question that. OP wants to capture constraints on data as ML-style types. But, ML-style types have very limited expressive power, and, when it comes to real-life situation are practically useless outside of the most trivial cases.
- mrkeen 4y ago> No. it's not the approach OP recommends. It absolutely is. > I have no idea why would you question that. I did not question [that they were different approaches], I explained, through example and counter-example, why they were the same approach. I will try again. Alexis wrote both 'validate' and 'parse' examples in ML-style types: validateNonEmpty :: [a] -> IO () // ML-typed 'validate' parseNonEmpty :: [a] -> IO (NonEmpty a) // ML-typed 'parse' More from the article: The difference lies entirely in the return type: validateNonEmpty always returns (), the type that contains no information, but parseNonEmpty returns NonEmpty a, a refinement of the input type that preserves the knowledge gained in the type system. Both of these functions check the same thing, but parseNonEmpty gives the caller access to the information it learned, while validateNonEmpty just throws it away. I chose OO-style types for my samples, because there's a large fraction of HN users who dismiss ML-ish stuff as academic, or "practically useless outside of the most trivial cases". // OO-typed 'validate' (my straw man) class User { // returns void aka '()' aka "the type that contains no information" void validateUser() throws InvalidUserEx {...} } /* OO-typed 'parse' (as per my baeldung link) * "gives the caller access to the information it learned" * In this case it gives back MORE than just the User, * it also gives back 'why it went wrong', per your request above for password validation * (In contrast with parseNonEmpty which just throws an exception.) */ class UserValidator { Validation<Seq<String>, User> validateUser(...) {...} } > But, ML-style types have very limited expressive power Hindley-Milner types are a godddamned crown-jewel of computer science.
- andrewflnr 4y agoYour fallacy is: https://blog.jaibot.com/the-copenhagen-interpretation-of-ethics/ https://blog.jaibot.com/the-copenhagen-interpretation-of-eth... Meanwhile, people with more than one bit in their worldview RAM can fall back to validation when it's the only option that makes sense for their domain, and use parsing when it's appropriate, which is, notwithstanding your handful of frankly niche examples compared to the vast bulk of CRUD code, most of the time in practice.