Comment by DonaldPShimoda | Hacker News Reader

Comment by DonaldPShimoda | Hacker News Reader

Parent Full thread

> Fascination with type systems does not seem to be all that useful in practice.

> ...

> The Rust borrow checker is an invariant enforcer. [...] This is real progress in programming language design, and is Rust's main contribution.

I'm so confused by your stance here. You essentially say "type systems are not useful" and then "oh but this most recent advance in type systems — that one is useful." Do you find type systems useful or not?

There are a lot of properties we can analyze statically, and practically all of them essentially amount to extensions of type systems. Any of them increases our ability to rule out undesirable programs from every beginning execution. Some of them have unintuitive syntax, but many of them are no more syntactically burdensome than most other type systems. This is especially true if you consider how far we've come with type inference, so we no longer have to write code with the verbosity of Java just to get some meager guarantees. It's still a very active area of research, but we're clearly making progress in useful ways (which you even highlight), so I don't really know what point it is you've set out to make.

I think the key is the following:

> It explicitly does automatic global analysis

They appear to think that the borrow checker isn't achieved with type theory, but with some other technique ("global analysis").

Although, to be fair, my understanding of making a practical affine type checker is that things get kind of wonky if you do it purely logically. So practically you do some data flow analysis. Which is, I believe, what rust is doing. This also explains why MIR was such a big deal for certain issues with borrow checking. They ended up with a format that was easier to run a data flow analysis on, and that allowed the borrow checker to handle things like non-lexical lifetimes, etc.

[I've only read about such things. So I might have mis-remembered some of the details. However, this is my take on why someone might not call rust's advances purely type theoretic (even if they can be handwaved as type theory at a high level).]

>They appear to think that the borrow checker isn't achieved with type theory, but with some other technique ("global analysis").

No, I think they appear to think that the borrow checker is not about the programmer stuffing the program with type theory annotations for this purpose, but the borrow checker handles the analysis automatically across the program.

Of course it doesn't handle it perfectly, so there's some "fighting the borrow checker" and lifetime annotations sometimes needed - but it's not like designing the whole of your program based on type theory - the same way you're somewhat free from thinking about freeing memory in a gc language.

Also, the borrow checker doesn't do global analysis. Not doing so is an important design decision in Rust, and is part of the reason why we don't infer type signatures, including lifetimes generally. You want to keep things easy to compute.

That said, you're right that the current borrow checker ("non-lexial lifetimes") is built off of a control flow analysis, absolutely. But it still operates only within bodies, not globally.

I'm so confused by your stance here. You essentially say "type systems are not useful" and then "oh but this most recent advance in type systems — that one is useful." Do you find type systems useful or not?

Not the original author but it seems like they're saying that type-systems are non-specific invariant enforcers and so have costs without necessarily having benefits whereas a user-specifiable invariant enforcer is more guaranteed to have the benefits.

More like: type-systems are a special kind of invariant enforcers, and so they are less useful than generalized invariant enforcers.

It is probably pretty presumptuous to assume, but I think that a lot of programmers that have only every been exposed to C/C++/C#, Java and Python have basically no concept of what a good type system can do for them.

Two examples from the top of my head:

1. Encoding matrix sizes into the data- and function-types, so that you can safely have a function `mat[c,b] mat_mult(mat[a,b] a, mat[c,d] b)` or even `mat[w-2,h-2] convolve(mat[w,h] input, mat[3,3] kernel)` and have the compiler check that you never use a matrix of the wrong size.

2. Actually checking the correctness of your implementation.

There is a very nice online demo of Liquid Haskell [1], where they defined the properties of ordered lists (each element has to be smaller or equal to the one before, line 119). Then they define a function that takes an (unordered) list and spits out a ordered one by applying a simple quicksort.

Now, if you break the algorithm (e.g. flip the < in line 193) and run Check, the compiler will tell you that you messed up your sorting algorithm.

Pretty neat.

edit: I just realized that LiquidHaskell is almost 10 years old. Sad to see that basically nothing made it into "production".

[1] http://goto.ucsd.edu:8090/index.html#?demo=Order.hs

For example one, it works for signal processing or graphics but compile-time dimensions are unusable in Machine Learning or Numerical Computing because it's too much friction on serialization/deserialization and some operations that reduce dimension or rank are based on runtime data (for example some dimensions are 1)

Sure, but this approach generalizes quite well. Especially in ML you have have a lot of matrices, many of them of known size (e.g. convolution kernels).

Also, while it looks like the matrix sizes have to be known at compile time, this is not the case. You are still free to use the same matrix types with dynamic sizes (or even mix them, useful for said convolutions).

In Haskell there that is achieved by using a "KnownNat", basically you elevate an integer from the value into the type level during run-time.

Type systems are useful, but not nearly as useful as many people believe they are.

Try working in a big system without them =P I think they are invaluable

They are especially useful when refactoring, or as a documentation tool.

However, without a type checker, choosing your names wisely will get you a long way.

I think anyone advocating type systems should spend a year working in a dynamic language, to get out of their echo chamber and form a more objective opinion.

