F# 键入规则作为推理规则

Question

由于 F# 使用 type inferencing 而类型推断使用 type rules，因此在哪里可以找到表示为 inference rules 的 F# 类型规则。我怀疑它们没有发布、容易定位，甚至不能作为推理规则使用，这就是我要问的原因。

谷歌搜索 F# type rules 没有返回任何相关内容。

搜索F# spec 给出section 14 - Inference Procedures 的解释，但没有给出实际规则。

我知道我可以通过阅读 F# 源代码 (Microsoft.FSharp.Compiler.ConstraintSolver) 来提取它们，但这可能需要一些时间来提取和验证。此外，虽然我精通 Prolog，它在理解约束求解器方面为我提供了一些帮助，但我仍然需要学习它来阅读它。

Answer 1

您是正确的，因为 F# 类型推断和类型检查的正式规范将使用推断规则的格式编写。

问题在于，任何现实的编程语言对于这种正式的规范来说都太复杂了。如果您想捕捉 F# 类型推断的全部复杂性，那么您只需使用数学符号来编写与 F# 编译器源代码中的内容基本相同的内容。

因此，编程语言理论家通常会为整个系统的一些有趣子集编写类型和推理规则 - 以说明与某些新方面相关的问题。

• F# 类型系统的核心部分基于标准 ML 语言。您可以在The Definition of Standard ML (PDF) 中找到正式指定的 ML 的一个合理子集。这解释了一些有趣的事情，比如“价值限制”规则。

• 我在正式确定 F# 数据库的工作方式方面做了一些工作，其中包括对提供的类型进行类型检查的简单模型，您可以在 F# Data paper 中找到该模型。

• F# Computation Zoo paper (PDF) 定义了 F# 计算表达式如何工作的类型规则。这实际上捕获了典型的用例，而不是编译器的作用。

总之，我认为在类型规则方面期望 F# 类型推断的正式规范是不可行的，但我认为其他任何语言都没有。语言的正式模型更多地用于探索小子集的微妙之处，而不是讨论整个语言。