Can Types Replace Validation?(blog.ploeh.dk)
blog.ploeh.dk
Can Types Replace Validation?
https://blog.ploeh.dk/2022/08/22/can-types-replace-validation/
34 comments
This is accurate, but it leaves out something worth note: types can reduce the scope of validation needed. That's still a worthwhile outcome to work towards.
Doing application programming in Python now after some years of Scala, the uncertainty when I'm looking at code is overwhelming. What type will this argument be? Any type. What fields are optional in this record? All of them. Is this variable bound here? It depends. Will this line of code be executed on a computer? Maybe, but the next line of code may be daydreamed by a taco.
There are ways to fight against this uncertainty (Pydantic, etc.) but you learn to unit test every little damn thing.
Scala will make you feel stupid sometimes because you don't understand the ideas underlying a piece of code, but a language like Python makes you discount your ability to know anything. A line of code "x = y" might be exercised by three different unit tests, but maybe they didn't follow that one code path where y is never bound. I get more paranoid about simplifying logic in Python than I ever did in Scala. Reading other people's code is like being a jaded detective in a noir film. The function parameter is named user_count, but the last time you assumed a parameter like that was a number, you took a blackjack to the back of the head and woke up wanted for murder.
This is just an observation about one narrow aspect of Python, by the way. I'm productive in Python, it's fun, and it's an amazing experience. The feeling of proximity to power with Python is unrivaled.
There are ways to fight against this uncertainty (Pydantic, etc.) but you learn to unit test every little damn thing.
Scala will make you feel stupid sometimes because you don't understand the ideas underlying a piece of code, but a language like Python makes you discount your ability to know anything. A line of code "x = y" might be exercised by three different unit tests, but maybe they didn't follow that one code path where y is never bound. I get more paranoid about simplifying logic in Python than I ever did in Scala. Reading other people's code is like being a jaded detective in a noir film. The function parameter is named user_count, but the last time you assumed a parameter like that was a number, you took a blackjack to the back of the head and woke up wanted for murder.
This is just an observation about one narrow aspect of Python, by the way. I'm productive in Python, it's fun, and it's an amazing experience. The feeling of proximity to power with Python is unrivaled.
Reminds me of the article "Parse, don't validate", which I found helpful in cleaning up my code and making it more coherent. https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...
I think there's value in making illegal states impossible to represent with the types you're using, even if you may not be able to completely replace validation. This is one of those cases where "perfect is the enemy of good".
I think there's value in making illegal states impossible to represent with the types you're using, even if you may not be able to completely replace validation. This is one of those cases where "perfect is the enemy of good".
Another interesting idea I've read, I think in a Haskell context, is proofs attached to values.
You prove that a string originating from the user was HTML escaped - by calling the HTMLEscape function which attaches the proof - and then later in the code whenever you output it in the template it won't be escaped anymore because it's proven to be escaped.
You prove that a string originating from the user was HTML escaped - by calling the HTMLEscape function which attaches the proof - and then later in the code whenever you output it in the template it won't be escaped anymore because it's proven to be escaped.
I went down this rabbit hole 2 months ago and stumbled upon the Curry-Howard correspondence [1].
I don't understand why I find this stuff fascinating.
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
I don't understand why I find this stuff fascinating.
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
TLA+ [1] and Idris come to mind.
Also Clojure Spec [2]
For the specific case you mention, "taint analysis" would be appropriate.
[1] https://softwareengineeringdaily.com/2018/11/09/tla-with-les... [2] https://www.youtube.com/watch?v=oyLBGkS5ICk Edit: links
[1] https://softwareengineeringdaily.com/2018/11/09/tla-with-les... [2] https://www.youtube.com/watch?v=oyLBGkS5ICk Edit: links
To add to this, you cannot have dependent proofs 'easily' in Haskell, but you can use LiquidHaskell for proofs!
Yes but for 99% of your needs, aren't types going to help you? Sure I can write some types that don't terminate but in practice is this really an issue?
Dependently typed languages such as Idris or Agda uses types for validation. Their type systems are also Turing complete, but you are only allowed to use total functions (that do halt) as proofs in types.
> This matters because understanding that a normal type system is not Turing-complete means that there are truths it can't express.
I thought Godel's incompleteness theorem makes this true for all systems of proofs beyond a certain complexity. Does it matter whether the type system is Turing-complete or not?
(I don't have a robust understanding of Godel's incompleteness theorem.)
I thought Godel's incompleteness theorem makes this true for all systems of proofs beyond a certain complexity. Does it matter whether the type system is Turing-complete or not?
(I don't have a robust understanding of Godel's incompleteness theorem.)
The incompleteness theorem says there are some truths that can't be proven, but it doesn't say they can't be expressed.
When you run a type checker, it's proving that a program conforms to the type, right? That's why it seems like the incompleteness theorem applies. (Though as I mentioned before, I'm playing a bit loose with the logic.)
Sure, but it is possible to be Turing-complete. There may be further things a Turing machine can never do, but we want to do at least that much. If the type system is not “fully powerful” in this way it may be lacking in some useful aspect.
Yeah, but the phrasing seems likely to mislead. It sort of implies that a Turing-complete type system can express all truths.
Types as they exist today provide shapes. But they dont provide l external limits. Every single type safe language Ive used (limited) merged together these concepts in the form of a stdlib pattern mixed with a “choose your own adventure” library or pattern. For example in typescript we use TS and lean heavily on zod. You cant avoid it. In TS especially you just have structural types so you have to filter everywhere on user defined or external data structures. Never mind setting limits on sizes, iterations, etc.
I think the primary problem is that the second we cross network or system boundaries all the guarantees go out the window. You have to be very defensive at every layer. If we’re ever able to encapsulate that in a type system that would be… impressive.
I think the primary problem is that the second we cross network or system boundaries all the guarantees go out the window. You have to be very defensive at every layer. If we’re ever able to encapsulate that in a type system that would be… impressive.
Have you seen the library runtypes for TS? It lets you specify types using a library rather than pure TS type syntax. The library code looks very similar to the normal TS type syntax, but when you use the type you get input validation for free. And of course the type TS thinks the type is matches what you’d expect based on your type definition.
Also, TS let’s you specify things like ”this type is an array of 4 numbers”. Obviously TS isn’t perfect, but it’s pretty good!
Also, TS let’s you specify things like ”this type is an array of 4 numbers”. Obviously TS isn’t perfect, but it’s pretty good!
It lets you specify the type of length of an array but it has absolutely no protection other than initialization. For example, you can _easily_ push to an `Array<number>(5)` so... other than initializing by hand with all positional arguments you aren't getting any safety.
That’s an interesting idea. You could define a custom type that has the type of [number, number] and combine it with Omit to remove methods that allow extending the array.
Types help verify you have done the necessary validation, assuming your validation library does type narrowing.
C#'s new compiler Roslyn added built in programmable linting with Roslyn Analyzers. You can run arbitrary code over the main source and raise compile time errors as desired. In theory you could implement all the desired checks in the compilation if not in the standard type system.
I think this cuts to the heart of the question about how useful static type systems are.
Other validation / schema systems are typically much more powerful and have nicer ergonomics & learning curves for expressing invariants and business rules for data.
TS approaches warp the way you represent data as objects, because the checking requirements will heavily influence the way you design the data objects and representations.
(Not to mention all the other wins non-TS methods have, like portability of the information as data to other systems and tooling, ability to transfer or load the validation data at runtime, share between programming languages, easier to support different versions of the data and the schema concurrently, etc)
Other validation / schema systems are typically much more powerful and have nicer ergonomics & learning curves for expressing invariants and business rules for data.
TS approaches warp the way you represent data as objects, because the checking requirements will heavily influence the way you design the data objects and representations.
(Not to mention all the other wins non-TS methods have, like portability of the information as data to other systems and tooling, ability to transfer or load the validation data at runtime, share between programming languages, easier to support different versions of the data and the schema concurrently, etc)
Hard disagree here, both compile-time static strong typing and runtime validation have their role and my experience has shown that combining them works best.
Knocking on static strong typing is not a productive mindset.
Knocking on static strong typing is not a productive mindset.
Incidently, there is a wave of popular python projects in dev python spheres that use types to define validation and serialization: fastapi, typer, etc.
Granted, the python typing system is very limited, and to get complete validation, you'll need more than types as python type hints can't express complex rules.
Also, as the articles mentions, the validation will occur at runtime, it can't in any way make sure the program is valid from mypy checks alone.
Still, it's really nice to define your input data types and contraints in one go.
Granted, the python typing system is very limited, and to get complete validation, you'll need more than types as python type hints can't express complex rules.
Also, as the articles mentions, the validation will occur at runtime, it can't in any way make sure the program is valid from mypy checks alone.
Still, it's really nice to define your input data types and contraints in one go.
The Python typing system is limited compared to what exactly? It already has union types, generics, bounded generics, union types, literal types and structural subtyping.
Compare it to Haskell, OCaml and Rust and it looks like a toddler tripping all over itself compared to an adult athlete running at a steady 20km/h.
There are libraries in these languages where you can get a compile error if you make a mistake in an SQL statement.
Also, Python technically has no typing system to speak of so your comment is kind of strange. Not to mention pattern matching, destructuring and other goodies that improve productivity.
There are libraries in these languages where you can get a compile error if you make a mistake in an SQL statement.
Also, Python technically has no typing system to speak of so your comment is kind of strange. Not to mention pattern matching, destructuring and other goodies that improve productivity.
> Compare it to Haskell, OCaml and Rust and it looks like a toddler tripping all over itself compared to an adult athlete running at a steady 20km/h.
Well that is a pretty tall order. Those languages probably have the most extensive type systems among the languages with significant use. But even so Python's type system has features that some of them don't have: for example Rust doesn't have structural subtyping.
> Also, Python technically has no typing system to speak of so your comment is kind of strange.
Python PEPs define the typing annotations and the typing rules for each annotation. That for me counts as a type system, despite the fact that there is not built in typechecker and you can run programs that you didn't type check.
> Not to mention pattern matching, destructuring and other goodies that improve productivity.
Python has pattern matching now: https://peps.python.org/pep-0636/
Well that is a pretty tall order. Those languages probably have the most extensive type systems among the languages with significant use. But even so Python's type system has features that some of them don't have: for example Rust doesn't have structural subtyping.
> Also, Python technically has no typing system to speak of so your comment is kind of strange.
Python PEPs define the typing annotations and the typing rules for each annotation. That for me counts as a type system, despite the fact that there is not built in typechecker and you can run programs that you didn't type check.
> Not to mention pattern matching, destructuring and other goodies that improve productivity.
Python has pattern matching now: https://peps.python.org/pep-0636/
[deleted]
> Normal type systems (like C#'s) aren't Turing-complete.
But it comes very very close: https://blog.hediet.de/post/how-to-stress-the-csharp-compile...
But it comes very very close: https://blog.hediet.de/post/how-to-stress-the-csharp-compile...
Though in most cases I reckon that enforcing constraints in the constructor is the right thing to do. It's not ideal, but it beats trying to write a constructive version of your program inside the type system.
TypeScript's type system however is Turing complete!
If I remember correctly, the original issue filed about this was more of an alert than an expression of excitement. In either case the exclamation is warranted, but it’s fascinating how since then the TS type system has grown significantly more expressive in the ways it can perform arbitrary computations. You certainly could write a compile-time JSON parser or a SQL database in TS types well before template literal types, but now you can do it with the semantics of a high level scripting language (hilariously [to me] more like a lisp than either JS or TS). Gob help us if anyone bolts arbitrary IO onto the thing to bring automatic type acquisition into the fray.
Oracle Types did just that (although it was an April Fools joke), it was quite fun to play with. https://github.com/microsoft/TypeScript/pull/43480
I genuinely love that there’s actual lisp in there. Gob help us all.
this guy is a legend to me.