Gradual typing seems like the worst of all worlds. You spend time adding typing but can't depend on it consistently. I was surprised using Dart that it would throw runtime type exceptions even though it looked like the code had explicit types.
So, that makes me notice I didn't clearly explain, that my idea here would be for some kind of guard blocks that enforce static typing (etc.) in some areas of code. Kinda similar to "unsafe" in Rust: ideally, you could start with e.g. fully dynamically typed code, then mark some parts of it with "I want this area typechecked", finally requiring all of it to be. Now that I think of it, seeing that in statically typed languages you can kinda already do this (with "Any" type, or "void*", or "interface{}", or whatsit), you could e.g. imagine marking some code blocks with a pragma "any=default" or "any=allowed" or "any=forbidden". So:
- "any=default" - marking the block as dynamically typed and not needing type annotations everywhere (but maybe allowing them if I want, and typechecking then if possible?) - modulo any inference;
- "any=allowed" - marking a block as "statically typed" with type annotations required, and "Any" allowed ("classical static typing");
- "any=forbidden" - would mark the block as statically typed with "Any" not allowed at all.
I'd then start by coding with whole codebase being "any=default", making it work like in JS/Python/Lua/...; then if happy with the prototype, I'd switch the whole codebase to "any=forbidden" and have the compiler force me to add type annotations. Finally if I know in some areas I really want the "Any", I'd mark some small blocks with "any=allowed", working as kinda "unsafe" marker in Rust. (Obviously, subject to bikeshedding over the specific pragma naming & modes.)
Similarly, I'd like to have another pragma for errors handling strictness (regardless whether actual error handling is done in a Rust-like "Result" way, in Go/Lua-like "soft-Result" way, or in an "exceptions" way), and for proving.
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.
So, 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>
Well, 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.
