为什么OCaml类型转换函数的命名形式是"A_of_B"?

Why is the OCaml type conversion function named in the form "A_of_B"?

像"A_of_B"这样的名字是OCaml中独特的命名约定,但我想知道为什么。这是法语和英语使用语言不同的结果吗?还是 Xavier Leroy 的个人喜好?

背景:我发现OCaml的类型转换函数的名称类似于A_of_B,例如Stdlib模块中的int_of_string : string -> intfloat_of_int : int -> float。其他流行的语言使用类似 AtoB 的名称,例如 C 中的 itoa 函数。

我的猜测是,当使用函数作为值时,它的目的是提高可读性,例如具有高阶函数,如函数组合:

# let compose f g = fun x -> f (g x);;
val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b = <fun>

在这里,组合直接反映在名称中:

# let string_of_float = compose string_of_int int_of_float;;
val string_of_float : float -> string = <fun>

虽然用相反顺序的函数名来阅读等价物可能有点困难:

compose int_to_string float_to_int

首先,让我们先简单介绍一下 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。下面是一段代码,从原始的 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;;

它像什么东西吗? ;) 稍晚一点,法国的 Formel 团队基于 Categorical Abstract Machine 开发了 ML 的新实现,后来变成了 SML,而 Caml 本身也诞生了 10 年晚于 1987 年的代码片段。三年后,即 1990 年,Xavier Leroy 基于称为 ZINC 的字节码解释器设计了 Caml 的全新实现。五年后,他们开发了一个优化编译器,又过了五年,在 2000 年,Objective Caml 诞生了,又名 O'Caml,现在是 OCaml。

这就是说,ML 最初是由英语社区设计和开发的,没有理由在法语或 Xavier 的偏好中搜索约定词源。事实上,我们可以在 LCF(例如 intoftoktokofint 运算符)和 LCF 的其他衍生产品(例如 HOL)中找到此约定,例如,HOL 1988 标准库已经具有函数 int_of_string,那时候Xavier还没毕业

那么,为什么要这样约定呢?它来自对程序的推理方式,这是逻辑而非命令式的(请记住,ML 是作为定理证明器中的元语言(逻辑语言)诞生的)。我们不是在考虑如何一个功能是如何实现的,而是在考虑这个词代表什么,那么int_of_string "42"是什么?它是一个整数,文本表示为“42”。我们不会“42”转换为整数并将其视为一个转换框,相反,我们使用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——一种思考程序和理解它们的强大方式语义。