如果您尽力实现一个功能，就可以说服自己这是不可能的。如果您不相信，可以将论点变得更正式：我们详尽地列举了程序，发现不可能。事实证明，只有六个有意义的案例需要考虑。

我不知道为什么不经常提出这种说法。

完全不正确的摘要：

• 第一幕：证明搜索很容易。
• 第二幕：依赖类型也是如此。
• 第三幕：Haskell仍然适合编写依赖类型的程序。

一，证明搜索游戏

首先，我们定义搜索空间。

我们可以将任何Haskell定义简化为以下形式之一

lem = (exp)

为了一些表达(exp)。现在我们只需要找到一个表达式。

查看在Haskell中进行表达式的所有可能方法：https : //www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-220003（这并不涉及扩展，请读者练习）。

它可以将页面放在单个列中，因此开始时并没有那么大。而且，它们大多数是用于某种形式的功能应用或模式匹配的糖。我们还可以通过字典传递来对类型类进行除糖处理，因此剩下的是可笑的小lambda演算：

• lambdas， \x -> ...
• 模式匹配， case ... of ...
• 功能应用， f x
• 构造函数C（包括整数文字）
• 常量，c（对于无法根据上述结构编写的基元，因此各种内建（seq）以及FFI（如果有的话））
• 变量（受lambda和case约束）

我们可以排除，每隔一定的理由，我认为真正的问题是关于纯演算（或读者可以枚举常量，排除黑魔术常量一样undefined，unsafeCoerce，unsafePerformIO使一切都崩溃（任何类型的居住，对于某些其中，类型系统是不完善的），并留有白色魔术常数，可以通过资金雄厚的论文将当前的理论论点概括为该常数。

我们还可以合理地假设我们想要一个不涉及递归的解决方案（以消除噪声，例如lem = lem和，fix如果您觉得自己以前无法使用它），并且实际上具有正常形式，或者最好是规范形式关于βη-等价形式。换句话说，我们按以下方法改进和检查了可能的解决方案集。

• lem :: _ -> _具有函数类型，因此我们可以假设WLOG其定义以lambda开头：

  -- Any solution
  lem = (exp)
  
  -- is η-equivalent to a lambda
  lem = \refutation -> (exp) refutation
  
  -- so let's assume we do have a lambda
  lem = \refutation -> _hole
  

现在枚举lambda。

• 它可能是一个构造函数，然后必须是Refl，但是没有证据表明Choose x y ~ 2在上下文中（这里我们可以形式化和枚举typechecker知道并可以派生的类型相等性，或者进行强制语法（相等性证明）并继续与他们一起玩这个证明搜索游戏），因此不会输入check：

  lem = \refutation -> Refl
  

  也许有某种方式构造该等式证明，但随后该表达式将从其他内容开始，这将是证明的另一种情况。

• 可能是某个构造函数的应用程序C x1 x2 ...，或者是该变量refutation（是否应用）；但是没有一种可能的类型正确，它必须以某种方式产生一个(:~:)，Refl这实际上是唯一的方法。

• 或者可能是一个case。WLOG，case在左边没有嵌套，也没有任何构造函数，因为在两种情况下都可以简化表达式：

  -- Any left-nested case expression
  case (case (e) of { C x1 x2 -> (f) }) { D y1 y2 -> (g) }
  
  -- is equivalent to a right-nested case
  case (e) of { C x1 x2 -> case (f) of { D y1 y2 -> (g) } }
  
  
  
  -- Any case expression with a nested constructor
  case (C u v) of { C x1 x2 -> f x1 x2 }
  
  -- reduces to
  f u v
  

  因此，最后一个子案例是可变案例：

  lem = \refutation -> case refutation (_hole :: x :~: y) of {}
  

  并且我们必须构建一个x :~: y。我们列举了_hole再次填充的方法。是Refl，但没有可用的证据，或者是（跳过某些步骤）case refutation (_anotherHole :: x :~: y) of {}，并且手上有无限的下降，这也是荒谬的。这里一个不同的可能论点是，我们可以case从应用程序中取出，以将这种情况从考虑的WLOG中删除。

  -- Any application to a case
  f (case e of C x1 x2 -> g x1 x2)
  
  -- is equivalent to a case with the application inside
  case e of C x1 x2 -> f (g x1 x2)
  

