[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.

[foldr]

>with null pointer exceptions being the simplest from of unhandled error.

I don't know of any practical language that forces you to handle the Nothing condition of a Maybe. Haskell has fromJust (as you note), Rust has unwrap. I suppose Idris could become practical one day, but it's not there yet. More fundamentally, without something like linear types, nothing in the type system can force you to check that a value of a particular sum type instantiates a particular variant. You're always free to ignore values, which means that you're free to ignore error conditions.

> Haskell's broken old IO APIs are hardly a model example of anything

I don't quite see what you're getting at here. My example function isn't part of Haskell's IO API. It's an example of what Haskell's IO API might look like if it used sum types for error handling rather than throwing exceptions. I fail to see how there can be anything inherently 'broken' about a hypothetical function that opens a file and returns either a file handle or an error.

>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.

So you're saying that you'd configure the compiler to do exactly the same checks that Go error linters do...none of which have anything to do with sum types.