Max*_*ber 1 ocaml compiler-errors static-typing
OCaml 两者都有不同的语法：
\n+.。3.。# 3 + 3;;\n- : int = 6\n# 3. +. 3.;;\n- : float = 6.\n# 3. + 3;;\nError: This expression has type float but an expression was expected of type\n int\n我可以看到使用其中一种机制来消除歧义，但为什么总是需要两个？ \n例如，我可以看到有时在文字末尾需要的情况，但不是为什么.OCaml可以弄清楚的地方需要它我们想要浮点运算，因为我们说我们想要浮点运算。3 +. 3
我正在寻找基于与其他语言功能交互的具体技术理由\xe2\x80\x93，而不是来自人体工程学的意见或论点。
\n简而言之，这是因为(+.)和(+)以及1和1.表示不同的值，尽管它们看起来很相似。这些值具有不同的类型、不同的表示形式和不同的语义。(+)一种语言在不同上下文中表现和工作相同的特性1称为临时多态性，OCaml 中不存在这种特性。OCaml 不会尝试根据程序的文本表示及其类型来推断您将使用哪个值，而是根据您正在使用的值以及您的使用方式来推断您的程序的类型。使用它们。这是 ML 与其他一些相反的语言的一个重要区别，即它们具有用户指定的类型，然后推断与该类型匹配的正确值并检查这些值是否正确使用。在机器学习中，输入是程序，输出是该程序的类型，（a）用于证明该程序类型良好并且在运行时不会出现任何类型错误，（b）用于证明生成本机和高性能代码，并删除所有推断类型。同样重要的是要理解，OCaml 中的类型推断并不是一种方便实用程序，可以让您在可以推断类型时省略类型（如 C++auto或 Scala 中的本地类型推断）。相反，它是编译过程和语言语义中的主要步骤，因为 OCaml 必须能够推断任何程序的类型。我们偶尔在 OCaml 程序中编写的类型仅用作约束，从不用作输入。此外，类型注释永远不会改变程序的行为。好吧，除非 GADT 发挥作用，但这是一个完全不同的故事。
为了更深入地了解，我们应该记住 OCaml 下的类型推断算法是语法驱动的和声明性的。语法驱动意味着程序语法完全定义了该程序的类型。此外，该算法确保如果该类型存在（即程序类型良好），则该推断类型是唯一且主要的。即，要么没有其他类型代表该程序，要么所有其他类型都是推断类型的实例。声明性意味着如何将类型分配给程序的规则是用声明性类型规则来描述的。该算法将程序正式转换为类型，从而实现/确保Curry-Howard对应，即计算机程序和数学证明之间的深层联系。这使我们能够谈论程序的正确性，反之亦然，谈论真理的正确性，即用程序证明我们的定理是正确的。这让我们回到了 OCaml/ML 的历史，它最初是LCF（可计算函数逻辑）定理证明器的元语言（ML）。
鉴于我们同意我们不想失去语言的重要属性，但问题仍然悬而未决，为什么我们不能实现语法驱动且可声明的临时多态性。嗯，事实上，我们可以，例如 Haskell 就有一个。还有一些向 OCaml 添加模块化隐式的工作。但这一切都伴随着权衡，最终它将成为一种完全不同的语言。到目前为止，在 OCaml 中，每个值都有一个类型或类型方案，并且 OCaml 运行时系统中没有类型可以表示+适用于整数和浮点数的运算符。
(+)话虽如此，如果你不说你可以定义自己的类型为 的运算符，那么对 OCaml 来说是不诚实的number -> number -> number，其中number是一个存在式，type number = Num : 'a typeid * 'a -> number每个操作都有一个单独的操作表，typeid存储在某个隐藏的哈希表中。但这将是动态类型（查看typeid每个值中如何打包），并且它与静态类型完全不同，静态类型可以在程序运行之前为您提供保证（在我们的示例中，该(+)函数可能会在运行时失败，并且我们的类型规则）不是声明性的，而是运算符的实现所固有的(+)）。