如果你足够努力去实现一个功能，你就能说服自己
这是不可能的。如果你不相信，可以提出论据
更正式：我们详尽地列举了程序，发现没有一个是可能的。事实证明，只有六个有意义的案例需要考虑。
我想知道为什么这个论点不经常提出。
完全不准确的总结：
- 第一幕：证明搜索很容易。
- 第二幕：依赖类型也是如此。
- 第三幕：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 和大小写约束）
我们可以排除每个常数，因为我认为问题是
真正关于纯 lambda 演算（或者读者可以枚举常量，
排除像undefined，unsafeCoerce这样的黑魔法常量，
unsafePerformIO 让一切都崩溃（任何类型都有人居住，并且，对于
其中一些，类型系统不健全），并留下白色魔法
目前的理论论证可以通过 a 推广到的常数
资金充足的论文）。
我们也可以合理地假设我们想要一个不涉及递归的解决方案
（如果您觉得自己做不到，可以消除 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 知道并可以派生或制作强制的语法
（等式证明）明确并继续玩这个证明搜索游戏
和他们一起），所以这不会输入检查：
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
所以最后一个子case是变量case：
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 演算的规范化证明应该给出
你开始的基本工具。以下论文包含一个
在第一部分介绍这个主题，但我承认我是个糟糕的法官
此类材料的难度：Which types have a unique inhabitant?
Focusing on pure program equivalence,
作者：Gabriel Scherer。
请随意提出更充分的资源和文献。
二。修正命题并用依赖类型证明它
您最初的直觉认为这应该编码一个有效的命题
绝对有效。我们如何修复它以使其可证明？
从技术上讲，我们正在查看的类型是用 forall 量化的：
forall x y. (x :~: y -> Void) -> Choose x y :~: 2
forall 的一个重要特征是它是一个不相关量词。
它引入的变量不能在这种类型的术语中“直接”使用。尽管在存在依赖类型时该方面变得更加突出，
今天它仍然弥漫在 Haskell 中，提供了另一种直觉来解释为什么这个（以及许多其他例子）在 Haskell 中是不可“证明的”：如果你想想为什么你
认为这个命题是有效的，你自然会从 x 是否等于 y 的案例拆分开始，但即使是这样的案例拆分，你也需要一种方法来
决定你站在哪一边，当然要看x和y，
所以它们不可能无关紧要。 Haskell 中的forall 与大多数人所说的“for all”完全不同。
关于相关性问题的一些讨论可以在 Richard Eisenberg 的论文Dependent Types in Haskell 中找到（特别是，第 3.1.1.5 节是初始示例，第 4.3 节是 Dependent Haskell 中的相关性，第 8.7 节是为了与其他具有依赖类型的语言）。
依赖的 Haskell 将需要一个 relevant 量词来补充 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)。
实际上，那台机器不是必需的，这只是缩短了
回答。
此时我正在编造一些东西，因为 Dependent Haskell 还不存在，
但这在相关的依赖类型语言（Coq、Agda、
Idris, Lean), 对类型族 Choose 的适当替换取模
（类型族在某种意义上太强大了，不能仅仅翻译为
功能，所以可能是作弊，但我离题了）。
这是 Coq 中的一个类似程序，还显示 lem 应用于 1 和 2
并且一个合适的证明确实可以通过choose 1 2 = 2的自反性简化为一个证明。
https://gist.github.com/Lysxia/5a9b6996a3aae741688e7bf83903887b
三。没有依赖类型
这里的一个关键问题是Choose 是一个封闭类型
具有重叠实例的族。这是有问题的，因为有
没有适当的方式来表达 x 和 y 在 Haskell 中不相等的事实，
要知道第一个子句Choose x x 不适用。
如果您喜欢 Pseudo-Dependent 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