[grumpyprole]

> only enforces the rather weak constraint that you cannot access a non-error return value in the case where the function returns an error.

This "rather weak constraint" as you put it, completely solves Tony Hoare's "billion dollar mistake": null pointer exceptions. Something Go also suffers from due to lack of Sum types. With regard to your Rust example, the compiler will give a warning that can be turned into an error to completely prevent this, if desired.

As the parent said, sum types are "foundational" and have many applications for writing safe statically checked code. Eradicating null pointers and enabling chainable result types are only the tip of the iceberg.

[foldr]

> This "rather weak constraint" as you put it, completely solves Tony Hoare's "billion dollar mistake": null pointer exceptions.

Yes. However, it doesn’t do what you seemed to be suggesting that it does, which is “catch all failures to handle errors”. You correctly note that Go’s linters can’t always do this, but also seem to erroneously suggest that Rust’s type system somehow can. This is backwards. Go’s error linters catch most instances of ignored error values, whereas Rust’s type system doesn’t do anything, in and of itself, to ensure that error values are not ignored. Of course there are compiler warnings to catch unused errors in Rust, but that’s fundamentally the same thing as the warnings you get from Go linters, and has nothing really to do with sum types. Whether or not an error is ‘ignored’ or ‘used’ in any interesting sense is not a formal property of a program that can be formally verified. (Yes, linear types, etc. etc., but you can formally use an error value in that sense while in practice ignoring the error.)

By the way, you don’t have to preach to me (or really anyone on HN) about the virtues of sum types. I’ve written a fair amount of Haskell and Rust code. My issue here is not with the utility of sum types, but with the erroneous claim that they somehow remove the need for linters or compiler warnings that flag unhandled errors.

[grumpyprole]

> but also seem to erroneously suggest that Rust’s type system somehow can.

I didn't bring Rust into this discussion, it is hardly a model implementation of sum types and using them for proofs, but it is certainly a step in the right direction.

> My issue here is not with the utility of sum types, but with the erroneous claim that they somehow remove the need for linters or compiler warnings

You are misrepresenting my posts, I am responding to an erroneous claim that linters are a satisfactory substitute for sum types.

[foldr]

Thread A:

>> no chance of forgetting to check the error, and works just as well as a stronger type system

>A linter-based syntactic check is no substitute for a proper type system. A type system gives a machine checked proof. A heuristic catches some but not all failures to handle errors, it will also give false positives.

Thread B:

> Go's lack of sum types mean that there is no static check for whether the error has actually been handled or not.

>>I dunno, my IntelliJ calls out unhandled errors. I imagine go-vet does as well.

>>>A simple syntactic check will only ever work as a heuristic. Heuristics don't work for all cases and can be noisy. The point is, no modern language should need such hacks. This problem was completely solved in the 70s with sum types. [emphasis mine]

What you said in these two threads seemed to suggest that the functionality of Go error linters can be subsumed by a 'proper type system' that includes sum types, and that such a type system would catch all failures to handle errors. But sum types by themselves do nothing to force handling of errors. You could add sum types to Go and you'd still need a linter to perform the exact same error handling checks that Go linters currently perform. Whatever kind of value a fallible function returns, you can always ignore that value as far as the type checker is concerned (unless you add something like linear types to your type system, which are orthogonal to sum types).

Apologies for the confusion re Rust. For Rust just read 'a language that handles errors using sum types'.

[grumpyprole]

> Sum types by themselves do nothing to force handling of errors,

If you have Haskell experience, then have you ever wondered how it is considered "null safe" and does not throw null pointer exceptions? Perhaps it is because optional "Maybe" types (the simplest form of error) must be explicitly unpacked? Yes, Haskell, being an old language without a sound type system, permits "fromJust" and its exceptions (a side effect) are not tracked like other effects. But despite this, are you seriously claiming that sum types "do nothing" to achieve this null safety?

If you want to understand the full proving power of sum types, I do not suggest Rust or Haskell as a model example. Coq, Agda, Idris or ATS will be better examples.

[foldr]

>But despite this, are you seriously claiming that sum types "do nothing" to achieve this null safety?

No. I said nothing about null safety. What I said is that “sum types by themselves do nothing to force handling of errors”. In fact I imagine that’s one of the reasons that Haskell uses exceptions for error handling in the IO monad. If Haskell had a non-raising function like

    openFile :: FilePath -> IOMode -> IO (Either IOError Handle)

then you could of course attempt to open a file without checking for an error:

    main :: IO ()
    main = do
        openFile “/foo/bar” ReadMode
        putStrLn “Did the file open successfully? No idea”

Sum types (by themselves) cannot be used to prove that all errors have been handled. In fact, formal proofs of this property using other type system features (such as linear types) are of fairly limited practical value, given that merely 'using' an error value in some type-theoretic sense doesn't necessarily entail actually taking appropriate action to handle it.

[grumpyprole]

> No. I said nothing about null safety. What I said is that “sum types by themselves do nothing to force handling of errors”.

Maybe (null) types are the simplest form of error type, with null pointer exceptions being the simplest from of unhandled error. They are therefore the easiest example to illustrate my point. You cannot simply choose to ignore them and remain credible. Haskell's broken old IO APIs are hardly a model example. Your Haskell code will at least give a compiler warning for ignoring the output. I would configure the compiler to turn this into an error.