为什么OCaml类型转换函数以“A_of_B”形式命名?

Jis*_*yun 0 ocaml naming

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

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

ivg*_*ivg 11

首先,让我们从OCaml 历史的简短介绍开始。Xavier Leroy 没有发明这门语言,而且这门语言也都不是在法国诞生的。OCaml 诞生于LCF(可计算函数逻辑)定理证明器的元语言 (ML),由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;;
Run Code Online (Sandbox Code Playgroud)

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

这就是说,最初,ML 是由英语社区设计和开发的,没有理由在法语或 Xavier 的偏好中搜索约定词源。我们,事实上,已经可以在LCF(例如,发现了这个惯例intoftoktokofint运营商)和LCF的其他衍生物,如HOL,例如,1988年HOL标准库中已有的功能int_of_string,当时泽维尔甚至没毕业然而。

那么,为什么会有这个约定呢?它来自对程序的推理方式,这是逻辑而非命令式(请记住,ML 是作为定理证明器中的元语言(逻辑语言)而诞生的)。而是想着如何的功能实现,我们正在考虑什么术语代表,所以是什么int_of_string "42"?它是一个整数,具有文本表示“42”。我们不会“42”转换为整数并将其视为一个转换框,而是使用数学中的声明式思维,例如,cos 0.0不转换0.01.0, cos 0.0 is 1.0。这种思维方式促进了等式推理 -- 一种思考程序和理解其语义的强大方式。


cor*_*ump 5

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

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

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

# let string_of_float = compose string_of_int int_of_float;;
val string_of_float : float -> string = <fun>
Run Code Online (Sandbox Code Playgroud)

而使用相反顺序的函数名称读取等效项可能有点困难:

compose int_to_string float_to_int
Run Code Online (Sandbox Code Playgroud)