61–64 of 64 posts
I didn't expect this to get posted here. Long time lurker here. I'm really interested in programming language design and ergonomics. What niche PL features would you like to see have more adoption?
This makes it easier to split raw inputs from validated inputs and delimiting where they are used in the code.
Earlier quoted context omitted.
Rust already supports the kind of behaviour you are describing for borrows, because of non-lexical lifetimes. Code like the following now compiles: fn main() { let mut x = 42; let y = &x; println!("{y}"); let z = &mut x; } Even though y's scope overlaps with z's, and they introduce conflicting borrows, this code compiles because the compiler treats y's borrow as dead after its last use (this has been true since Rust…
> If you didn't have that guarantee, at worst your mutex's guard object would be immediately dropped For named local variables it's a different story. They should remain alive until the end of their lexical scope. But for unnamed temporaries created in expressions different rules should apply - as soon as there is no reference to such temporary, it should be destroyed.
https://smallcultfollowing.com/babysteps/blog/2023/03/15/tem...
Typically, a temporary's lifetime is bounded by the statement it is in, but for the subject of a match, this extension overlaps with all its arms even if the temporary borrow is not used after the subject is evaluated (i.e. you borrowed, you read and copied a field out of the borrow).
The issue seems to be that this is a syntactic transformation, but the expected behaviour requires type information, so you can tell whether to extend the temporary's lifetime by whether that lifetime leaks the immediately containing scope.
This is kind of similar to how type parameter unification in Hindley-Milner works. There's even an analogy made between the two things here:
https://okmij.org/ftp/ML/generalization.html#gen-mismanageme...
Earlier quoted context omitted.
Poor man's runtime "dynamic" version. AKA: A much worse version. In advanced cases, you'd need dependent types, but the only place where that almost shows up is in the "amount "Contracts" has been around a long time and has not caught on. That's usually a good sign that better approaches are prevailing. In other words: refinement types are a better solution.
> Poor man's runtime "dynamic" version. AKA: A much worse version. Contracts don't have to be evaluated dynamically, that's just one way they're implemented. See SPARK/Ada for an example of contracts being used to prove programs statically, not just test them dynamically.
For full formal proofs it's easier to use cbmc or esbmc though
I can see how it can be useful to start with a broad type, e.g. a union, and narrow it down in a block. However, I don't quite get the opposite direction shown in their example (first an int, then a string, then a union).