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

21–30 of 35 posts

Re: Can Types Replace Validation?

#21

Post by im3w1l »

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.

Re: Can Types Replace Validation?

#22

Post by atwood22 »

thinkingkong wrote: post #20

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

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!

Re: Can Types Replace Validation?

#23

Post by eyelidlessness »

webstrand wrote: post #14
eyelidlessness wrote: post #12

Earlier quoted context omitted.

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

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.

Re: Can Types Replace Validation?

#24

Post by pdhborges »

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.

Re: Can Types Replace Validation?

#25

Post by fulafel »

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)

Re: Can Types Replace Validation?

#26

Post by cakoose »

nighthawk454 wrote: post #18
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.)

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.

Re: Can Types Replace Validation?

#27

Post by tobbebex »

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.

Re: Can Types Replace Validation?

#28

Post by Sakos »

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

Re: Can Types Replace Validation?

#29

Post by thinkingkong »

atwood22 wrote: post #22
thinkingkong wrote: post #20

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

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

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(5)` so... other than initializing by hand with all positional arguments you aren't getting any safety.

Re: Can Types Replace Validation?

#30

Post by atwood22 »

thinkingkong wrote: post #29
atwood22 wrote: post #22

Earlier quoted context omitted.

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

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 (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.
Post reply on HN