[HN Gopher] Can Types Replace Validation?
       ___________________________________________________________________
        
       Can Types Replace Validation?
        
       Author : todsacerdoti
       Score  : 20 points
       Date   : 2022-08-22 10:26 UTC (2 days ago)
        
 (HTM) web link (blog.ploeh.dk)
 (TXT) w3m dump (blog.ploeh.dk)
        
       | aliswe wrote:
       | this guy is a legend to me.
        
       | 323 wrote:
       | 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.
        
         | throwaway545232 wrote:
         | 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...
        
       | alphanumeric0 wrote:
       | 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?
        
       | chowells wrote:
       | 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.
        
       | BiteCode_dev wrote:
       | 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.
        
       | joshribakoff wrote:
       | Types help verify you have done the necessary validation,
       | assuming your validation library does type narrowing.
        
       | jameshart wrote:
       | > 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...
        
       ___________________________________________________________________
       (page generated 2022-08-24 23:01 UTC)