如何在Haskell中使用反驳来引导类型检查器？
How to use a refutation to direct the type checker in Haskell?
下面程序中的填坑是否一定需要非建设性的手段？如果是，如果 x :~: y 可判定是否仍然如此？
更一般地说，如何使用反驳来引导类型检查器？
（我知道我可以通过将 Choose 定义为 GADT 来解决这个问题，我专门询问类型族）
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module PropositionalDisequality where
import Data.Type.Equality
import Data.Void
type family Choose x y where
Choose x x = 1
Choose x _ = 2
lem :: (x :~: y -> Void) -> Choose x y :~: 2
lem refutation = _
如果你足够努力去实现一个功能，你就能说服自己
这是不可能的。如果你不相信，可以提出论点
更正式：我们详尽地列举了程序，发现 none 是可能的。事实证明，只有六个有意义的案例需要考虑。
我想知道为什么这个论点不经常出现。
完全不准确的总结：
- 第一幕：证明搜索很简单。
- 第二幕：依赖类型也是。
- 第三幕：Haskell 仍然适合编写依赖类型的程序。
我。证明搜索游戏
首先我们定义搜索space.
我们可以将任何 Haskell 定义简化为以下形式之一
lem = (exp)
对于某些表达式 (exp)。现在我们只需要找到一个表达式。
查看 Haskell 中所有可能的表达方式：
https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-220003
（这不考虑 reader 的扩展、练习）。
它适合单列中的一个页面，所以开始时 没有那么大。
此外，它们中的大多数是用于某种形式的功能应用程序或
模式匹配;我们也可以用字典去除类型classes
通过，所以我们只剩下一个可笑的小 lambda 演算：
- lambdas，
\x -> ...
- 模式匹配，
case ... of ...
- 函数应用，
f x
- 构造函数，
C（包括整数文字）
- 常量，
c（对于无法根据上述构造编写的原语，因此各种内置函数（seq），如果重要的话可能还有 FFI）
- 变量（受 lambda 和大小写约束）
我们可以排除每一个常量，因为我认为问题是
真正关于纯 lambda 演算（或者 reader 可以枚举常量，
排除黑魔法常数，如 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 了解并可以推导或制定强制转换的语法
（等式证明）明确并继续玩这个证明搜索游戏
和他们一起），所以这不是类型检查：
lem = \refutation -> Refl
也许有某种方法可以构建相等性证明，但是
expression 将以其他内容开始，这将是另一个
证明案例。
可能是构造函数的某种应用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.
要阅读有关此主题的更多信息，我想 course/book 关于 lambda 演算
直到简单类型 lambda 演算的归一化证明应该给出
你开始的基本工具。以下论文包含一个
在第一部分介绍了这个主题，但不可否认我是一个糟糕的判断者
这样的难度material：哪些类型有独特的居民？
专注于纯程序等价，
加布里埃尔·谢勒 (Gabriel Scherer)。
欢迎提出更充足的资源和文献。
二．修正命题并用依赖类型证明它
你最初的直觉是这应该编码一个有效的命题
绝对有效。我们如何修复它以使其可证明？
从技术上讲，我们正在查看的类型是用forall量化的：
forall x y. (x :~: y -> Void) -> Choose x y :~: 2
forall 的一个重要特征是它是一个 不相关的 量词。
它引入的变量不能在这种类型的术语中使用"directly"。虽然这方面在依赖类型的存在下变得更加突出，
它仍然在 Haskell 今天 流行，提供了另一种直觉来解释为什么这个（以及许多其他例子）在 Haskell 中不是 "provable"：如果你想为什么你
认为这个命题是有效的，你自然会从 x 是否等于 y 的案例拆分开始，但即使要进行这样的案例拆分，你也需要一种方法来
决定你站在哪一边，当然要看x和y，
所以他们不能无关紧要。 Haskell 中的 forall 与大多数人对 "for all" 的意思完全不同。
关于相关性问题的一些讨论可以在 Richard Eisenberg 的论文 Dependent Types in Haskell 中找到（特别是第 3.1.1.5 节中的初始示例，第 4.3 节中的相关性 Haskell 和第 8.7 节用于与具有依赖类型的其他语言进行比较）。
Dependent 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
这也假设第一个 class 不平等的概念 /~，补充 ~，
帮助 Choose reduce when it is in the context and a decision function
(==?) :: foreach x y. Either (x :~: y) (x :/~: y)。
实际上，那台机器不是必需的，那只是为了缩短
回答。
此时我正在编造东西，因为 Dependent Haskell 还不存在，
但这在相关的依赖类型语言（Coq、Agda、
Idris, Lean), modulo 类型族的适当替换 Choose
（类型族在某种意义上太强大了，不能仅仅翻译为
功能，所以可能是作弊，但我离题了）。
这是 Coq 中的一个类似程序，它还显示了 lem 适用于 1 和 2
并且合适的证明确实通过 choose 1 2 = 2.
的自反性简化为证明
https://gist.github.com/Lysxia/5a9b6996a3aae741688e7bf83903887b
三。没有依赖类型
这里的一个关键困难来源是 Choose 是一个封闭类型
具有重叠实例的家庭。这是有问题的，因为有
没有正确的方式来表达 x 和 y 在 Haskell 中不相等的事实，
要知道第一个子句 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 的 "irrelevance" 的声明并不矛盾，该函数正在检查一个布尔值（或者更确切地说是一个 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
下面程序中的填坑是否一定需要非建设性的手段？如果是，如果 x :~: y 可判定是否仍然如此？
更一般地说，如何使用反驳来引导类型检查器？
（我知道我可以通过将 Choose 定义为 GADT 来解决这个问题，我专门询问类型族）
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module PropositionalDisequality where
import Data.Type.Equality
import Data.Void
type family Choose x y where
Choose x x = 1
Choose x _ = 2
lem :: (x :~: y -> Void) -> Choose x y :~: 2
lem refutation = _
如果你足够努力去实现一个功能，你就能说服自己 这是不可能的。如果你不相信，可以提出论点 更正式：我们详尽地列举了程序，发现 none 是可能的。事实证明，只有六个有意义的案例需要考虑。
我想知道为什么这个论点不经常出现。
完全不准确的总结：
- 第一幕：证明搜索很简单。
- 第二幕：依赖类型也是。
- 第三幕：Haskell 仍然适合编写依赖类型的程序。
我。证明搜索游戏
首先我们定义搜索space.
我们可以将任何 Haskell 定义简化为以下形式之一
lem = (exp)
对于某些表达式 (exp)。现在我们只需要找到一个表达式。
查看 Haskell 中所有可能的表达方式： https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-220003 （这不考虑 reader 的扩展、练习）。
它适合单列中的一个页面，所以开始时 没有那么大。 此外，它们中的大多数是用于某种形式的功能应用程序或 模式匹配;我们也可以用字典去除类型classes 通过，所以我们只剩下一个可笑的小 lambda 演算：
- lambdas，
\x -> ... - 模式匹配，
case ... of ... - 函数应用，
f x - 构造函数，
C（包括整数文字） - 常量，
c（对于无法根据上述构造编写的原语，因此各种内置函数（seq），如果重要的话可能还有 FFI） - 变量（受 lambda 和大小写约束）
我们可以排除每一个常量，因为我认为问题是
真正关于纯 lambda 演算（或者 reader 可以枚举常量，
排除黑魔法常数，如 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 了解并可以推导或制定强制转换的语法 （等式证明）明确并继续玩这个证明搜索游戏 和他们一起），所以这不是类型检查：lem = \refutation -> Refl也许有某种方法可以构建相等性证明，但是 expression 将以其他内容开始，这将是另一个 证明案例。
可能是构造函数的某种应用
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.
要阅读有关此主题的更多信息，我想 course/book 关于 lambda 演算 直到简单类型 lambda 演算的归一化证明应该给出 你开始的基本工具。以下论文包含一个 在第一部分介绍了这个主题，但不可否认我是一个糟糕的判断者 这样的难度material：哪些类型有独特的居民？ 专注于纯程序等价， 加布里埃尔·谢勒 (Gabriel Scherer)。
欢迎提出更充足的资源和文献。
二．修正命题并用依赖类型证明它
你最初的直觉是这应该编码一个有效的命题 绝对有效。我们如何修复它以使其可证明？
从技术上讲，我们正在查看的类型是用forall量化的：
forall x y. (x :~: y -> Void) -> Choose x y :~: 2
forall 的一个重要特征是它是一个 不相关的 量词。
它引入的变量不能在这种类型的术语中使用"directly"。虽然这方面在依赖类型的存在下变得更加突出，
它仍然在 Haskell 今天 流行，提供了另一种直觉来解释为什么这个（以及许多其他例子）在 Haskell 中不是 "provable"：如果你想为什么你
认为这个命题是有效的，你自然会从 x 是否等于 y 的案例拆分开始，但即使要进行这样的案例拆分，你也需要一种方法来
决定你站在哪一边，当然要看x和y，
所以他们不能无关紧要。 Haskell 中的 forall 与大多数人对 "for all" 的意思完全不同。
关于相关性问题的一些讨论可以在 Richard Eisenberg 的论文 Dependent Types in Haskell 中找到（特别是第 3.1.1.5 节中的初始示例，第 4.3 节中的相关性 Haskell 和第 8.7 节用于与具有依赖类型的其他语言进行比较）。
Dependent 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
这也假设第一个 class 不平等的概念 /~，补充 ~，
帮助 Choose reduce when it is in the context and a decision function
(==?) :: foreach x y. Either (x :~: y) (x :/~: y)。
实际上，那台机器不是必需的，那只是为了缩短
回答。
此时我正在编造东西，因为 Dependent Haskell 还不存在，
但这在相关的依赖类型语言（Coq、Agda、
Idris, Lean), modulo 类型族的适当替换 Choose
（类型族在某种意义上太强大了，不能仅仅翻译为
功能，所以可能是作弊，但我离题了）。
这是 Coq 中的一个类似程序，它还显示了 lem 适用于 1 和 2
并且合适的证明确实通过 choose 1 2 = 2.
https://gist.github.com/Lysxia/5a9b6996a3aae741688e7bf83903887b
三。没有依赖类型
这里的一个关键困难来源是 Choose 是一个封闭类型
具有重叠实例的家庭。这是有问题的，因为有
没有正确的方式来表达 x 和 y 在 Haskell 中不相等的事实，
要知道第一个子句 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 的 "irrelevance" 的声明并不矛盾，该函数正在检查一个布尔值（或者更确切地说是一个 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