没有更多的情况了。搜索已完成，我们没有找到实现(x :~: y -> Void) -> Choose x y :~: 2。QED。

要阅读有关此主题的更多信息，我想一本有关lambda演算的课程/书，直到简单类型的lambda演算的归一化证明应为您提供入门的基本工具。以下论文在第一部分中对此主题进行了介绍，但我承认我对此类材料的难易程度判断不佳：哪些类型的居民独特？Gabriel Scherer着重于纯程序等效。

随意提出更多充足的资源和文献资料。

二。修正命题并用依赖类型证明

您最初的直觉认为这应该编码一个有效的命题，这绝对是正确的。我们如何解决它以使其可证明？

从技术上讲，我们要查看的类型可以通过以下方式量化forall：

forall x y. (x :~: y -> Void) -> Choose x y :~: 2

的重要特征forall是它是不相关的量词。它引入的变量不能在这种类型的术语中“直接”使用。尽管在依赖类型的存在下，这一方面变得更加突出，但它仍然在Haskell至今仍然存在，这为Haskell中的这一点（以及许多其他示例）为何不可“证明”提供了另一种直觉：如果您思考为什么认为该命题是有效的，您自然会从关于是否x等于的案例拆分开始y，但即使要进行案例拆分，您也需要一种方法来确定您所处的一方，当然必须考虑x和y，所以它们不能不相关的。forall 在Haskell中，一点也不像大多数人所说的“为所有人”所指。

关于相关性的一些讨论可以在Richard Eisenberg的论文《Haskell的依存类型》中找到（特别是第3.1.1.5节是一个示例，第4.3节是从属Haskell的相关性，第8.7节是与其他语言的对比）。依赖类型）。

依赖的Haskell将需要一个相关的量词来补充forall，这将使我们更接近证明这一点：

foreach x y. (x :~: y -> Void) -> Choose x y :~: 2

然后我们可能会这样写：

lem :: foreach x y. (x :~: y -> Void) -> Choose x y :~: 2
lem x y p = case x ==? u of
  Left r -> absurd (p r)  -- x ~ y, that's absurd!
  Right Irrefl -> Refl    -- x /~ y, so Choose x y = 2

这还假定了不等式的第一概念/~，即补充~，以帮助Choose减少在上下文中的不平等和决策功能(==?) :: foreach x y. Either (x :~: y) (x :/~: y)。实际上，这种机器不是必需的，只是可以简化答案。

在这一点上，我正在编造东西，因为尚不存在从属Haskell，但这在相关的从属类型语言（Coq，Agda，Idris，Lean）中很容易实现，对类型族进行了适当的替换Choose（类型族在有些功能太强大而无法翻译为单纯的功能，因此可能会作弊，但我离题了。

这是Coq中的一个可比较程序，它还显示了lem适用于1和2的程序，并且适当的证明确实会因的反射率而减少为证明choose 1 2 = 2。

https://gist.github.com/Lysxia/5a9b6996a3aae741688e7bf83903887b

三，没有依赖类型

困难的一个关键来源是Choose实例重叠的封闭型族。这是有问题的，因为在Haskell中没有适当的方式来表达x和y不相等这一事实，要知道第一个子句Choose x x不适用。

如果您喜欢伪依赖的Haskell，更有效的方法是使用布尔类型相等：

-- In the base library
import Data.Type.Bool (If)
import Data.Type.Equality (type (==))

type Choose x y = If (x == y) 1 2

等式约束的替代编码对于此样式很有用：

type x ~~ y = ((x == y) ~ 'True)
type x /~ y = ((x == y) ~ 'False)

这样，我们就可以得到上述类型命题的另一个版本，可以在当前的Haskell中表达（其中SBool的单例类型Bool），从本质上可以理解为添加了x和等于相等的假设y。这与先前关于“无关紧要”的主张并不矛盾forall，该函数正在检查布尔值（或更确切地说是SBool），该布尔值将检查x和延迟y给调用者lem。

lem :: forall x y. SBool (x == y) -> ((x ~~ y) => Void) -> Choose x y :~: 2
lem decideEq p = case decideEq of
  STrue -> absurd p
  SFalse -> Refl