4 ms·

No language has a 'static check for whether the error has actually been handled or not'. In Rust, for example, you can just 'unwrap' an error. In Haskell you

No language has a 'static check for whether the error has actually been handled or not'. In Rust, for example, you can just 'unwrap' an error. In Haskell you can use 'fromJust'. And in Go you can just ignore 'err' and assume it is 'nil'. Sum types might be the 'mathematical dual of product types' but programming languages are not mathematics. The possibly implementations of sum types are quite varied. It makes sense in low-level languages for the programmer to use what makes sense in the particular situation.

grumpyprole 3y ago
Unwrap and fromJust can be disallowed if need be, they are "unsafe" convenience functions whose use can and should be tracked. Not all languages with sum types will permit them. Rust also has "unsafe" code blocks, should we also claim it is therefore not memory safe? Some would try to do so, but at least this unsafe code is tracked and not idiomatic. > programming languages are not mathematics This may be how you choose to view them. But many of us seeking to build safer and more correct software aim to make programming more like mathematics. Mathematics tells us how to compose and tells us how to prove. Both things the software industry is currently failing at.
- memefrog 3y ago
  >Unwrap and fromJust can be disallowed if need be, they are "unsafe" convenience functions whose use can and should be tracked. And with the same sort of third-party tools you use to 'track' those and ensure they're not used, you can track unused error returns in Go or C. > Not all languages with sum types will permit them. All do. >Rust also has "unsafe" code blocks, should we also claim it is therefore not memory safe? Some would try to do so, but at least this unsafe code is tracked and not idiomatic. Absolutely we should! Rust fanatics try to claim it is a memory-safe language when it isn't. Real memory-safe languages like Java have existed for far longer. >This may be how you choose to view them. But many of us seeking to build safer and more correct software aim to make programming more like mathematics. Mathematics tells us how to compose and tells us how to prove. Both things the software industry is currently failing at. You missed the entire point of what I said.
  - grumpyprole 3y ago
    > All do No, this is not true. A total functional programming language can disallow partial functions that circumvent the type checker. Again, linters only get you so far. For example, sum types eradicate null pointer exceptions, linters do not.
    - memefrog 3y ago
      I don't give a shit what languages CAN do in theory. I care what languages DO do. And all languages (that aren't research projects like agda) provide escape hatches here. Even Haskell. >Again, linters only get you so far You brought up linters. Not me.
      - valenterry 3y ago
        He still has a point. In theory you might need a language like Idris/Agda, but in praxis it still makes a big difference. It is true that you will see that a function can return an error and that you choose to ignore it. It's also true that you can do the same in many other languages that use sumtypes. But it is still different. Because while ignoring an error in go is as easy as putting an underscore next to the happy-case, in languages with sumtypes that doesn't work. The equivalent in other languages would be to return a struct and then just access one value and ignore the other one. In that case, the practical implications would be the same. But when using a sumtype, a few things change. First, you can not just access the happy-case value, you are (or at least can be) forced to also "access" the unhappy-case value. Either in a pattern match, in a fold-function and so on. You know have to return something, even if it is an empty value our "escaping" by throwing an error. On top of that, what happens if a function can partially succeed? Take a graphql request as a practical example where this is quite common. With Go's style of error handling, how do you model that? I.e. say you need to redactor a function that previously either succeeded or failed into one that now can partially succeed and fail. In a language with sumtypes I would now switch from a sumtype Success|Error to more complex type Success|Error|PartialSuccess which makes it a breeze to refactor my code because the compiler will tell me all the places where I have to consider a new case and what it is. I'm genuinely curious, how would you model that in Go and what implication would such a refactoring have on existing code? I imagine it would be quite different in praxis.

grumpyprole 3y ago

Unwrap and fromJust can be disallowed if need be, they are "unsafe" convenience functions whose use can and should be tracked. Not all languages with sum types will permit them. Rust also has "unsafe" code blocks, should we also claim it is therefore not memory safe? Some would try to do so, but at least this unsafe code is tracked and not idiomatic. > programming languages are not mathematics This may be how you choose to view them. But many of us seeking to build safer and more correct software aim to make programming more like mathematics. Mathematics tells us how to compose and tells us how to prove. Both things the software industry is currently failing at.

memefrog 3y ago
>Unwrap and fromJust can be disallowed if need be, they are "unsafe" convenience functions whose use can and should be tracked. And with the same sort of third-party tools you use to 'track' those and ensure they're not used, you can track unused error returns in Go or C. > Not all languages with sum types will permit them. All do. >Rust also has "unsafe" code blocks, should we also claim it is therefore not memory safe? Some would try to do so, but at least this unsafe code is tracked and not idiomatic. Absolutely we should! Rust fanatics try to claim it is a memory-safe language when it isn't. Real memory-safe languages like Java have existed for far longer. >This may be how you choose to view them. But many of us seeking to build safer and more correct software aim to make programming more like mathematics. Mathematics tells us how to compose and tells us how to prove. Both things the software industry is currently failing at. You missed the entire point of what I said.
- grumpyprole 3y ago
  > All do No, this is not true. A total functional programming language can disallow partial functions that circumvent the type checker. Again, linters only get you so far. For example, sum types eradicate null pointer exceptions, linters do not.
  - memefrog 3y ago
    I don't give a shit what languages CAN do in theory. I care what languages DO do. And all languages (that aren't research projects like agda) provide escape hatches here. Even Haskell. >Again, linters only get you so far You brought up linters. Not me.
    - valenterry 3y ago
      He still has a point. In theory you might need a language like Idris/Agda, but in praxis it still makes a big difference. It is true that you will see that a function can return an error and that you choose to ignore it. It's also true that you can do the same in many other languages that use sumtypes. But it is still different. Because while ignoring an error in go is as easy as putting an underscore next to the happy-case, in languages with sumtypes that doesn't work. The equivalent in other languages would be to return a struct and then just access one value and ignore the other one. In that case, the practical implications would be the same. But when using a sumtype, a few things change. First, you can not just access the happy-case value, you are (or at least can be) forced to also "access" the unhappy-case value. Either in a pattern match, in a fold-function and so on. You know have to return something, even if it is an empty value our "escaping" by throwing an error. On top of that, what happens if a function can partially succeed? Take a graphql request as a practical example where this is quite common. With Go's style of error handling, how do you model that? I.e. say you need to redactor a function that previously either succeeded or failed into one that now can partially succeed and fail. In a language with sumtypes I would now switch from a sumtype Success|Error to more complex type Success|Error|PartialSuccess which makes it a breeze to refactor my code because the compiler will tell me all the places where I have to consider a new case and what it is. I'm genuinely curious, how would you model that in Go and what implication would such a refactoring have on existing code? I imagine it would be quite different in praxis.