由于F#使用类型推理，而类型推理使用类型规则，因此F#类型规则表示为找到的推理规则。我怀疑它们不易发布，不易定位，甚至不可作为推理规则使用，这就是我为什么要问的原因。
在谷歌上搜索F# type rules不会返回任何相关信息。
搜索F#规范在section 14 - Inference Procedures中给出了解释，但没有给出实际的规则。
我知道我可以通过阅读F#源代码（Microsoft.FSharp.Compiler.ConstraintSolver）来提取它们，但提取和验证可能需要时间。此外，虽然我精通Prolog，它为我理解约束求解器提供了一些帮助，但我仍有一条学习曲线可以阅读。
您是正确的，F#类型推理和类型检查的正式规范将使用推理规则的格式编写。
问题是，对于这种形式化的规范来说，任何现实的编程语言都太复杂了。如果你想捕捉F#类型推理的全部复杂性，那么你只需要使用数学符号来编写与F#编译器源代码基本相同的东西。
因此，编程语言理论家通常为整个系统的一些有趣的子集编写类型和推理规则，以说明与某些新方面相关的问题。
-
F#类型系统的核心部分是基于标准ML语言的。您可以在标准ML的定义（PDF）中找到正式指定的ML的合理子集。这解释了一些有趣的事情，比如"值限制"规则。
-
我做了一些关于F#数据库工作方式的形式化工作，其中包括一个简单的类型检查位模型，您可以在F#Data论文中找到。
-
F#Computation Zoo论文（PDF）定义了F#计算表达式如何工作的键入规则。这实际上捕获了典型的用例，而不是编译器所做的。
总之，我认为在类型规则方面期望F#类型推理的形式化规范是不可行的，但我认为任何其他语言都没有。语言的形式模型更多地用于探索小子集的微妙之处，而不是用于谈论整个语言。