如何使用引用来指导Haskell中的类型检查器？

Question

在以下程序中填充孔是否一定需要非建设性的手段？如果是，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仍然适合编写依赖类型的程序。

I。证明搜索游戏

首先我们定义搜索空间。

我们可以将任何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演算（或读者可以枚举常数，排除诸如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，但没有证据表明上下文（在这里我们可以形式化并枚举类型相等typechecker知道并且可以派生强制性语法（平等证明）明确并继续玩此证明搜索游戏与他们），因此不会输入check：

  Choose x y ~ 2

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

• 可能是构造函数lem = \refutation -> Refl 的某些应用，或者变量C x1 x2 ...（是否应用）；但这是不可能的类型正确，它必须以某种方式产生refutation，而(:~:)实际上是唯一的方法。
• 否则可能是Refl。 WLOG，左侧没有嵌套的case，也没有任何嵌套构造函数，因为在两种情况下都可以简化表达式：

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 {}从应用程序中删除这种情况，从考虑WLOG。

case

没有其他情况了。搜索完成，我们没有找到-- 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)
的实现。 QED。
要阅读有关此主题的更多信息，我想一本关于lambda微积分的课程/书直到简单型lambda演算的归一化证明是您入门的基本工具。以下论文包含一个在第一部分中对该主题进行了介绍，但是我承认我是一个糟糕的法官这种材料的难度：(x :~: y -> Void) -> Choose x y :~: 2，通过加布里埃尔·谢勒（Gabriel Scherer）。
随时建议提供足够的资源和文献。
II。修正命题并用依赖类型证明]
您最初的直觉认为这应该编码一个有效的命题绝对是有效的。我们如何解决它以使其可证明？
从技术上讲，我们要查看的类型是用Which types have a unique inhabitant?
Focusing on pure program equivalence量化的：
forall
forall x y. (x :~: y -> Void) -> Choose x y :~: 2
的重要特征是它是
无关
量词。在这种类型的术语中，它引入的变量[[不能直接使用]。尽管在依赖类型的存在下，这一方面变得更加突出，它仍然遍及Haskell today，提供了另一种直觉来说明为什么此（以及许多其他示例）在Haskell中“不可证明”：如果您想一想为什么认为该命题是有效的，您自然会从forall是否等于x的大小写分割开始，但是即使要进行这种大小写分割，您也需要一种方法decide您在哪一边，当然必须看y和x，因此它们不会无关紧要从属Haskell将需要一个relevant量词来补充y，并且这将使我们更接近证明这一点：
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。实际上，不需要机械，只是缩短了时间回答。

此时，我正在编造东西，因为相关的Haskell还不存在，但这在相关的依存类型语言（Coq，Agda，Idris，精益），对类型族(==?) :: foreach x y. Either (x :~: y) (x :/~: y)进行适当的替换（类型家族在某种意义上太强大了，以至于不能仅仅翻译为功能，所以可能是作弊，但我离题了。
这里是Coq中的一个可比较程序，也显示Choose应用于1和2并且适当的证明确实会因lem的反射率而减少为证明。
choose 1 2 = 2
III。没有依赖类型
这里的关键困难源是https://gist.github.com/Lysxia/5a9b6996a3aae741688e7bf83903887b是封闭类型实例重叠的家庭。这是有问题的，因为有无法表达Haskell中Choose和x不相等这一事实，知道第一个子句y不适用。
如果您是伪依赖的Haskell，更有用的方法是使用布尔类型相等：
Choose x x
等式约束的替代编码对此样式很有用：

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

type Choose x y = If (x == y) 1 2
这样，我们可以得到上面的类型提议的另一个版本，可在当前的Haskell中表示（其中type x ~~ y = ((x == y) ~ 'True)
type x /~ y = ((x == y) ~ 'False)
是SBool的单例类型），这基本上可以理解为添加了Bool相等的假设并且x是可确定的：

y