The name like "A_of_B" is a unique naming convention in OCaml, but I want to know why. Is it a result of the different language usage between French and English? Or Xavier Leroy's personal preference?
Background: I found that OCaml's type conversion functions have the name like A_of_B
, for example, int_of_string : string -> int
or float_of_int : int -> float
in Stdlib module. Other popular languages use the name like AtoB
, for example, itoa
function in C.
First of all, let's start with a short excursus to the history of OCaml. Xavier Leroy didn't invent the language and neither the language was born in France. OCaml was born from the Meta Language (ML) of the LCF (Logic for Computable Functions) theorem prover, developed in Stanford and University of Edinburgh by Robin Milner. Below is a snippet of code, obtained from the original LCF 1977,
let gensrinfo th =
let srthm = disjsrvars th in
let hypfrees = formlfrees(hyp srthm)
and hyptyvars = formltyvars(hyp srthm)
and (),p,() = destimpequiv(concl srthm) in
srthm , termmatch(hypfrees,hyptyvars) p;;
Does it resemble something? ;) It was a little bit later when the French Formel team developed a new implementation of ML, based on the Categorical Abstract Machine, that later turned into SML, and Caml itself was born 10 years later than the code snippet above in 1987. And three years later, in 1990, Xavier Leroy designed a completely new implementation of Caml based on a bytecode interpreter called ZINC. Five years later, they developed an optimizing compiler, and five more years later, in 2000, Objective Caml was born, aka O'Caml and, now, OCaml.
This is all to say that, originally, ML was designed and developed by the English-speaking community and there is no justification to search for the convention etymology in the French language or Xavier's preferences. We, indeed, can find this convention already in LCF (e.g., intoftok
, tokofint
operators) and in other derivatives of LCF, such as HOL, e.g., the HOL 1988 standard library already had the function int_of_string, at that time Xavier didn't even graduate yet.
So, why this convention? It comes from the way of reasoning about programs, which is logical rather than imperative (remember, ML was born as a meta-language (the logic language) in a theorem prover). Instead of thinking about how a function is implemented, we are thinking about what the term represents, so what is int_of_string "42"
? It is an integer, that has textual representation "42". We do not convert "42" into an integer and think about it as a transformation box, instead, we employ declarative thinking as in mathematics, e.g., cos 0.0
doesn't convert 0.0
into 1.0
, cos 0.0
is 1.0
. This style of thinking facilitates equational reasoning -- a powerful way of thinking about programs and understanding their semantics.