haskell - 如何在Haskell中使用引用来指示类型检查器？

Question

在以下程序中填补漏洞是否一定需要非 build 性的手段？如果是，那么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 = _

Answer 1

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

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

完全不准确的摘要:

第一幕:证明搜索很容易。

第二幕:也依赖类型。

第三幕:Haskell仍然适合编写依赖类型的程序。

一，证明搜索游戏

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

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

lem = (exp)

对于某些表达式 (exp)。现在，我们只需要查找一个表达式。

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

它可以将页面放在单个列中，因此开始时并没有那么大。
而且，它们大多数是糖，用于某种形式的功能应用或
模式匹配;我们也可以用字典去掉糖类类
通过，所以我们剩下的是可笑的小λ演算:

lambdas，\x -> ...

模式匹配，case ... of ...

函数应用程序，f x

构造函数，C(包括整数文字)

常数，c(用于无法根据上述结构编写的基元，因此包括各种内置函数(seq)，如果可能的话还可以使用FFI)

变量(受lambda和大小写限制)

我们可以排除所有常量，理由是我认为问题是
纯粹关于纯lambda演算(或读者可以枚举常数，
排除magic常量，例如 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

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

可能是构造函数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微积分的 class /书
直到简单型lambda演算的归一化证明
是您入门的基本工具。以下论文包含一个
在第一部分的介绍，但我承认我是一个糟糕的法官
这种 Material 的难度: 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根本不像大多数人所说的“为所有人”所指。

关于相关性的一些讨论可以在Richard Eisenberg的 Dependent Types in 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，精益)，对类型族 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