What is The OCaml Way?

A little bit of context. Ruby on Rails has so-called “The Rails Way”, which includes such principles: RESTful, CRUD, DRY, KISS, MVC, etc. Ruby has its own philosophy, which is harder to explain, but which includes “somebody have already developed a gem for that”, BDD, objects overuse, development of eDSLs. Both were majorly formed by agile and startup cultures, where, as I feel it, delivery speed is much more important than software correctness and performance.

Does OCaml/OCaml community has “The OCaml Way”? What the values and beliefs OCaml developers put into approaches, designs, patterns, workflows, toolchains and the language itself or what is “OCaml (solutions) engineering school” could be?

1 Like

I don’t think ocaml is organized to have a cross-language motto or cohesive culture. IMO, the Ocaml is “go your own way” (we have multiple concurrency frameworks, many standard libraries, multiple ide integrations, lots of different ways to accomplish the same thing).

2 Likes

I’m a bit doubtful about that kind of tribalism. They tend to increase each ones blind spots and emprison people in systems of beliefs rather than nurture curiosity.

Except for language idioms which do in practice have an expressive impact, I seems to me that sound engineering practices largely ignore language barriers.

13 Likes

I think that one big idea that idiomatic OCaml programs use is “make illegal states unrepresentable,” a quote which I believe comes from OCamler Yaron Minsky. It means that OCaml programs should leverage the type system to make programs correct by construction, avoiding runtime checks when the programmer knows that the program cannot enter a certain state.

For example, say that a Foo is either a Bar, which has a name and an age, or a Baz, which only has an age. The “bad” way to express this, which might be done in languages without the strengths of OCaml’s type system, is

type foo = {
  typ : string; (* typ is either "bar" or "baz" *)
  name : string; (* should be "" if typ is "baz" *)
  age : int;
}

The right way to do this is:

type bar = {
  bar_name : string;
  bar_age : int;
}

type baz = {
  baz_age : int;
}

type foo = Bar of bar | Baz of baz

This idea can be taken further with GADTs, e.g. the post here about the well-typed parser ("Parsing" terms into a well-typed representation: a GADT puzzle).

6 Likes

Well-put. I would add that this is the “ML way”, and is shared with all the ML-family languages (including Haskell).

I kind of feel that the FP koans do exemplify some sort of “ML way”. And that there is something to the “value-oriented programming” approach. This consists in trying to maximize the prevalence of referentially-transparent positions in program texts, and trying to map as much as possible of computation to inductions on well-founded orders.

Oof. That was really abstruse wiith a bunch of long words. What I mean is

  1. as much as possible, try to make your programs have a lot of spots where you can reason locally about equality of expressions. So you can insert debug-wrappers ad libitum, for instance.

  2. Don’t use while-loops, but rather for-loops, with possibly interesting data-structure they iterate over. So iteration is bounded, and you explicitly represent the stuff carried from one iteration to the next.

Induction, not iteration.

And I think that Rust shares a lot of this. Probably inherited from ML, via people like Graydon Hoare.

3 Likes

I understand what you are saying. Instead of making a loop comparison, the “OCaml way,” at least for me, is to use tail-recursive functions. They are as equally powerful as loops theoretically (see SSA is Functional Programming — Princeton University). Mutation of local variables is actually unnecessary and a compiler tends to transform mutations into multiple immutable temporaries in SSA form, which could even be given different stack offsets! My personal view is that since mutation of loop variables can be achieved by passing accumulators in a pure way, the latter should be preferred due to easier reasoning, and I think that is one aspect of the “OCaml way.”

I think that the structured induction over interesting data structures that you mention are greatly helped by writing recursive functions, which match over the inductive structure of the data (while a for loop tends to match over the inductive structure of a natural number). This also highlights the strength of OCaml’s type system! (Make illegal states unrepresentable)

There is a particular paper that for me has always exemplified this “induction, induction, induction” approach to computation that characterizes “thinking in ML”. It is The Constructive Engine by Huet. The problem is, it’s hard to find. But what he does there, is show you how to take lambda-terms a la deBruijn, and come up with useful induction principles that let you do all the various kinds of computation you want, in comprehensible ways.

I’m not doing a good job of explaining it, but … when you’re inducting on a deBruijn lambda-term, you have an environment mapping indices to some sort of value, and what you’re really inducting on is some equivalence class of values, not on a particular value. It’s been … 30 years since I read the paper, but really understanding it well was crucial to my development as an FP programmer. Really, really crucial.

I cannot recommend that paper, and working thru it with keyboard-at-the-ready, enough.

2 Likes

I think another aspect of the “OCaml Way” is pragmatic imperative programming. Some algorithms can only be expressed efficiently with in-place updates, and OCaml doesn’t stop you from implementing these algorithms. Mutable local variables and jumps are as equally powerful as functional programming with tail recursion and accumulator passing style, as seen with the SSA transformation, but where imperative programming is more powerful than functional programming is that imperative programming allows you to update an arbitrarily deep data structure in-place given a reference to the memory cell. The union-find data structure and associated algorithms, crucial for implementing Hindley-Milner type inference, is one such example where mutable memory cells are necessary for efficiency. OCaml shines because it is both functional and imperative.

3 Likes

Or as the koan has it ( Functional Programming Koans, in OCaml by Doug Bagley — Translated by humans ):

The Koan of Side Effects

A student of FP came to Daniel de Rauglaudre and asked how to achieve FP Nature. Daniel replied, “to achieve FP Nature, you must learn to program without side effects and other imperative features”. So the student went away to learn how to program in this style. He studied very hard so he could rid his programs of references and for-loops. He struggled to only use let bindings and let rec loops. One day, in order to find inspiration, he was studying the code of the Masters, and in reading the source of Camlp4, he saw a number of uses of references and for-loops! He rushed back to Daniel de Rauglaudre and exclaimed, “How can you tell me not to use imperative features when you use them yourself!” Daniel measured the student carefully in his gaze and replied, “But I already know how to program without side-effects.” At that moment the student was enlightened.

:rofl:

5 Likes