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

[grumpyprole]

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

Apologies I missed that bit, it is indeed a perfectly reasonable API.

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

We are arguing semantics as to what constitutes a "handled error". If a user chooses to explicitly throw away the error and not use the value, then you are arguing it is not handled. I am arguing that it has been handled (and checked as such). Either way sum types are a step in the right direction, despite all the shortcomings and unsound type systems of "practical" languages.