什么是公理 K？
What is Axiom K?
我注意到自 HoTT 以来，关于 "Axiom K" 的讨论出现得更频繁了。我相信这与模式匹配有关。我很惊讶在 TAPL、ATTAPL 或 PFPL 中找不到参考。
- 什么是公理 K？
- 是否像在 SML 中那样用于 ML 样式的模式匹配（或仅依赖模式匹配）？
- Axiom K 的适当参考是什么？
公理K又称为身份证明唯一性原理，是关于身份类型性质的公理在 Martin-Löf 的依赖类型理论中。这种类型在 System F 等更简单的类型理论中不存在（实际上无法定义），因此这可能是您在提到的书中没有遇到它的原因。
身份类型写成Id(A,x,y)或x = y并编码属性即x和y相等（在Curry-Howard correspondence).有一种基本的方法可以给出身份类型的证明，那就是refl : Id(A,x,x)，即证明x等于它自己。
在他的 thesis, Thomas Streicher introduced a new eliminator for the identity type which he called K (as the next letter in the alphabet after J, the standard eliminator for the identity type). It states that any proof p of an equality of the form x = x is itself equal to the trivial proof refl. From this, it follows that any two proofs p and q of any equation x = y are equal, hence the alternative name "uniqueness of identity proofs". What's remarkable is that he proved that this does not follow from the standard rules of type theory. I recommend reading Dan Licata's article on the homotopy type theory blog 中调查身份类型时，如果您想了解为什么不，他解释得比我好得多。
回答问题的第二部分：ML 样式的模式匹配与 K 无关，因为 ML 没有身份类型，因此甚至无法制定 K 公理。另一方面，依赖模式匹配需要 K，正如 Thierry Coquand 在 "Pattern matching with dependent types (1992)" 中介绍的那样。这样做的原因是在身份类型refl的构造函数上通过模式匹配非常容易证明K：
K : (p : x = x) -> p = refl
K refl = refl
事实上，Conor McBride 在他的论文 ("Dependently typed functional programs and their proofs (2000)") 中表明，K 是 唯一 依赖模式匹配真正添加到依赖类型理论的东西。
我自己对这个主题的兴趣是理解为什么依赖模式匹配需要 K 以及如何限制它以使其不再需要。结果是 paper 和 Agda 中 --without-K 选项的新实现。基本思想是依赖模式匹配时用于案例分析的统一算法不应该删除x = x形式的方程，因为这样做需要K。如果你想的话，我建议你阅读（介绍）论文了解更多。
我注意到自 HoTT 以来，关于 "Axiom K" 的讨论出现得更频繁了。我相信这与模式匹配有关。我很惊讶在 TAPL、ATTAPL 或 PFPL 中找不到参考。
- 什么是公理 K？
- 是否像在 SML 中那样用于 ML 样式的模式匹配（或仅依赖模式匹配）？
- Axiom K 的适当参考是什么？
公理K又称为身份证明唯一性原理，是关于身份类型性质的公理在 Martin-Löf 的依赖类型理论中。这种类型在 System F 等更简单的类型理论中不存在（实际上无法定义），因此这可能是您在提到的书中没有遇到它的原因。
身份类型写成Id(A,x,y)或x = y并编码属性即x和y相等（在Curry-Howard correspondence).有一种基本的方法可以给出身份类型的证明，那就是refl : Id(A,x,x)，即证明x等于它自己。
在他的 thesis, Thomas Streicher introduced a new eliminator for the identity type which he called K (as the next letter in the alphabet after J, the standard eliminator for the identity type). It states that any proof p of an equality of the form x = x is itself equal to the trivial proof refl. From this, it follows that any two proofs p and q of any equation x = y are equal, hence the alternative name "uniqueness of identity proofs". What's remarkable is that he proved that this does not follow from the standard rules of type theory. I recommend reading Dan Licata's article on the homotopy type theory blog 中调查身份类型时，如果您想了解为什么不，他解释得比我好得多。
回答问题的第二部分：ML 样式的模式匹配与 K 无关，因为 ML 没有身份类型，因此甚至无法制定 K 公理。另一方面，依赖模式匹配需要 K，正如 Thierry Coquand 在 "Pattern matching with dependent types (1992)" 中介绍的那样。这样做的原因是在身份类型refl的构造函数上通过模式匹配非常容易证明K：
K : (p : x = x) -> p = refl
K refl = refl
事实上，Conor McBride 在他的论文 ("Dependently typed functional programs and their proofs (2000)") 中表明，K 是 唯一 依赖模式匹配真正添加到依赖类型理论的东西。
我自己对这个主题的兴趣是理解为什么依赖模式匹配需要 K 以及如何限制它以使其不再需要。结果是 paper 和 Agda 中 --without-K 选项的新实现。基本思想是依赖模式匹配时用于案例分析的统一算法不应该删除x = x形式的方程，因为这样做需要K。如果你想的话，我建议你阅读（介绍）论文了解更多。