Checked exceptions (like in Java) interact very poorly with higher order functions. For example, try using map with a function that can throw an exception in Java. This is a well-known open problem and an active area of research. The key word for this line of work is “effect system”, see for example Effect system - Wikipedia.
In brief, it’s hard to design a system that is reasonably type safe, compositional, and not a complete pain to use for the programmer. But people are working on it.
EDIT: And no, monads are not good enough in general.
What are you trying to demonstrate? Because the type system does not track exceptions, it can’t detect that End_of_file can’t be raised by Hashtbl.find and catching it here does not make much sense.
Of course, most of the time, I don’t care much about microefficiency, at least within reason. A small constant factor means little if a program is going to be run rarely and only for a few seconds. A small amount of the time, I do care about microefficiency, but generally that’s only for a small subset of programs, and after profiling running code, you can optimize it.
What you do care about almost all the time is how long it takes to get from idea to finished code, and for that, option or result is going to make your life easier.
BTW, weirdly, I used Coq a lot before I ever touched OCaml. There, you can get the ultimate in safety, which is proving theorems about your code, or actually using the type system to encode arbitrary properties so if a program is correctly typed, it is also perfectly correct. Unfortunately, Coq is not the most practical system for writing code day to day; as it stands, it’s best reserved for very high value systems. Someday, I want to use a programming system that lets me prove theorems about my code day to day while still retaining the practicality of a language like OCaml. Part of going in that direction, though, is trying to maintain many of the same programming techniques one would use in a system like Coq, and sticking to functional paradigms where possible is part of that. It is much easier to reason about functional code.
No, when I say efficiency I mean it, I don’t mean the development time, and I think it’s important. Is using option going to make your life easier? Not in my experience, you just write some catch blocks and then handle and throw again as appropriate, makes the code more readable.
I believe that it’s for very very very… high end systems.
In fact, it looks like a totally different world (like outer space standpoint vs. walking in the forest).
It’s worth playing just a little bit with Coq to get that feeling.
Our experience differs. Your opinion is noted, but I don’t agree with it, and I’m unlikely to in the future. My way, the compiler catches all mistakes.
Probably the prototype of a multi paradigm language that contain enough computational logic to do something interesting. It’d be really cool to move beyond type systems for writing real world code. It’d also significantly improve AGI algorithms, for sure. I had suggested implementing M-Search with Coq, that’s an algorithm that searches for the proof that yields the best solution for a problem (basically). Such magical automated programming will likely be common fodder by 2040, but how do we get from here to there. Anyhow, it’d really be very interesting if my OCaml code looked like ADATE problem specifications if you know what I mean. Then, I could not only implement mathematical types correctly, but also enforce all sorts of logical constraints and relations among my mathematical objects (that would go beyond type, module and object systems), including programs.
Code length is usually not what one is optimizing for. Correctness is what one cares about. If you want to minimize code length, use APL. That said, in a pattern matching language like OCaml, the version that uses exceptions and the version that uses option are usually nearly same length, only with one, the compiler checks your work.
Anyhow, it’d really be very interesting if my OCaml code looked like ADATE problem specifications if you know what I mean. Then, I could not only implement mathematical types correctly, but also enforce all sorts of logical constraints and relations among my mathematical objects (that would go beyond type, module and object systems), including programs.