8 ms·

> 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

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

Verdex 5y ago
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).]
- coldtea 5y ago
  >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.
- steveklabnik 5y ago
  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.
joe_the_user 5y ago
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.
- amelius 5y ago
  More like: type-systems are a special kind of invariant enforcers, and so they are less useful than generalized invariant enforcers.
preseinger 5y ago
Type systems are useful, but not nearly as useful as many people believe they are.
- mountainriver 5y ago
  Try working in a big system without them =P I think they are invaluable
  - amelius 5y ago
    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.
    - morelisp 5y ago
      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.)
      - deleted 5y ago
        [deleted]
    - Verdex 5y ago
      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.
halpert 5y ago
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.
- andrewjl 5y ago
  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/OwnershipManifesto.md#non-copyable-types https://github.com/apple/swift/blob/main/docs/OwnershipManif...
- dragonwriter 5y ago
  > 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.
- teakettle42 5y ago
  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.
  - halpert 5y ago
    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.
    - dllthomas 5y ago
fho 5y ago
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 http://goto.ucsd.edu:8090/index.html#?demo=Order.hs
- mratsim 5y ago
  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)
  - fho 5y ago
    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.

Verdex 5y ago

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

coldtea 5y ago
>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.
steveklabnik 5y ago
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.

joe_the_user 5y ago

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.

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

preseinger 5y ago

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

mountainriver 5y ago
Try working in a big system without them =P I think they are invaluable
- amelius 5y ago
  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.
  - morelisp 5y ago
    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.)
    - deleted 5y ago
      [deleted]
  - Verdex 5y ago
    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.

halpert 5y ago

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.

andrewjl 5y ago
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/OwnershipManifesto.md#non-copyable-types https://github.com/apple/swift/blob/main/docs/OwnershipManif...
dragonwriter 5y ago
> 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.
teakettle42 5y ago
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.
- halpert 5y ago
  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.
  - dllthomas 5y ago

fho 5y ago

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 http://goto.ucsd.edu:8090/index.html#?demo=Order.hs

mratsim 5y ago
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)
- fho 5y ago
  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.