5 ms·

Re. 3 & 5: my theory is that a language with gradual typing, gradual error handling enforcement, and "gradual proving" that is seamlessly embedded in it (see e.

by akavel 5y ago

Re. 3 & 5: my theory is that a language with gradual typing, gradual error handling enforcement, and "gradual proving" that is seamlessly embedded in it (see e.g. the https://nim-lang.org/docs/drnim.html https://nim-lang.org/docs/drnim.html experiment) could hopefully actually work here. And as to dynamic typing, I found it useful when prototyping, to quickly PoC/MVP the "happy path" of an idea/design, and see if it is worth investing any bigger effort, or just completely crap. Ideally I'd then (gradually) enable (or, "un-disable") statical typing, error handling enforcement, and formal proving. Question is, can anyone design & implement a language that would have all of that, and still be readable and understandable to a common programmer (like me). Re. 6: for API design, I have some (feeble) hopes behind https://aip.dev https://aip.dev; as to the rest, I have immense hopes behind https://enso.org https://enso.org

Chris2048 5y ago
The problem isn't best case scenario, but possibility of abuse. gradual typing is an easy way to acquire more tech debt once tickets are closed and no-one comes back to add more types. Corps like a simple plan->code->test->done without any "return" to code considered "done".
Chris2048 5y ago
Is that enso software related to the software launcher by Aza Raskin?
- akavel 5y ago
  Noo, I don't think so, from googling what you describe it seems just a clash of names.
musingsole 5y ago
> Question is, can anyone design & implement a language that would have all of that, and still be readable and understandable to a common programmer No, because exception handling and the answer to "what type are these data?" are product questions. Hard questions that no one really wants to work out because what if our customer base wants something completely different in 6 months? This is largely reflected in cloud providers being unwilling/unable to provide account spend caps: what is a sane response once the budget goes over? AWS can't tell you; only you can define it. (This isn't to say "there's nothing AWS can do for you here" -- they could but won't for other reasons). Python is the largest, common language that can support gradual checking systems being added in over time, and mypy has outlined a great framework for doing just that. But it's not a silver bullet and can't be because the problems are cultural, not mathematic. Either spend the time working out what you want your software to do, or don't. But don't argue "strictness" is "correctness".
- fatbird 5y ago
  But don't argue "strictness" is "correctness" I feel my mind expanding right now the same way I did when I first heard "concurrency and parallelism aren't the same thing".
- akavel 5y ago
  Hm; I guess when being in talks with a company using the language, assuming the pragmas idea I elaborated in a cousin comment, I'd then be asking questions like: "Is your codebase any=default or any=forbidden? What percentage of it is any=allowed?" (Instead of the current: "are you using JS, Go, or Rust?") Notably, in my particular case, what you say is a problem is exactly why I want it: because when writing the PoC, I don't really know what I'm doing yet; and I want to only sketch it. Once I see the sketch and it looks like the general idea has some promise, I want to "grab the pen and start drawing" - i.e. start diving into the nitty-gritty dark corners of ugly interactions, corner cases, & stability, as a way of better understanding & exploring my domain/project/idea (specifically, using the compiler as a tool that is forcing me to do that, by asking me difficult questions). And I may want it graded in various areas of my codebase: some are super unimportant or still being explored, and I'm ok having them explicitly marked as "sketchy"; others are where I really care about extreme security, so want full prover power, and I want to know their exact boundaries too; finally, some are the "more or less know what I'm doing, but not life-critical" to bigger or lesser extent; notably with some small corners marked with an explicit "caution: here be dragons" `unsafe` (I mean, `any=allowed`) yellow tape.
eweise 5y ago
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.
- akavel 5y ago
  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.
  - 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.

by akavel 5y ago

Chris2048 5y ago

The problem isn't best case scenario, but possibility of abuse. gradual typing is an easy way to acquire more tech debt once tickets are closed and no-one comes back to add more types. Corps like a simple plan->code->test->done without any "return" to code considered "done".

Chris2048 5y ago

Is that enso software related to the software launcher by Aza Raskin?

akavel 5y ago
Noo, I don't think so, from googling what you describe it seems just a clash of names.

musingsole 5y ago

> Question is, can anyone design & implement a language that would have all of that, and still be readable and understandable to a common programmer No, because exception handling and the answer to "what type are these data?" are product questions. Hard questions that no one really wants to work out because what if our customer base wants something completely different in 6 months? This is largely reflected in cloud providers being unwilling/unable to provide account spend caps: what is a sane response once the budget goes over? AWS can't tell you; only you can define it. (This isn't to say "there's nothing AWS can do for you here" -- they could but won't for other reasons). Python is the largest, common language that can support gradual checking systems being added in over time, and mypy has outlined a great framework for doing just that. But it's not a silver bullet and can't be because the problems are cultural, not mathematic. Either spend the time working out what you want your software to do, or don't. But don't argue "strictness" is "correctness".

fatbird 5y ago
But don't argue "strictness" is "correctness" I feel my mind expanding right now the same way I did when I first heard "concurrency and parallelism aren't the same thing".
akavel 5y ago
Hm; I guess when being in talks with a company using the language, assuming the pragmas idea I elaborated in a cousin comment, I'd then be asking questions like: "Is your codebase any=default or any=forbidden? What percentage of it is any=allowed?" (Instead of the current: "are you using JS, Go, or Rust?") Notably, in my particular case, what you say is a problem is exactly why I want it: because when writing the PoC, I don't really know what I'm doing yet; and I want to only sketch it. Once I see the sketch and it looks like the general idea has some promise, I want to "grab the pen and start drawing" - i.e. start diving into the nitty-gritty dark corners of ugly interactions, corner cases, & stability, as a way of better understanding & exploring my domain/project/idea (specifically, using the compiler as a tool that is forcing me to do that, by asking me difficult questions). And I may want it graded in various areas of my codebase: some are super unimportant or still being explored, and I'm ok having them explicitly marked as "sketchy"; others are where I really care about extreme security, so want full prover power, and I want to know their exact boundaries too; finally, some are the "more or less know what I'm doing, but not life-critical" to bigger or lesser extent; notably with some small corners marked with an explicit "caution: here be dragons" `unsafe` (I mean, `any=allowed`) yellow tape.

eweise 5y ago

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.

akavel 5y ago
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.
- 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.