Lambda the Ultimate

In what way does making Maybe a monad add to its value for error handling beyond what you get as a discriminated union? Is there some extra sauce that you get beyond what something like boost::optional provides in a non-monadic language?

Maybe and boost::optional are (mostly) the same thing. Other than the fact the Boost developers are careful not to use scary words like "monad" in mixed company. :)

Maybe (and boost::optional) does provide semantics above and beyond an arbitrary discriminated union or sum type.

A few older LtU threads may be of interest:

this and this

I don't have time for a really good answer, but basically, you do get some extra sauce. Basically, you get the ability to take a bunch of computations, each of which may fail, and string them together as though none of them fail. The result of the whole thing is a discriminated union, so you ignore failure until the very end. This hides the discriminated union and becomes basically as convenient as traditional exception handling. I don't know whether boost::optional lets you compose operations in this way.

Undoing Dynamic Typing shows a clever solution to localizing deferred errors (in the context of in the interfacing statically-typed languages with dynamic-typed languages) by using control operators to rollback to the point where the error was introduced.

Monads can be used to encode an out-of-band return mechanism very similar to what's in use in Java (though you have a wide range of choices). It's not clear to me from your post whether your objections would apply to such an encoding.

I don't think I would object to it, as the mechanism used is not specific to exceptions, and the behaviour of the underlying object is fully specified algebraically (correct me if I'm wrong). So the "exceptions" are not out of band information, they are simply handled in a fashion where we can propagate them as out of band information should we like to, which I think is better.

I was merely wondering about the runtime costs of monadic structured code, how much optimization is needed for suitably efficient execution, etc. I suppose it depends how pervasive the use of monads is, but let's say it's limited to taming effects and exceptions (and not say, to CPS transform the program).

i think the fact that language-systems today have only one way to represent themselves is part of the problem. sometimes i very much don't want to see the error code. other times i only want to see the error handling. other times i want to see everything together.

I'm curious: in which situations do you not want to see the errors? I'm just wondering what you're trying to achieve while ignoring the edge cases, ie. what type of development are you typically doing in such situations: debugging, testing, writing extensions, ...?

Using error code for every errors is tedious as you see in the code all the special handling which must be chained even if you just want to report .. that's there was an error.

With exceptions the unrolling happen automatically which reduce the size of the code, too bad programming with exceptions is hard.

Using error code for every errors is tedious as you see in the code all the special handling which must be chained even if you just want to report .. that's there was an error.

Yes, this is a problem with totality when combined with closed sums. I'm looking into polymorphic variants to hopefully alleviate this somewhat. Of course, I expect actual error conditions to be fewer in total languages *because* it's somewhat tedious. I think that's a good thing actually.

