请给出Hack语言类型系统的精确描述。它在网上似乎不存在——我只能在文档中找到一些例子——所以请在你的回答中详细描述它。
例如，我想知道在Hack中是如何定义子类型的，以及在各种Hack类型检查/静态分析模式(strict, special, decl)中使用了什么赋值兼容性的概念。
如果你想要一个Hack的正式语言规范，现在还没有，尽管我们认为最终会有一个。如果你想要关于语言的推理规则和形式证明，那么，我们更多地关注于创造一种实用的语言，而不是坐下来花时间证明它听起来是正确的。:)(也就是说，100%严格的代码应该是合理的，即没有运行时类型错误，如果不是，那就是一个bug;我们只是永远不会坐下来正式证明这一点。
所以，你链接到的文档是最好的，除非你想开始挖掘typechecker源代码。为此，您可能首先对统一代码、子类型关系和一般类型检查的细节感兴趣。(还有很多很多，但如果你是那种想要挖掘我们如何实现统一的细节的人，我相信你可以自己找到剩下的:))
如果你有关于实现的具体问题，如果他们在主题上，请随时在SO上用"hacklang"标签提问，总的来说，我很乐意在美国太平洋时间的工作时间在Freenode上的#hhvm中聊天。