Borrow-checking without type-checking (scattered-thoughts.net)
68 points by jamii 9 hours ago
Panzerschrek 7 hours 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 7 hours 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 6 hours 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.
pie_flavor 2 hours 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.
teaearlgraycold 6 hours ago
Yes to dynamic typing. Yes to static analysis.
Pay08 5 hours ago
antonvs 6 hours 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 5 hours ago
choeger 6 hours 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.
cardanome an hour ago
Pay08 5 hours ago
drabbiticus 3 hours ago
Can someone help confirm whether I understand correctly the semantics difference between the final-line eval of
x^
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?