haskell - 证明类型级析取的幂等性

Question

我已经定义了类型级析取如下:

{-# LANGUAGE DataKinds, TypeFamilies #-}

type family Or (a :: Bool) (b :: Bool) :: Bool
type instance Or False a = a
type instance Or True a = True

现在我想证明(在 Haskell 中)它是幂等的。也就是我要建一个词 idemp带类型

idemp :: a ~ b => proxy (Or a b) -> proxy a

这在操作上等同于 id . (显然，我可以将其定义为 unsafeCoerce ，但这是作弊。)

可能吗？

Answer 1

你要求的东西是不可能的，但很像它可能会做的事情。这是不可能的，因为证明需要对类型级别的 bool 值进行案例分析，但是您没有数据可以让您发生这样的事件。解决方法是通过单例仅包含此类信息。

首先，让我注意您的 idemp 类型有点混淆。约束 a ~ b只需将同一事物命名两次。以下类型检查:

idemq :: p (Or b b) -> p b
idemq = undefined
idemp :: a ~ b => p (Or a b) -> p a
idemp = idemq

(如果您有一个约束 a ~ t 其中 t 不包含 a ，通常最好用 t 替换 a 。异常(exception)是在 instance 声明中:实例头中的 a将匹配任何东西，因此即使那个东西还没有明显变成 t ，实例也会触发。但我离题了。)

我声称 idemq无法定义，因为我们没有关于 b 的有用信息.唯一可用的数据是 p -of-something，我们不知道是什么 p是。

我们需要根据 b 上的案例进行推理.请记住，对于一般递归类型族，我们可以定义类型级别的 bool 值，它们既不是 True也不是 False .如果我打开 UndecidableInstances , 我可以定义

type family Loop (b :: Bool) :: Bool
type instance Loop True = Loop False
type instance Loop False = Loop True

所以 Loop True不能简化为 True或 False ，而且在本地更糟糕的是，没有办法证明

Or (Loop True) (Loop True) ~ Loop True     -- this ain't so

没有办法摆脱它。我们需要运行时证据来证明我们的 b是表现良好的 bool 值之一，它以某种方式计算出一个值。让我们歌唱

data Booly :: Bool -> * where
  Truey   :: Booly True
  Falsey  :: Booly False

如果我们知道 Booly b ，我们可以做一个案例分析，告诉我们 b是。然后每个案例都会顺利通过。下面是我的玩法，使用 PolyKinds 定义的相等类型打包事实，而不是抽象使用 p b .

data (:=:) a b where
  Refl :: a :=: a

我们的关键事实现在被清楚地陈述和证明:

orIdem :: Booly b -> Or b b :=: b
orIdem Truey   = Refl
orIdem Falsey  = Refl

我们可以通过严格的案例分析来部署这个事实:

idemp :: Booly b -> p (Or b b) -> p b
idemp b p = case orIdem b of Refl -> p

案情分析一定要严密，要查证证据不是乱七八糟的谎言，而是诚实正直 Refl默默收拾 Or b b ~ b的证明这是修复类型所必需的。

如果您不想明确地使用所有这些单例值，您可以按照 kosmikus 的建议，将它们隐藏在字典中，并在需要时提取它们。

Richard Eisenberg 和 Stephanie Weirich 有一个 Template Haskell 库，可以为您处理这些家庭和类。她也可以构建它们并让您编写

orIdem pi b :: Bool. Or b b :=: b
orIdem {True}   = Refl
orIdem {False}  = Refl

在哪里 pi b :: Bool.扩展到 forall b :: Bool. Booly b -> .

但它是如此的闲聊。这就是为什么我的帮派正在努力添加一个实际的 pi对于 Haskell，它是一个非参数量词(与 forall 和 -> 不同)，可以通过 Haskell 类型语言和术语语言之间的非平凡交集中的东西来实例化。这个 pi也可以有一个“隐式”变体，默认情况下参数是隐藏的。两者分别对应使用单例族和类，但不需要定义数据类型三遍来获得额外的工具包。

值得一提的是，在总类型理论中，不需要传递 bool 值 b 的额外副本。在运行时。问题是， b仅用于证明数据可以从 p (Or b b) 传输。至 p b ，不一定要使数据被传输。我们不会在运行时在活页夹下进行计算，因此无法对等式进行不诚实的证明，因此我们可以删除证明部分和 b 的副本交付它。正如 Randy Pollack 所说，在强归一化微积分中工作的最好的事情是不必对事物进行归一化。