3 ms·
If I'm understanding you correctly, this is basically what we have with Typescript, and it's...fine, but it's not great. The difference between what you're sugg
by wk_end 5y ago
If I'm understanding you correctly, this is basically what we have with Typescript, and it's...fine, but it's not great. The difference between what you're suggesting and what Rust does is that in Rust the unsafety is lexically scoped - it concerns static code, not live data, so it can't escape the unsafe code block. Whereas in Typescript, as soon as you let an `any` flow back into the rest of the system, all bets are off.
ETA: If you're suggesting actually preventing the flow of Any-typed data out of the Any-typed blocks, well, that's going to make things pretty hard. Any-typed code wouldn't be able to call any "safe" code, because that safe code might do something like take its (presumably safe!) input and stash it away somewhere. Safe code wouldn't be able to access any unsafe data whatsoever - all calls into unsafe code would have to be completely procedural. It'd be painfully limiting.
I'll also add that it's not trivial at all to statically type a dynamically typed code base if it's exploiting that dynamism at all. "Just go back and add type annotations" could be a multi-engineer-year project requiring refactoring of huge chunks of the system. If you believe in static types, encouraging completely unprincipled dynamism at the language level for any reason besides backwards compatibility with existing dynamic code seems like a mistake.
- akavel 5y agoSo, IANAPLT, and I think that must be definitely clear now if it wasn't enough so before... but then, who says I can't dream! :D and in this dream of mine, those things seem to indeed be lexically scoped, apparently... :) As to the next thing, I feel I don't understand completely the details of what you wrote in the ETA section, but wouldn't it be similar like with unsafe in Rust? AFAIU, it's on the writer of the code in the unsafe block to ensure that whatever leaves the unsafe zone, it has its invariants all buttoned up and behaves properly back in the civilised world. As for not being trivial, I kind of maybe have to understand (I found esp. Hishamhm's presentations about the design and evolution of the Teal language, née TL a.k.a. Typed Lua, enlightening yet approachable in this regard); yet, again, IANAPLT and I can dream :) and who knows, maybe some actual PLT will look at it and say, whaa, hmmm; but is it really for sure impossible? I. AM. CURIOUS..... <cue ominous thunder>
- wk_end 5y agoWell, all I mean in the "ETA" is that if you want very robust guarantees about type safety - more robust than Rust's notion of safety - then you're going to be very, very restricted in what you can do. OTOH, if you're fine with looser guarantees about correctness, I'm not sure if marking blocks as safe/unsafe really gets you much more than Typescript, which does (with strictness turned on) force you to be explicit whenever you're using anys. And it's unclear how you can "button up" dynamic data and pass it back to the civilized world.
- 2143 5y agoWhat's IANAPLT? I googled and got nothing.
- akavel 5y agoI Am Not A Programming Language Theorist (Theoretician?...)