4 ms·

That reminds me a problem I thought I had in STYX... For a few months I had the feeling that a good switch-expression requires the bottom type... It turns out

That reminds me a problem I thought I had in STYX... For a few months I had the feeling that a good switch-expression requires the bottom type... It turns out that the `assert(0)` idiom, used in a lambda, is sufficient: var u32 a = switch b do { 1 => 2, /* ... */ else => function(): u32 => {assert(0, "crash");}() }; The `else` case (similar to C `default`) simply crashes the program but the type system is happy because the lambda return type is compatible.

lloeki 3y ago
Makes me think of other similar cases raised by typing systems. In my Ruby case this is RBS (+ Steep). A typical pattern is to use `__FILE__` or `__dir__` which are references to respectively the current file path and the current file's dir path. It's quite frequent to see the following - highly summarised - idiom: # in foo.rb JSON.parse(File.read(File.join(__dir__, 'some/data.json'))) Here type checking yells at you, because the signature of `__FILE__` and `__dir__` is: () -> String | nil Which intuitively makes no sense at first! But then you realise that the signature is such because if you `eval` some Ruby code then neither can return a file path: irb> eval('__dir__') => nil But after all this code is in a file! It can't return `nil`! Or, can it? irb> eval(File.read('foo.rb')) (irb):1:in `join': no implicit conversion of nil into String (TypeError) Ah. So maybe you know that your code never does that. So to satisfy the typing system, you do: JSON.parse(File.read(File.join(__dir__ || some_fallback, 'some/data.json'))) Where `some_fallback` may be a sane value, or another way to get to the proper path, or just `raise "this file is not meant to be eval'd"`. And well, maybe it doesn't today and in the future it will†; or maybe you have some third party tooling that ends up doing just that†. It feels like useless boilerplate, but in a way the typing system is totally right, and just made you make your code more robust. Back to the switch case, I had a few similar situations, and for the life of me I could not figure why it was yelling at me. "That should not happen. That cannot happen. These are the only types that can get through." Well, thinking it through it turns out again that it was totally right and I missed a very specific and legit case in another part, and handing that case (through either conversion, guard clause, or adding the case in switch) was completely warranted. Aaaand back to TFA IIUC it seems to propose something like: # instead of this begin case (parsed = parse(input)) when Integer then handle_int(parsed) when Float then handle_float(parsed) ... end rescue ParseError ... end # or this begin parsed = parse(input) rescue ParseError ... end case parsed when Integer then handle_int(parsed) when Float then handle_float(parsed) ... end # it suggests this, which feels very Ruby, like `def ... rescue ... end` case (parsed = parse(input)) when Integer then handle_int(parsed) when Float then handle_float(parsed) rescue ParseError ... end # which is actually equivalent to this, and not the first example which wraps around the whole thing, including when clauses case ( parsed = begin parse(input) rescue ParseError ... end ) when Integer then handle_int(parsed) when Float then handle_float(parsed) end # and could optionally be written as this for clarity? or maybe if you write it first it applies to the case expression and if you write at the bottom it applies to the whole case block, and you can write both?? case (parsed = parse(input)) rescue ParseError ... when Integer then handle_int(parsed) when Float then handle_float(parsed) rescue HandlingError ... end # or maybe with a new keyword if it's not clear enough, but I find that a bit ugly case (parsed = parse(input)) when Integer then handle_int(parsed) when Float then handle_float(parsed) when_rescuing ParseError rescuing ParseError # what else??? end Interesting! † happened.

lloeki 3y ago

Makes me think of other similar cases raised by typing systems. In my Ruby case this is RBS (+ Steep). A typical pattern is to use `__FILE__` or `__dir__` which are references to respectively the current file path and the current file's dir path. It's quite frequent to see the following - highly summarised - idiom: # in foo.rb JSON.parse(File.read(File.join(__dir__, 'some/data.json'))) Here type checking yells at you, because the signature of `__FILE__` and `__dir__` is: () -> String | nil Which intuitively makes no sense at first! But then you realise that the signature is such because if you `eval` some Ruby code then neither can return a file path: irb> eval('__dir__') => nil But after all this code is in a file! It can't return `nil`! Or, can it? irb> eval(File.read('foo.rb')) (irb):1:in `join': no implicit conversion of nil into String (TypeError) Ah. So maybe you know that your code never does that. So to satisfy the typing system, you do: JSON.parse(File.read(File.join(__dir__ || some_fallback, 'some/data.json'))) Where `some_fallback` may be a sane value, or another way to get to the proper path, or just `raise "this file is not meant to be eval'd"`. And well, maybe it doesn't today and in the future it will†; or maybe you have some third party tooling that ends up doing just that†. It feels like useless boilerplate, but in a way the typing system is totally right, and just made you make your code more robust. Back to the switch case, I had a few similar situations, and for the life of me I could not figure why it was yelling at me. "That should not happen. That cannot happen. These are the only types that can get through." Well, thinking it through it turns out again that it was totally right and I missed a very specific and legit case in another part, and handing that case (through either conversion, guard clause, or adding the case in switch) was completely warranted. Aaaand back to TFA IIUC it seems to propose something like: # instead of this begin case (parsed = parse(input)) when Integer then handle_int(parsed) when Float then handle_float(parsed) ... end rescue ParseError ... end # or this begin parsed = parse(input) rescue ParseError ... end case parsed when Integer then handle_int(parsed) when Float then handle_float(parsed) ... end # it suggests this, which feels very Ruby, like `def ... rescue ... end` case (parsed = parse(input)) when Integer then handle_int(parsed) when Float then handle_float(parsed) rescue ParseError ... end # which is actually equivalent to this, and not the first example which wraps around the whole thing, including when clauses case ( parsed = begin parse(input) rescue ParseError ... end ) when Integer then handle_int(parsed) when Float then handle_float(parsed) end # and could optionally be written as this for clarity? or maybe if you write it first it applies to the case expression and if you write at the bottom it applies to the whole case block, and you can write both?? case (parsed = parse(input)) rescue ParseError ... when Integer then handle_int(parsed) when Float then handle_float(parsed) rescue HandlingError ... end # or maybe with a new keyword if it's not clear enough, but I find that a bit ugly case (parsed = parse(input)) when Integer then handle_int(parsed) when Float then handle_float(parsed) when_rescuing ParseError rescuing ParseError # what else??? end Interesting! † happened.