[Edit: I think the cases where there's "nothing to do" are actually a symptom of this problem, namely, throwing exceptions for situations which aren't really exceptional at all. I conjecture that total languages would reduce this silliness. There's always something to do for a true error, ie. prompt the user to retry, kill a misbehaving agent, etc.]

[...] tedious as you see [...] all the special handling which must be chained [...]

Yes, this is a problem with totality when combined with closed sums. I'm looking into polymorphic variants to hopefully alleviate this somewhat.

I don't immediately see how polymorphic variants could make it easier to propagate (or chain) error conditions. OTOH, I could imagine something like polymorphic variants, rather than an open (generative) datatype, to be used as a type for exceptions (or errors) to track which cases have been handled, but that is a different problem.

Indeed, I think that the actual problem with exceptions is knowing whether you've handled all of them. It would be useful to be able to say that no exceptions can be propagated out of a particular expression.

Of course, I expect actual error conditions to be fewer in total languages *because* it's somewhat tedious.

I'm not entirely sure what you intend to mean when you say "actual error condition". According to Merriam-Webster, "actual" means "existing in fact and not merely as a possibility".

Note that programs typically need to handle two rather different kinds of error conditions: error conditions resulting from external (potentially physical) stimuli (e.g. corrupted file, network connection that fails (when the line is cut), ...), and error conditions resulting from internal software defects (bugs).

Error conditions from external stimuli cannot be eliminated by even proving the program correct. If you implement two equivalent programs, one in a total language and another in a partial language, surely they will have to handle all the same error conditions resulting from external stimuli.

OTOH, a total language might encourage (or even force) you to pay more attention to the correctness of algorithms within the program. While this would likely reduce the number of "error" conditions required to be handled by the program, it would likely increase the number of "ordinary" conditions handled by the program. I'm not saying that this would be a bad thing, but there is a trade-off.

[Edit: I think the cases where there's "nothing to do" are actually a symptom of this problem, namely, throwing exceptions for situations which aren't really exceptional at all. I conjecture that total languages would reduce this silliness. There's always something to do for a true error, ie. prompt the user to retry, kill a misbehaving agent, etc.]

I think that is misunderstanding (or misrepresenting) the role of exception handling. Sure, there is usually something to do --- given a proper context. The difficulty is that at the point in the program where you detect a problem, there might not be anything reasonable to do. This is particularly a problem with writing reusable components. At the point you detect an error in a reusable component, what can you reasonably do? The proper action depends on the context in which the component is used. The best thing you can do is to let the error be handled by another part of the program where a reasonable action can be taken. Exception handling is one way to allow that without having to explicitly propagate errors everywhere. It allows an exception handler to be defined (only) at the point in a program where a proper action can be taken.

I don't immediately see how polymorphic variants could make it easier to propagate (or chain) error conditions.

I'm thinking of something along the lines of First-class Messages with Match Functions, with some extensions.

I'm not entirely sure what you intend to mean when you say "actual error condition". According to Merriam-Webster, "actual" means "existing in fact and not merely as a possibility".

I mean errors that result from truly exceptional circumstances, such as failing hard disks, rather than from language constructs whose partiality results in "errors" (like casting exceptions, null pointer exceptions, etc.).

Error conditions from external stimuli cannot be eliminated by even proving the program correct. If you implement two equivalent programs, one in a total language and another in a partial language, surely they will have to handle all the same error conditions resulting from external stimuli.

Yes. The total language should also have already specified these edge cases, which means it has a greater chance of continuing or at least failing gracefully.

it would likely increase the number of "ordinary" conditions handled by the program. I'm not saying that this would be a bad thing, but there is a trade-off.

Well, there's nothing stopping you from using a default case and just exiting the program. That's what would happen in a partial program for unhandled exceptions, so no convenience lost IMO.

Sure, there is usually something to do --- given a proper context. The difficulty is that at the point in the program where you detect a problem, there might not be anything reasonable to do. [...] Exception handling is one way to allow that without having to explicitly propagate errors everywhere. It allows an exception handler to be defined (only) at the point in a program where a proper action can be taken.

Yes, the adage generally goes, "detect errors at a low-level, handle them at a high-level". The only two answers I have at the moment are:

1. we don't really have a total language on which to conclude how prevalent and onerous this truly is,

2. monadic code structure can replicate the necessary decoupling of error generator to error handler.

I just don't know how much overhead monads really entail. No one seems to have addressed that question of mine. :-)

I think that Coq satisfies 1. There are probably others like ACL2, Isabelle and Agda, but I'm not very familiar with them.

I recently wrote a combinator parser in Coq which required adding exceptions. I was able to use exceptions+'dependent types' to deal with things fairly straight-forwardly and it wasn't too bad. However, I wasn't able to figure out how to encode exceptions in such a way that all exceptional situations could be defined at any point in the program code, in an "as you go" type manner. That is, I ran into "The Expression Problem". This isn't a big problem for my code, but it does make it hard to imagine a component architecture using exceptions in Coq.

In looking at the expression problem, it isn't clear to me that it can be solved in Coq or any other total strongly-typed programming language without some special ingredient. It seems that all of the solutions make use of back-doors in the type system. I'm very curious if anyone knows of a solution.

Wouter Swierstra's Data types à la carte has a solution to the expression problem. It uses a type:

data Expr f = In (f (Expr f ))

It seems to me that this type displays contravariant type recursion, or as Coq told me: "Non-strictly positive occurrence of Expr". The reason for disallowing types like this is that bottom can sneak back in. I wasn't able to come up with an example using this type, but I'd be curious if anyone knows of one.

I think that Coq satisfies 1. There are probably others like ACL2, Isabelle and Agda, but I'm not very familiar with them.

You might be right. I tend to exclude Coq because it sort of evolved from OCaml, which is not only partial, which Coq obviously addresses, but also violates capability security principles (which I think are synergistic with totality, in that some of the same problems raised by one exist in the other as well).

In looking at the expression problem, it isn't clear to me that it can be solved in Coq or any other total strongly-typed programming language without some special ingredient. It seems that all of the solutions make use of back-doors in the type system. I'm very curious if anyone knows of a solution.

You might be right. OCaml's solution with polymorphic variants requires a form of unrestricted recursion. I wouldn't argue for full totality, particularly with regards to recursion, but I've come to strong believe that totality minus recursion at the library level is a must.

Signal being one of those words (along with "process" and "message") which can mean widely different things depending on which computer science context you are in. I'm assuming that you don't mean the OS-generated asynchronous notification mechanism found in Unix and similar operating systems; nor signals-as-events as found in frameworks like Qt.

In fact, if you'll pardon my ignorance :), I'm not entirely sure what you mean. :)

I think efficient exceptions leads to overuse of exceptions. We should instead strive for better interfaces which ideally wouldn't throw *any* exceptions. For instance, instead of throwing null pointer exceptions, just eliminate the possibility of null pointers entirely!

Inefficient exceptions or returning errors (as a sum+pattern matching) encourages total interfaces which inevitably improves software reliability.

...and many (including me) feel that unavoidable-null is a big problem.

On the other hand, NULL is a cheap hacky way of implementing the Maybe monad WRT pointer/reference types. It has the advantage that null-trapping is frequently free at runtime, at least until you try and dereference one. It has the disadvantage that the languages with null pointers make it hard to avoid--and frequently use nulls for things other than to indicate failure (such as null=default, null=no change; see also this c2 page for a list of ways that nulls are (ab)used).

It is possible (though it requires a lot of typing) to do bottom-propogation with NULLs. (I.e. write functions from pointers to pointers that return NULL when passed NULL).

That said--there is much to be said for writing routines which cannot return failure.

Ada 2005:

function Lookup (T : Table) return not null Ref_Element;

Safer and more efficient.