The average user of Haskell, Rust, or ML today has certainly spent sufficient time in the Python/JS/Tcl/what have you mines.

The opposite is much less likely to be true; at best they may have done a project or two in Java or started migrating to TypeScript.

(Please also keep in mind: The average ML user probably reads, or intentionally avoids, HN. The average JS user doesn’t know it exists.)

What you appear to be saying is that people who like type systems must be ignorant because with experience you suspect they would think differently.

This seems to me to be extremely uncharitable point of view.

But let's roll with it.

I advocate type systems.

I've also worked in several non-trivial projects in lua. Several non-trivial projects in python. Several trivial projects in common lisp. Several trivial projects in erlang.

Additional I've worked in a non trivial project in ruby for several months. And one non trivial project in node for a year. Both of these in a professional 8 hours a day capacity.

I still advocate type systems. More so after working in dynamic languages.

Common Lisp has a type system, if I understood your meaning right.

Common Lisp also has a system for OO coding but Common Lisp is not an OO Language.

"Type system" is being used here to mean "static type checking" while CLisp has some facilities for this they are implementation-specified and not commonly used. (Even its dynamic typing checking is not commonly used.)

Common lisp is dynamically typed.

There are type hints that you can give the compiler, but I believe that's only useful for generating faster assembly. Also you can get compile time warnings from macros, but that's much closer in nature to getting a parse error (something pretty much every language does that I'm aware of static or dynamically typed).

I wouldn't be surprised to learn that there exists a common lisp typing extension that someone made with macros (after all racket has something like that iirc), however if it exists I didn't use it regardless.

see here: http://sbcl.org/manual/index.html#Handling-of-Types

I advocate for type systems specifically because of how much I've worked with dynamic languages in big corps.

That's exactly what I did, because I felt that I was just too sure that typed language were just superior to non typed languages without actually having proper experience.

I learnt Clojure, to the point that it's now my favourite language and the one I use for many things. Nevertheless, I still think that typed languages have two advantages that make them a more practical option for most situations:

- It's easier to evolve your code. This includes refactor but also normal program evolution through aggregation.

- It allows to express abstractions in pure code, rather than in documents or comments.

The first advantage requires little explanation. The second I think is more difficult to appreciate without enough experience with typed systems and an interface oriented programming style.

How these two things are important for a given person is difficult to say. I have come to the conclusion that it relates a lot to how your brain works. Unfortunately, mine can only track 3 or 4 things at the same time, so I need to abstract away anything else than the little piece of code I'm working on and get the compiler to worry about how things glue together.

I need the comfort of getting the compiler to help me change my hats and be able not to think about anything else that the concrete piece of code I'm working on and the interfaces of the other parts it uses. When I don't have this possibility, I miss it even more than the comfort of programming using inmutable data structures that Clojure spoilt me with. I think need to seriously try Scala 3 at some point, since it seems to combine inmutable data structures by default with an advance type system (although the lenses libraries I've seen look like an abomination in comparison with Clojure's update-in and company, not to mention the absolute elegance and triviality of the implementation of the latter: https://github.com/clojure/clojure/blob/clojure-1.10.1/src/c...).

So I would second your recommendation and encourage people trapped in dynamic language echo chambers to try for a year something like Typescript or Kotlin to appreciate other ways of doing things in languages with practical type systems. Perhaps some of them will discover that it suits them better or help them better understand why they prefer the dynamic style.

I was a mild advocate of static type systems. Then I spent about two years working on dynamic languages, mostly Python, on two jobs with otherwise very different code bases. I am now fully converted: after that experience, I strongly, strongly, strongly advocate static typing, so much that I will leave any job that requires me to use languages that lack them. I don't know if I was just unlucky, but I found that experience to be dreadful. Aside from the million small friction points, I remember things like needing to allocate a full week for a refactor that would have taken less than one hour (and that's a pessimistic estimate) with the standard tools of a static language's IDE.

I really don't see the advantages of dynamic languages. Supposedly you develop faster, but in my experience that's absolutely not true.

For me it all depends on the size of the project. For personal projects below a certain size dynamic typing is 50x faster than static. But that benefit drops off sharply once the project gets over a certain size or once there are more than a couple of people involved.

That's why I liked JavaScript -> TypeScript. I can bang out a prototype of some small piece in JavaScript and then add the types once I'm sure it worked. I save tons of time getting to MVP / proof of concept first and then filling in the constraints later.

I find usually that happens after a couple thousand of lines, so beyond one off scripts the advantage isn't there much.

And some of it is just bad language syntax or culture making it obtuse, not the staticness of the language. It also has an increased learning curve.

Yeah, you have to work so hard to write maintainable code in "dynamic" languages. It's also super hard to debug them. It's easier to write the first thing that runs, but that's not enough.

I'm working in Python. I agree with you. Refactoring is much harder, especially with large code bases

I’m not sure this is true. John Brant and Don Roberts did the some of the original refactoring work in Smalltalk under Ralph Johnson at UUIC.

I remember sitting with them at OOPSLA and discussing just this at length. Java was in full momentum ascendancy. Eclipse was the new will-solve-everyones-problems IDE. There was a LOT of interest in doing for typed Java in Eclipse what John and Don had both done in Smalltalk during their advanced degrees. They too thought typing would make it easier.

And what they shared with me is that it actually made it harder. Type systems are complicated to model. It gets combinatorial complex to model transformations across all the edge cases.

It may be argued that this was/is more a statement about the Java type system in particular, which is not generally extolled anyway.

But the basic take away was that refactoring becomes easier and easier as the language syntax and model gets simpler. A more complicated language like Ruby, without types, was also harder.

Or put another way… refactoring engines work with AST models. The more complicated your AST, the harder refactoring gets. I think type systems generally add, rather than remove, complexity from language models.

But perhaps there is a way to make it so. Just sharing some thoughts of yore from some guys that spent a lot of time studying refactoring.

I spent about a decade pretty much solely in dynamic languages (ruby and javascript mostly) before switching to pretty much entirely working in a fairly lame statically typed language (java). Languages with static type systems are enormously, glaringly, better. Really where the benefit comes from is static analysis; it's just that languages with static type systems have better static analysis capabilities. This may not strictly be the case in theory but it definitely is in practice.

Oh, I'll never program in a dynamically typed language again. I'm sold on that. What I'm speaking to is the notion that types are the best model for solving most/all problems in software engineering.

Do people commonly think types are a solution to most or all problems? Other than correctness I am not sure what software engineering problems a type system actually solves, and the rest of the debate is about the expressiveness of the type system (or lack thereof, which forces suboptimal engineering practices in some languages).

Static typing is just another form of static analysis. However, it's static analysis enforced by the language rather than a third party tool. That allows me to be confident in my dependencies too if I see them putting the type system to work.

Protobuf is moving us that way with microservices too. Since they're a strongly typed message format, it's harder to make mistakes in the interface between two services.

I also like that languages can have complete local static analysis. Sure, the business requirements might be large and spread across many areas, but I will break them down into smaller chunks and encode invariants into the type system so that if the small chunk compiles, I am confident it does exactly what I expect, and I don't need to remember exactly where it fits in the larger picture

> Do people commonly think types are a solution to most or all problems?

There's certainly a subclass of programmers who believe this, yes.

I can see this kinda. It would be interesting to experiment with how black and white this is.

Historically, most cases have been either compile time (static) or run time (dynamic) type checking. And left between one or the other, and experiences like the above, people make their binary choice.

More and more in my Python code, I do some type annotations I can. My feeling is that the annotation coverage ROI is non linear. I get a lot of mileage out of the types I can add easily. When it gets complicated (interesting unions or deep containment) it gets harder and harder. Enough so that sometimes it influences my design decisions just to make the typing job easier.

I’m left to wonder how this scales as the code base/team size scales. If the pain of 0 types is 100 in a large project, and 100% types cuts it to 10, what happens if we all do the easier 80% annotations. Is the pain 80% less too? Or is my personal experience mirrored and it actually is quite a bit better than just 80% reduction?

> either compile time (static) or run time (dynamic) type checking

But it is not that black and white, is it? Python is actually somewhat static in that it checks (some) types during runtime. Other dynamically typed languages live completely by the "when it quacks like a duck" playbook.

On the other hand, Haskell is completely statically typed. Still you can write many programs without annotating any types at all, as the compiler is pretty good at inferring types from their context.

> Enough so that sometimes it influences my design decisions just to make the typing job easier.

This is a very good thing. You definitely want the type system (and tests!) to guide your system design.

Rust's borrow checker isn't a type system. It's a static analyzer that tries to determine if it can figure out when to free your allocation.

I'm not deeply familiar with Rust borrow checker, but my understanding is that Swift will in the near-future support move only types. Are those not somewhat similar to what Rust has?

See here for more re Swift: https://github.com/apple/swift/blob/main/docs/OwnershipManif...

Why do you think that’s not a type system?

Literally all type systems could be described as “a static analyzer” that tries to assign and validate properties over the code it’s analyzing.

All compilers also rely on the results of that static analysis to direct codegen.

Rust’s type system implements substructural typing, and the borrow checker is an integral element of that type system.

Based on your definition, then any static analyzer is a type system, because type information and the usage of those types is basically all that’s available for static analysis.

Types define what operations can be performed. The borrow checker looks at allocations and determines when they can be freed. It really has nothing to do with types. An ideal implementation of the borrow checker could be totally type unaware and work with dynamically typed languages.

> It really has nothing to do with types.

I was under the impression that it's substantially an implementation of an affine type system (https://en.m.wikipedia.org/wiki/Substructural_type_system).

Probably you could build such a thing without thinking about types per-se, but I don't think the designers of Rust did that, and I am not sure that makes it "not a type system" anyway.

> any static analyzer is a type system

"Any static analysis checking correctness is either a linter or a type checker" isn't a claim I would make, but I am not sure offhand how I would argue against it.

> Rust's borrow checker isn't a type system

No, it's the thing that enforces a type system.

The borrow/move semantics it enforces are a (part of a) type system.

Reply on news.ycombinator.com