Comment by _bxg1 | Hacker News Reader

Comment by _bxg1 | Hacker News Reader

Good points. However, I disagree with this:

> But please, stop pretending that type-level programming is a desirable thing. It's a kludge, and hopefully a temporary one. Personally, I want to write all my specifications in more-or-less the same language I use to write ordinary code. It's the tool's job to prove correctness or, if it must, tell me that it failed.

I don't see explicit type-programming as (always) a kludge; oftentimes it's the primary vocabulary for expressing certain ideas. I.e. type annotations are not (always) just typechecker-hints, but can be explicit documentation of intent.

> We need to be able to step up the strength of our specifications without switching language all the time. We need to integrate typed and untyped code

This has been a revelation during my time spent with TypeScript. The fact that I can just add a comment that disables an unhelpful type error on a given line is a game-changer. Or that I can assert to the system "no really, this value that has a union type is actually just this particular subset of that union" (cast) and retain meaningful checks after that point. Having a type system that's flexible has made it enormously more useful. It allows you to deal with those cases where what you want to do can't be type-checked, within the context of (and playing nicely with) a broader system that is type-checked.

As somebody who moved from untyped to typed (Python to Rust) I think the two biggest arguments for typed systems are:

- they encourage you to keep you code data oriented, which is usually (at least in my experience) a food thing

- certain classes of mistakes can be checked for before you even run the code itself

They also make refactoring much easier. Renaming a function or variable and having all "true" references renamed (not just things with the same name but in a different scope), for example.

Safely and automatically renaming a function, local or global variable does not require a type system (see clojure and many other dynamic languages). Only renaming an instance field on a class needs it (because then all accesses on an object must be renamed, which requires knowledge of the type of your variables).

Incidentally programming in a more functional style reduces the need for this kind of thing. it doesn't eliminate it though so it can still be a source of runtime bugs when typos creep in, that's a trade off you have to make.

Unit tests for business logic and specifications for data shape can help to catch those typos as a side effect of the other benefits they bring. However typo catching will never be as solid as in a typed language, I've decided I'm ok with that as long as I'm not programming something that could kill someonev if it crashes.

If you're writing an application that could kill someone if it crashes, you'd better not be relying on the type system to catch those crashes for you, since it will only catch the most obvious ones.

For any life-critical system you want first and foremost to have a battery of end-to-end tests that run the software on the target hardware under various operating conditions. No amount of software-only testing/formal methods will give you this part.

Then, you want to have a formal specification of your program that can be run through a model checker - this would be the industry standard, though, if you have a team of PhDs at your disposal, you could also try to go with full formal verification a la Coq.

Finally, you want unit testing, integration testing, and possibly a type system to help day-to-day development. But do note, none of these should be critical for assuring the system works as indended - if typos in your code aren't caught by your end-to-end tests, what hope is there that they will catch complex dynamic behaviors?

> If you're writing an application that could kill someone if it crashes, you'd better not be relying on the type system to catch those crashes for you, since it will only catch the most obvious ones.

Safety critical systems are quite different from the vast majority of software systems, and raising them as an example in a general programming argument isn't really fair. There already are safety critical certifications that are mandatory for many aviation and healthcare related applications. They generally utilize heavy testing, model checking, and supporting documentation. Very few commercial industries operate with this much attention to quality, basically because it's too expensive.

The GP had raised them, that's the only reason I commented about this.

You are right though, the standard for that type of software is very different from regular programming.

Still, we shouldn't forget that even the strongest typing can't substitute testing. Most likely, even if you had a formally proved system, which is already much, much more difficult than any other kind of regular software development practice, you would still want some amount of testing to go with that system before putting it in production.

Yes I agree

It doesn't require it, but by all indications it makes the tooling much easier to write when there is a type system and it's constraints reducing the surface area.

Another thing to consider is the type system of Idris where the compiler may recognise at compile time that the value can only be of a certain subset of a union and, more importantly, can use the type of a function to infer much of the correct implementation, like, all the cases that must be handled and sometimes even how to handle them.

Lots of type systems support type inference. It seemed (I could have misinterpreted) like the OP was suggesting that in a perfect world all types would be inferred. That's the idea I was disagreeing with.

Normal type inference deduces the type from the code, Idris can infer the implementation from the type if the type is specific enough. In a way, this is Church in action: the type is a theorem, and the compiler is a proof assistant that helps to automatically find a proof (a correct program having that type).

So Idris is an argument supporting your position: if it works (it is still part of a research program), the types are the primary expression, and the code is secondary.

I read the OP differently. Type-level programming (not to be confused with type-oriented programming) is using the typechecker to perform computation on types, which proves guarantees at compiler time. In this case, types are less about documentation, they are literally proofs of properties of the program by construction. In fact, type-level programming is usually unreadable[0] unless the reader has deep knowledge of the specific language implementation of type families, functional dependencies, poly-kinds, etc (whatever permits typelevel programming in that language).

I'm getting that the OP is arguing against these ad-hoc constructs (type families etc) and would much rather write these proofs in the same language as ordinary code (e.g. writing the law "List x where length(x) == 5" in the type rather than "forall a. List (S (S (S (S (S Z))))) a") which, well who can disagree?

In a sense, you and OP both agree on the same thing. Types are good. No types (or unreadable ad-hoc constructs for types) are not good.

[0]: https://aphyr.com/posts/342-typing-the-technical-interview uses type-level programming in Haskell to solve N-queens

> type annotations are not (always) just typechecker-hints, but can be explicit documentation of intent

More than this, in highly expressive type systems such as Haskell's, they can carry proofs. This can be useful for constraining the capabilities of effects (ie: we can state that a particular function has the ability to make a network request but cannot open files) as well as assisting us in writing the correct implementation by construction. As an author of a type-level library it's also highly useful for generating code from arbitrary types that is also correct by construction and deriving obvious implementations so we have to write less code.

Haskell's type system may soon be able to check for usage as well by encoding linearity into the type system. This will enable to tell the type checker that a function which has a resource must use it at least once. Without explicitly sequencing our nice, pure code the compiler can ensure that linearity is preserved. Idris 2 is experimenting with this as well. It seems like a pretty good idea.

And all of this type level stuff is so useful that we want to do more of it. Dependently typed languages remove the separation between the type language and the language of terms. This is powerful stuff.

It is sensible to include this in TypeScript, because it needs to interface with potentially large swathes of plain JavaScript, which is akin to unsafe code in Rust.

TypeString type assertions are like C++ reinterpret_cast. If you're wrong about what you think it is, that's as good as undefined behavior in C++, virtually anything can happen.

I'm only nitpicking because this is one of the things the article complains about but I think you're conflating two types of saftey. All Javascript (TypeScript included) is "safe" in the sense of C++/Rust. Using the wrong TypeScript type in TypeScript can result in programming errors but not unsafety or undefined behaviour in C++/Rust terms.

Reply on news.ycombinator.com