Borrow-checking without type-checking • Hacker News Board

Re: Borrow-checking without type-checking

#31

Post by antonvs » Thu, Apr 23, 2026, 6:28 PM UTC

_flux wrote: post #8

antonvs wrote: post #7

Earlier quoted context omitted.

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.

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…

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

Re: Borrow-checking without type-checking

#32

Post by Pay08 » Thu, Apr 23, 2026, 6:52 PM UTC

DonaldPShimoda wrote: post #21

Pay08 wrote: post #4

Earlier quoted context omitted.

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.

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…

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.

Re: Borrow-checking without type-checking

#33

Post by Pay08 » Thu, Apr 23, 2026, 6:56 PM UTC

pie_flavor wrote: post #18

Pay08 wrote: post #4

Earlier quoted context omitted.

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.

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.

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.

Re: Borrow-checking without type-checking

#34

Post by pie_flavor » Fri, Apr 24, 2026, 2:54 AM UTC

Pay08 wrote: post #33

pie_flavor wrote: post #18

Earlier quoted context omitted.

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.

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.

What's that supposed to mean? If I say `def foo(x)`, what autocomplete do I get off `x.`?

Re: Borrow-checking without type-checking

#35

Post by choeger » Fri, Apr 24, 2026, 7:30 PM UTC

cardanome wrote: post #20

choeger wrote: post #5

Earlier quoted context omitted.

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.

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

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.