compiler-errors - 为什么OCaml具有强制性的独特的float和int文字语法？

Question

OCaml具有以下两种不同的语法:

浮点运算与int运算。浮点运算以点号+.结尾。

浮点文字与int文字。浮点字面量以点结尾:3.。

# 3 + 3;;
- : int = 6
# 3. +. 3.;;
- : float = 6.
# 3. + 3;;
Error: This expression has type float but an expression was expected of type
         int

我可以看到使用其中一种机制来消除歧义，但是为什么总是需要两种机制呢？
例如，我可以看到有时在文字的末尾需要.的情况，但是为什么Ocaml却想出我们想要浮点运算的原因，而3 +. 3却不需要为什么，因为我们是说我们想要浮点运算。
我正在寻找与其他语言功能互动的特定技术理由，而不是人机工程学的观点或论据。

Answer 1

简而言之，这是因为(+.)和(+)以及1和1.表示不同的值，尽管它们看起来相似。这些值具有不同的类型，不同的表示形式和不同的语义。使(+)和1在不同上下文中工作相同的语言的功能称为即席多态性，它在OCaml中不存在。 OCaml不会尝试从程序的文本表示形式及其类型中推断出要使用的值，而是根据所使用的值以及您的使用方式推断出程序的类型是什么使用它们。 ML是其他语言之间的重要区别，而其他语言则以相反的方式运行，即它们具有用户指定的类型，然后推断与该类型匹配的正确值并检查这些值是否正确使用。在ML中，输入是程序，输出是该程序的类型，(a)用于证明程序类型正确，并且在运行时不会出现任何类型错误，(b)用于生成本机代码和高性能代码，并删除所有推断的类型。同样重要的是要了解，OCaml中的类型推断不是一种方便实用的工具，它可以让您在可以推断类型时忽略它们(例如，在C++的auto中或在Scala中的本地类型推断)。相反，它是编译过程和语言语义的主要步骤，因为OCaml必须能够推断任何程序的类型。我们偶尔在OCaml程序中编写的类型仅用作约束，而绝不用作输入。而且，类型注释永远不会改变程序的行为。好吧，除非GADT发挥作用，但这是一个完全不同的故事。
为了更深入地了解，我们应该记得OCaml下面的类型推断算法是语法驱动的和声明性的。语法驱动意味着程序语法完全定义了该程序的类型。此外，该算法确保如果类型存在(即程序类型正确)，则此推断出的类型是唯一且具有主体性。也就是说，没有其他类型可以代表此程序，或者所有其他类型都是推断类型的实例。声明性意味着用declarative type rules描述如何将类型分配给程序的规则。该算法将程序正式转换为类型，从而启用/确保Curry-Howard对应关系，计算机程序与数学证明之间的深层联系。这使我们能够谈论程序的正确性以及反之的真理的正确性，即用程序证明我们的定理是正确的。这使我们回到了OCaml/ML的历史，OCaml/ML最初是LCF(可计算函数逻辑)定理证明者的元语言(ML)。
既然我们同意不希望失去该语言的重要属性，那么这个问题仍然悬而未决，为什么我们不能实现语法驱动且可声明的即席多态。好吧，事实上，我们可以，例如，Haskell有一个。还有一些将modular implicits添加到OCaml的工作。但是，所有这些都伴随着权衡，最终将是一种完全不同的语言。到目前为止，在OCaml中，每个值都有一个类型或类型方案，并且OCaml运行时系统中没有任何类型可以表示可用于int和float的+运算符。
话虽如此，对OCaml而言，不要不说您可以定义自己的(+)运算符，其类型为number -> number -> number，这是不诚实的，其中number是存在的type number = Num : 'a typeid * 'a -> number，其中每个typeid的操作表都存储在一些隐藏的哈希表中。但这是动态类型化(请参阅typeid如何包装在每个值中)，并且与静态类型化完全不同，它可以保证程序在运行之前(在我们的示例中，此(+)函数可能在运行时失败，类型规则不是声明性的，而是(+)运算符的实现所固有的。