Hacker News Reader

Comment by im_down_w_otp | Hacker News Reader

>"The type system is for structuring how your program runs not its logical correctness."

Type-level programming can be a very powerful and useful way to coerce correctness in some scenarios, so I'm really confused by this statement.

View on HN

I think the arguments on both sides are valid.

In dynamic programming languages, I generally prefer factoring business logic outside of procedures and into lookup tables. This is sometimes called "data-driven" or "table-oriented" programming. It eliminates control flow, which makes code more maintainable and less buggy.

Using Julia's dispatch mechanism accomplishes a similar goal. Here, multiple dispatch is akin to a table lookup. It may even be faster than the explicitley data-driven approach since the lookup can be done in compile-time.

I like data driven programming too. The code can become more declarative this way and the logic more malleable.

Part of his point seems to be that you can manipulate data with code, but you can't manipulate your app's typings with code.

Expressing your business domain in types makes it more likely that a given change of requirements demands a lot of by-hand, non-abstractable changes to the code.

I'd argue on the contrary, having the business domain in the type system allows the compiler to help you ensure the changes are made correctly instead of relying purely on tests (which are still valuable, but I'll take guarantees where I can get them).

The type system also makes it easy to reduce the state space of the program. For example, if a method takes an int as a parameter you have a pretty large state space. But if it takes a strongly typed enum which can only be of 3 values, now you have restricted the surface area for which you have to test. If you exploit the type system to this effect it is very powerful.

I agree with both your points! I didn't make a value judgment, and in fact I think our comments aren't mutually exclusive, we're just describing the pros for each side of what ends up being a trade-off.

The problem I call out is less of an issue for the parts of the domain that are unlikely to change often, or that touch fewer parts of the system.

"Part of his point seems to be that you can manipulate data with code, but you can't manipulate your app's typings with code."

You can do both you know.

Yeah if you’re writing a standard library or a parser or maybe a database query optimizer, but if you aren’t writing code about code, then it’s probably not the way to go.

take a look at https://blog.moertel.com/posts/2006-10-18-a-type-based-solut... for a good counterexample

Off topic: the link in your profile seems to no longer have its intended contents

thanks, removed it!

Is it a good counterexample? It seems to have approximately the same misuse resistance as parameter binding or equivalent apis. (For example, the dom api.)

In particular, this property of the described system makes it trivial for the unknowing or uncaring to subvert it: > It provides a string-management kernel that lets you create “safe strings” by certifying a regular string as representing either text or a fragment of a known language.

From what I understood, the certification is an unchecked assertion made by the program. One of the comments gives a great example of how this will go wrong in practice. The other aspect of this that is glossed over is that many data schemas represent all these things as "text". It is again an exercise for the program to get this right at the io boundaries.

i am perhaps biased, since my day job is working on static type inference for python[0], but i genuinely do believe that encoding properties like this into the type system gives you not just an extra level of safety, but an extra level of expressiveness when modelling your data in code. it's the equivalent of having units in physics.

i agree that it's not foolproof, but it's better than treating everything as an undifferentiated string.

[0] https://github.com/google/pytype

The idea is to make security reviews easier. You can easily find all the places "safe strings" are created to see if they are doing the right parsing or sanity checks. The code that only uses the safe api needs less scrutiny, at least for the class of bugs this design is supposed to help with.

I don't know. I'm of course biased, though that bias is built on several years of dealing with increasingly critical systems and the entirely avoidable issues those systems faced due to a preponderance of foot-guns that could have been otherwise mitigated with clever use of "ahead of time" constraint checking and enforcement. Not to mention the runtime quality and localizability of your diagnostics goes up a ton too when you know ahead of time that when you see certain kinds of errors/exceptions/failures that they must have happened in certain places and/or under very narrow conditions.

It also has a very nice quality of not mucking up your runtime performance with doing all the constraint checking on-demand and in very branchy ways.

As a simple example of how useful the approach can be, here's a thing we did awhile ago for making safe abstractions to low-level hardware resources: https://blog.auxon.io/2019/10/25/type-level-registers/ .

With that approach we could build a pipeline to consume hundreds of pages of SoC datasheet, generate the appropriate type specs from the register definitions, and end up with an API to the hardware that would fail to compile if a program was written to consume the hardware interface in a way that violated the spec in the datasheet.

Reply on news.ycombinator.com