微信公众号搜"智元新知"关注
微信扫一扫可直接关注哦!

为什么OCaml具有强制性的独特的float和int文字语法?

如何解决为什么OCaml具有强制性的独特的float和int文字语法?

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

我可以看到使用其中一种机制来消除歧义,但是为什么总是需要两个 ? 例如,我可以看到一种情况,在文字的末尾有时需要.,有时是 ,但是为什么在3 +. 3中,OCaml可能会认为需要浮点运算,因为我们要使用浮点运算。

我正在基于与其他语言功能的交互(而不是来自人体工程学的观点或论据)寻求具体的技术依据。

解决方法

简而言之,这是因为(+.)(+)以及11.表示不同的值,尽管它们看起来相似。这些值具有不同的类型,不同的表示形式和不同的语义。使(+)1在不同上下文中工作相同的语言的功能称为即席多态性,它在OCaml中不存在。 OCaml不会尝试从程序的文本表示形式及其类型中推断出要使用的值,而是根据所使用的值以及您的使用方式推断出程序的类型是什么使用它们。 ML是其他语言之间的重要区别,而其他语言则以相反的方式运行,即它们具有用户指定的类型,然后推断与该类型匹配的正确值并检查这些值是否正确使用。在ML中,输入是程序,输出是该程序的类型,(a)用于证明程序类型正确,并且在运行时不会出现任何类型错误,(b)用于生成本机代码和高性能代码,并删除所有推断的类型。同样重要的是要了解OCaml中的类型推断不是一种便利实用程序,它可以让您在可以推断类型时忽略它们(例如在C ++的auto中或在Scala中进行局部类型推断)。相反,它是编译过程和语言语义的主要步骤,因为OCaml必须能够推断任何程序的类型。我们偶尔在OCaml程序中编写的类型仅用作约束,而绝不用作输入。而且,类型注释永远不会改变程序的行为。好吧,除非GADT发挥作用,但这是一个完全不同的故事。

为了更深入地了解,我们应该记得OCaml下的类型推断算法是语法驱动的声明性的。语法驱动意味着程序语法完全定义了该程序的类型。此外,该算法确保如果类型存在(即程序类型正确),则此推断出的类型是唯一且具有主体性。也就是说,没有其他类型可以代表此程序,或者所有其他类型都是推断类型的实例。声明性意味着用declarative type rules描述如何将类型分配给程序的规则。该算法将程序正式转换为类型,从而启用/确保Curry-Howard对应关系,计算机程序与数学证明之间的深层联系。这使我们能够谈论程序的正确性以及反之的真理的正确性,即用程序证明我们的定理是正确的。这使我们回到了OCaml / ML的历史,它最初是LCF(可计算函数逻辑)定理证明者的元语言(ML)。

鉴于我们同意我们不想失去该语言的重要属性,这个问题仍然悬而未决,为什么我们不能实现语法驱动且可声明的即席多态性。好吧,事实上,我们可以,例如,Haskell有一个。还有一些将modular implicits添加到OCaml的工作。但是,所有这些都伴随着权衡,最终将是一种完全不同的语言。到目前为止,在OCaml中,每个值都有一个类型或类型方案,并且OCaml运行时系统中没有任何类型可以表示+运算符,该运算符可用于整数和浮点数。

话虽如此,不要说您可以定义类型为(+)的{​​{1}}运算符(其中number -> number -> number是存在的{{ 1}},并为存储在某个隐藏哈希表中的每个number提供单独的操作表。但这将是动态类型的(请参见type number = Num : 'a typeid * 'a -> number在每个值中的包装方式),它与静态类型完全不同,它为您的程序在运行之前提供了保证(在我们的示例中,此{{1} }函数可能会在运行时失败,并且我们的键入规则不是声明性的,而是typeid运算符的实现所固有的。)

,

每个函数都有一个类型,这就是导致OCaml语法的原因。如果您传递了不合适的参数,则编译器会因错误而拒绝您的代码。

这似乎很明显,但是在包括基本数学运算符在内的任何函数中也是如此:名为+.的函数具有类型:

val (+.): float -> float -> float

仅此而已。如果您使用int而不是float,则编译器会告诉您您的代码是错误的。 OCaml没有任何显示。编译器仅检查参数是否与功能签名一起有效。不是吗错误。

您可能会指出这一点是错误的,因为任何C编译器都将接受您的代码行并按预期结果产生浮点数。但这是另一种语言,即使此可以¹起作用,OCaml内也不允许这样做。您无法转义该类型。

language specification很清楚:每个函数都是由参数的类型定义的,并且您不能提供多类型的参数。

这使编译器可以轻松地优化代码,但是您必须将参数明确转换为函数签名所期望的参数。

¹实际上不会,因为OCaml中int的内存表示形式与C语言中的int并不完全相同(但这是另一个子喷射器)

版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。