Can Types Replace Validation?
blog.ploeh.dk
Can Types Replace Validation?
1–10 of 35 posts
Re: Can Types Replace Validation?
#2this guy is a legend to me.
Re: Can Types Replace Validation?
#3Another 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.
Re: Can Types Replace Validation?
#4Another 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.
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...
Re: Can Types Replace Validation?
#5Yes 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?
Re: Can Types Replace Validation?
#6This 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.
Re: Can Types Replace Validation?
#7Incidently, 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.
Re: Can Types Replace Validation?
#8Types help verify you have done the necessary validation, assuming your validation library does type narrowing.
Re: Can Types Replace Validation?
#9> 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...
Re: Can Types Replace Validation?
#10> 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...
TypeScript's type system however is Turing complete!