Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Can Types Replace Validation?

blog.ploeh.dk

Post reply on HN
Print view View original

31–35 of 35 posts

Re: Can Types Replace Validation?

#31

Post by cakoose »

im3w1l wrote: post #21
cakoose wrote: post #16

> 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.)

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.)

Re: Can Types Replace Validation?

#32

Post by bvoq »

323 wrote: post #3

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.

To add to this, you cannot have dependent proofs 'easily' in Haskell, but you can use LiquidHaskell for proofs!

Re: Can Types Replace Validation?

#33

Post by pdimitar »

fulafel wrote: post #25

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 representa…

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.

Re: Can Types Replace Validation?

#34

Post by pdimitar »

pdhborges wrote: post #24
BiteCode_dev wrote: post #7

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 pr…

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.

Re: Can Types Replace Validation?

#35

Post by pdhborges »

pdimitar wrote: post #34
pdhborges wrote: post #24

Earlier quoted context omitted.

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 goodi…

> 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/

Post reply on HN