I keep having these surprising experiences where I’ll implement something fairly complicated in OCaml and it works correctly as soon as I fix the type errors. This is a fairly pleasing thing (and makes me feel like adopting OCaml for my work was a smart move), but I’m curious as to whether other people have this experience relatively routinely.
(I’m inspired to write this because I implemented a relatively tricky data structure yesterday and discovered after I’d assembled a randomized property test for it that I couldn’t find any bugs. This isn’t the first time that this has happened, but I find it notable that it seems to happen for me a lot more often when I work in OCaml.)
Several months ago I was working on a codebase that generates an OCaml library from a JSON spec. One feature of the library was that it allowed one to download files. Unfortunately, the abstraction was insufficient and the functions generated would download the entire file into memory as a string. This limitation made it easy to OOM the process whenever downloading large files. Instead, the spec allowed the download to occur asynchronously, so I set off to make the function return an Async pipe instead of a string.
This simple little change was neither simple nor little when I eventually realized that most of the library would have to be rewritten in a monadic style. After fighting the compiler for several days and rewriting a couple thousand lines of code, the code finally compiled. You should have seen the bewilderment on my face when it just worked exactly as expected on the first try.
I find it amazing how a good abstraction can essentially make certain code changes entirely mechanical (in this case I’m referring to the monadic interface for Async’s deferreds)
Truth be told, I do that a lot. I really do not like running code (because that requires me to test, either manually or write these pesky unit tests), so if I can write my code in a mostly reasonable way (without going overboard) where the compiler can just refuse to compile if I messed up I much prefer that.
And I do have the experience @perry mentions quite often. This is not to say I’m a good programmer by any means, it’s that apparently the amount of types is decent to make enough invalid states unrepresentable to yield apparently correct programs.
Happens all the time for me. In my personal projects that are all written in OCaml, the errors I have to chase are usually failures on my part to choose the correct algorithm or to implement it efficiently. In my projects at work in C++, the errors I frequently chase more often than not turn out to be null pointer dereferences caused by object lifetime problems.
That’s the main reason I like strongly typed languages. (For suitably strong definitions of “strongly typed”.) You can start with the types, go on to implementation, and by the time the type checker gives you the thumbs up, you’ve often written what you intended to write.
It’s a bit less surprising if you view it through the Curry-Howard isomorphism: You write a theorem. You then work on writing a proof of that theorem. By the time the proof checker accepts the proof as valid, it is often correct.
Perhaps the fact that we find that last part surprising actually says less about OCaml than it does about other languages we have to work with…
Vaguely relevant Knuth quote:
Beware of bugs in the above code; I have only proved it correct, not tried it.
I would add that it’s a combination of strong types and functional paradigms. With functions, you have inputs and an output, each of which can be typechecked, and so each unit does its little bit of computation while maintaining local connectivity ie. the dataflow graph has few edges, all of which can be typechecked. Adding imperative constructs increases the graph’s connectivity, often connecting disparate locations, while disconnecting the local connections where type checking is most useful (since imperative statements return unit).
Coming from a dynamically typed language, I have to stop myself from shouting with joy every time I do a destructive refactoring and everything just works after the type errors are fixed. This is how programming should be!
I miss one thing though - how do you use the REPL for debugging and exploration if the data needed is big and complex. I’m dealing with a scene graph and my functions manipulate them over multiple passes. Sometimes things don’t work as expected, and I have to isolate the nodes manually, feed them into the entire pipeline, and put log statements everywhere. This is not specific to Typed FP, but I was wondering if you have any ideas on ways to deal with this problem in OCaml. Tests are one, but ideally I want to be able to run just a single function in the REPL with just the data it needs.
I tend to use utop and dune utop ./path/to/lib/sources to do this kind of debugging. You still need a lot of prints and you cannot always do it but it often helps.
Have you tried using qcheck to write generators for your data structures?
edit to clarify my tone: I meant this question in the friendly, inquisitive sense of “Have you tried this approach out and found it useful and/or problematic?” I definitely did not intend the aggressive, unfriendly sense of “Why didn’t you just do x already?” Rereading, it struck me that this wasn’t entirely clear.
