29 ms·

Borrow-checking without type-checking

91 points by jamii 5mo ago

Panzerschrek 5mo ago
In my programming language I have some sort of "borrowing" too (although it's named differently). But my language has no dynamic typing, only static typing is used and thus all checks are compile-time and have no runtime cost. Why bothering with dynamic typing and paying runtime costs for it?
- jamii 5mo ago
  > The goal is that most of your code can have the assurances of static typing, but you can still opt in to dynamically-typed glue code to handle repls, live code reloading, runtime code generation, malleable software etc.
- Pay08 5mo ago
  Dynamic typing is neat, I actually prefer it to static typing. Most people who think they have a problem with dynamic typing actually have a problem with weak typing.
  - choeger 5mo ago
    Dynamic typing is no typing. The point of types is to prove the absence of errors. Dynamic typing just has these errors well-structured and early, but they're still errors.
    - Pay08 5mo ago
      Errors that you can recover from. I simply appreciate the added flexibility. Have you ever tried making a container of arbitrary types in C++?
      - lmm 5mo ago
        If C++ was the only static type system I'd experienced, I would also think it was a bad idea. Have you ever used an ML-family language?
        Pay08 5mo ago
        Nope. Closest thing I have used was probably Haskell.
        lmm 5mo ago
        Haskell ought to be good enough. Did you struggle with making your containers there?
        Pay08 5mo ago
        Interestingly enough, I have never needed them there. Granted, I have written a few orders of magnitude less Haskell than I have C++. Still, the difference is worth interrogating (when I'm less sleep deprived).
      - SuperV1234 5mo ago
        You cannot do anything meaningful with a container of arbitrary types, it's just bad design. If you want to apply the same operation on all of them, then they share some API commonality -- therefore you can use polymorphism or type erasure. If they don't, you still need to know what types they are -- therefore you can use `std::variant`. If they really are unrelated, why are you storing them together in the same container? Even then, it's trivial in C++: `std::vector<std::any>`.
    - cardanome 5mo ago
      > The point of types is to prove the absence of errors Maybe for you. Originally static typing was to make the job of the compiler easier. Dynamic typing was seen as a feature that allows for faster prototyping. And no, dynamic typing does not mean untyped. It just means type errors are checked at runtime instead of compile time. You can have strongly typed dynamic languages. Common Lisp is a very good example. Weak typing is a design mistake. Dynamic typing has its place as it allows you to have types that are impossible to express in most static type systems while avoiding the bureaucratic overhead of having to prematurely declare your types. The best languages allow for gradual typing. Prototype first then add types once the general shape of your program becomes clear.
      - choeger 5mo ago
        You seem to have no idea what you're talking about. Type theory is a thing, much older than any compiler. And soundness has a meaning. > It just means type errors are checked at runtime instead of compile time. This is a fundamental misconception. A type checker proves the absence of errors. It doesn't check for error conditions. That is: A program that isn't (cannot be proven to be) well-typed can very well be correct. But a program that is well-typed is guaranteed to be free from certain errors. What you call "dynamically typed", in contrast, is comsequent just value inspection and stopping the evaluation/execution early. A program that has been executed successfully often is not necessarily correct.
  - teaearlgraycold 5mo ago
    Yes to dynamic typing. Yes to static analysis.
    - Pay08 5mo ago
      What?
      - teaearlgraycold 5mo ago
        TypeScript!
  - antonvs 5mo ago
    Technically, in a type theory context, there’s no such thing as “dynamic typing”. Types are a static, syntactic property of programs. The correct term for languages that don’t have syntactic types is “untyped”. > Most people who think they have a problem with dynamic typing actually have a problem with weak typing. All people who say things like this have never studied computer science.
    - _flux 5mo ago
      The term unityped is used as well, and at typing level this also makes sense: you have one type called object, you put that object alongside the value object ("tag"), and then at runtime all operations on that object check if its type object provides the operation the code is trying to apply on it (or maybe each value object directly knows the operations it supports). I think I prefer this term. "syntactic type" is a weird term to me, though. Is that in common use?
      - antonvs 5mo ago
        "Unityped" is informal, and inaccurate in a type theory context. The description you gave refers to the runtime/semantic domain, not to types in the type theory sense. I used "syntactic type" to underscore that formally, typing is a syntactic system that assigns types to terms, where terms are syntactic expressions. Because of that, it's usually redundant to include "syntactic". You'll typically see it used when it's being contrasted to some other less standard approach to typing, e.g.: https://blog.sigplan.org/2019/10/17/what-type-soundness-theorem-do-you-really-want-to-prove/ https://blog.sigplan.org/2019/10/17/what-type-soundness-theo...
  - pie_flavor 5mo ago
    The standard complaint of pointless type errors that static type analysis would catch has nothing to do with weak typing, nor does the other one about unreliable listing of available ops in your editor by pressing `.` and looking at the autocomplete list. If you think the only thing people think is wrong about dynamic typing is JS `==` then you are swinging at a strawman from a decade ago.
    - Pay08 5mo ago
      In every IDE I have ever used, the autocomplete hasn't been a problem. They at the very least tend to put the concrete type you're working with at the top of the list. As for type errors, the strictness that static typing enforces is simply not needed in the majority of cases. And in the ones where it is needed, most languages I know provide a way for you to enforce the usage of the correct type.
      - pie_flavor 5mo ago
        What's that supposed to mean? If I say `def foo(x)`, what autocomplete do I get off `x.`?
  - DonaldPShimoda 5mo ago
    There is no consistent definition of the term "weak typing". Do you mean implicit coercion? > Most people who think they have a problem with dynamic typing actually have a problem with weak typing. Ironically, I would counter that, in my experience, most people who have a problem with static typing actually have a problem with verbose type systems, like Java's or C++'s — or Rust's. (Rust is at least gaining something for its verbosity.) Type inference is a neat way to bridge the gap. OCaml, Haskell, and Swift (to name a few) all feature distinct type inferencing that give you the benefits of static types without as much syntactic overhead.
    - QuadmasterXLII 5mo ago
      I deeply deeply want to love OCaml but its inherent lack of dynamic dispatch for int / float / complex is brutal
    - gwerbin 5mo ago
      Nim type inference was a joy to use although I haven't touched the language in several years due to the language community seeming to collapse a bit.
    - Pay08 5mo ago
      To be clear, I don't have a problem with static typing. It has it's place, but all things being equal, I prefer dynamic (or even better, gradual) typing. I never put much water into the various verbosity criticisms, whether it's about type systems or file reading in Java.
  - gwerbin 5mo ago
    Sorta? Python has fairly strong types but it's no fun debugging a `None has no attribute foo` error deep inside some library function with a call site 1000 LoC away from the actual place where the erroneous None originally arose, due to a typo. It's not just Python too, I've hit the same issue in Common Lisp. Yes one can run contracts and unit tests and static analysis, but what's a type checker anyway other than a very strict static analysis tool?
  - pjmlp 5mo ago
    Dynamic typing doesn't scale in large teams, it is however great in small projects, or if optional typing is supported, which took a long time to learn from languages like structured BASIC dialects. It is no accident that all mainstream dynamic languages now have optional typing support, either in the language directly or via linters.
    - Pay08 5mo ago
      Oh yeah, I'm massively in favour of gradual typing. Python's choice to not actually enforce type hints is perhaps the most moronic language design I've ever seen.
  - mamcx 5mo ago
    > Most people who think they have a problem with dynamic typing actually have a problem with weak typing. No, the real actual problem is with invisibility aka: the absence of readability: In a "dynamic typing" program the interpreter knows what `a` is but YOU not. In very strong sense. You can imagine that `a` is a `int` because, well, you write the program, right? But in fact, is only probabilistic assumption. Some day, `a` will be a program that delete the files of your computer.
Serhii-Set 5mo ago
[dead]
drabbiticus 5mo ago
Can someone help confirm whether I understand correctly the semantics difference between the final-line eval of x^ vs. x* ? It seems like either one evaluates the contents of the `box`, and would only make a difference if you tried to use `x` afterwards? Essentially if you final-line eval `x^` and then decide you want to continue that snippet, you can't use `x` anymore because it's been moved. Awkwardly, it also hasn't been assigned so I'm not sure the box is accessible anymore?
- jamii 5mo ago
  > It seems like either one evaluates the contents of the `box`, and would only make a difference if you tried to use `x` afterwards? More or less. x^ moves the whole box whereas x* copies the contents of the box. > Awkwardly, it also hasn't been assigned so I'm not sure the box is accessible anymore? Yes, if you move something and don't assign it then it gets dropped, same as rust.
  - drabbiticus 5mo ago
    Great, thanks for the clarification!
16603366004 5mo ago
[dead]

91 points by jamii 5mo ago

In my programming language I have some sort of "borrowing" too (although it's named differently). But my language has no dynamic typing, only static typing is used and thus all checks are compile-time and have no runtime cost. Why bothering with dynamic typing and paying runtime costs for it?

jamii 5mo ago
> The goal is that most of your code can have the assurances of static typing, but you can still opt in to dynamically-typed glue code to handle repls, live code reloading, runtime code generation, malleable software etc.
Pay08 5mo ago
Dynamic typing is neat, I actually prefer it to static typing. Most people who think they have a problem with dynamic typing actually have a problem with weak typing.
- choeger 5mo ago
  Dynamic typing is no typing. The point of types is to prove the absence of errors. Dynamic typing just has these errors well-structured and early, but they're still errors.
  - Pay08 5mo ago
    Errors that you can recover from. I simply appreciate the added flexibility. Have you ever tried making a container of arbitrary types in C++?
    - lmm 5mo ago
      If C++ was the only static type system I'd experienced, I would also think it was a bad idea. Have you ever used an ML-family language?
      - Pay08 5mo ago
        Nope. Closest thing I have used was probably Haskell.
        lmm 5mo ago
        Haskell ought to be good enough. Did you struggle with making your containers there?
        Pay08 5mo ago
        Interestingly enough, I have never needed them there. Granted, I have written a few orders of magnitude less Haskell than I have C++. Still, the difference is worth interrogating (when I'm less sleep deprived).
    - SuperV1234 5mo ago
      You cannot do anything meaningful with a container of arbitrary types, it's just bad design. If you want to apply the same operation on all of them, then they share some API commonality -- therefore you can use polymorphism or type erasure. If they don't, you still need to know what types they are -- therefore you can use `std::variant`. If they really are unrelated, why are you storing them together in the same container? Even then, it's trivial in C++: `std::vector<std::any>`.
  - cardanome 5mo ago
    > The point of types is to prove the absence of errors Maybe for you. Originally static typing was to make the job of the compiler easier. Dynamic typing was seen as a feature that allows for faster prototyping. And no, dynamic typing does not mean untyped. It just means type errors are checked at runtime instead of compile time. You can have strongly typed dynamic languages. Common Lisp is a very good example. Weak typing is a design mistake. Dynamic typing has its place as it allows you to have types that are impossible to express in most static type systems while avoiding the bureaucratic overhead of having to prematurely declare your types. The best languages allow for gradual typing. Prototype first then add types once the general shape of your program becomes clear.
    - choeger 5mo ago
      You seem to have no idea what you're talking about. Type theory is a thing, much older than any compiler. And soundness has a meaning. > It just means type errors are checked at runtime instead of compile time. This is a fundamental misconception. A type checker proves the absence of errors. It doesn't check for error conditions. That is: A program that isn't (cannot be proven to be) well-typed can very well be correct. But a program that is well-typed is guaranteed to be free from certain errors. What you call "dynamically typed", in contrast, is comsequent just value inspection and stopping the evaluation/execution early. A program that has been executed successfully often is not necessarily correct.
- teaearlgraycold 5mo ago
  Yes to dynamic typing. Yes to static analysis.
  - Pay08 5mo ago
    What?
    - teaearlgraycold 5mo ago
      TypeScript!
- antonvs 5mo ago
  Technically, in a type theory context, there’s no such thing as “dynamic typing”. Types are a static, syntactic property of programs. The correct term for languages that don’t have syntactic types is “untyped”. > Most people who think they have a problem with dynamic typing actually have a problem with weak typing. All people who say things like this have never studied computer science.
  - _flux 5mo ago
    The term unityped is used as well, and at typing level this also makes sense: you have one type called object, you put that object alongside the value object ("tag"), and then at runtime all operations on that object check if its type object provides the operation the code is trying to apply on it (or maybe each value object directly knows the operations it supports). I think I prefer this term. "syntactic type" is a weird term to me, though. Is that in common use?
    - antonvs 5mo ago
      "Unityped" is informal, and inaccurate in a type theory context. The description you gave refers to the runtime/semantic domain, not to types in the type theory sense. I used "syntactic type" to underscore that formally, typing is a syntactic system that assigns types to terms, where terms are syntactic expressions. Because of that, it's usually redundant to include "syntactic". You'll typically see it used when it's being contrasted to some other less standard approach to typing, e.g.: https://blog.sigplan.org/2019/10/17/what-type-soundness-theorem-do-you-really-want-to-prove/ https://blog.sigplan.org/2019/10/17/what-type-soundness-theo...
- pie_flavor 5mo ago
  The standard complaint of pointless type errors that static type analysis would catch has nothing to do with weak typing, nor does the other one about unreliable listing of available ops in your editor by pressing `.` and looking at the autocomplete list. If you think the only thing people think is wrong about dynamic typing is JS `==` then you are swinging at a strawman from a decade ago.
  - Pay08 5mo ago
    In every IDE I have ever used, the autocomplete hasn't been a problem. They at the very least tend to put the concrete type you're working with at the top of the list. As for type errors, the strictness that static typing enforces is simply not needed in the majority of cases. And in the ones where it is needed, most languages I know provide a way for you to enforce the usage of the correct type.
    - pie_flavor 5mo ago
      What's that supposed to mean? If I say `def foo(x)`, what autocomplete do I get off `x.`?
- DonaldPShimoda 5mo ago
  There is no consistent definition of the term "weak typing". Do you mean implicit coercion? > Most people who think they have a problem with dynamic typing actually have a problem with weak typing. Ironically, I would counter that, in my experience, most people who have a problem with static typing actually have a problem with verbose type systems, like Java's or C++'s — or Rust's. (Rust is at least gaining something for its verbosity.) Type inference is a neat way to bridge the gap. OCaml, Haskell, and Swift (to name a few) all feature distinct type inferencing that give you the benefits of static types without as much syntactic overhead.
  - QuadmasterXLII 5mo ago
    I deeply deeply want to love OCaml but its inherent lack of dynamic dispatch for int / float / complex is brutal
  - gwerbin 5mo ago
    Nim type inference was a joy to use although I haven't touched the language in several years due to the language community seeming to collapse a bit.
  - Pay08 5mo ago
    To be clear, I don't have a problem with static typing. It has it's place, but all things being equal, I prefer dynamic (or even better, gradual) typing. I never put much water into the various verbosity criticisms, whether it's about type systems or file reading in Java.
- gwerbin 5mo ago
  Sorta? Python has fairly strong types but it's no fun debugging a `None has no attribute foo` error deep inside some library function with a call site 1000 LoC away from the actual place where the erroneous None originally arose, due to a typo. It's not just Python too, I've hit the same issue in Common Lisp. Yes one can run contracts and unit tests and static analysis, but what's a type checker anyway other than a very strict static analysis tool?
- pjmlp 5mo ago
  Dynamic typing doesn't scale in large teams, it is however great in small projects, or if optional typing is supported, which took a long time to learn from languages like structured BASIC dialects. It is no accident that all mainstream dynamic languages now have optional typing support, either in the language directly or via linters.
  - Pay08 5mo ago
    Oh yeah, I'm massively in favour of gradual typing. Python's choice to not actually enforce type hints is perhaps the most moronic language design I've ever seen.
- mamcx 5mo ago
  > Most people who think they have a problem with dynamic typing actually have a problem with weak typing. No, the real actual problem is with invisibility aka: the absence of readability: In a "dynamic typing" program the interpreter knows what `a` is but YOU not. In very strong sense. You can imagine that `a` is a `int` because, well, you write the program, right? But in fact, is only probabilistic assumption. Some day, `a` will be a program that delete the files of your computer.

Serhii-Set 5mo ago

[dead]

drabbiticus 5mo ago

Can someone help confirm whether I understand correctly the semantics difference between the final-line eval of x^ vs. x* ? It seems like either one evaluates the contents of the `box`, and would only make a difference if you tried to use `x` afterwards? Essentially if you final-line eval `x^` and then decide you want to continue that snippet, you can't use `x` anymore because it's been moved. Awkwardly, it also hasn't been assigned so I'm not sure the box is accessible anymore?

jamii 5mo ago
> It seems like either one evaluates the contents of the `box`, and would only make a difference if you tried to use `x` afterwards? More or less. x^ moves the whole box whereas x* copies the contents of the box. > Awkwardly, it also hasn't been assigned so I'm not sure the box is accessible anymore? Yes, if you move something and don't assign it then it gets dropped, same as rust.
- drabbiticus 5mo ago
  Great, thanks for the clarification!

16603366004 5mo ago

[dead]