证明类型级析取的幂等性

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

你所要求的东西是不可能的，但可能会有类似的东西来代替。这是不可能的，因为证明需要对类型级别布尔值进行案例分析，但是您没有数据来使这样的事件发生。修复方法是通过单例包含这样的信息。

首先，让我注意到您的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。例外是在instance声明中:实例头中的a将匹配任何内容，因此即使该内容尚未明显变为t，该实例也将被激发。但我离题了。)

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

我们需要在b上通过案例进行推理。请记住，对于一般的递归类型族，我们可以定义既不是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是行为良好的布尔值之一，以某种方式计算一个值。因此，让我们一起歌唱

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有一个模板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也可以有一个“隐式”变量，默认情况下参数是隐藏的。这两种方法分别对应于使用单例系列和类，但是不需要三次定义数据类型来获得额外的工具包。

值得一提的是，在全类型理论中，不需要在运行时传递额外的布尔b副本。问题是，b只是用来证明数据可以从p (Or b b)传输到p b，而不一定是为了传输数据。我们在运行时不在活页夹下计算，所以没有办法炮制一个不诚实的等式证明，因此我们可以擦除证明组件和交付它的b副本。正如Randy Pollack所说，在一个高度规范化的微积分中工作的最好的事情就是不必将事情标准化。

Answer 2

正如John L在他的评论中所说的那样，据我所知，目前没有额外的限制就无法做到这一点。您不能利用这样一个事实，即Bool在术语级别上是一种封闭类型，并且无法在idemp中对kind Bool的类型变量进行案例分析。

典型的解决方案是使用单例类型在术语级别上反映Bool类型结构：

data SBool :: Bool -> * where
  SFalse :: SBool False
  STrue  :: SBool True

对于任何b :: Bool，只有一个SBool b的居民(当然是模数undefined )。

使用SBool，这个定理很容易证明(我不知道您为什么要添加额外的相等约束，我打算删除它)：

idemp' :: SBool a -> proxy (Or a a) -> proxy a
idemp' SFalse x = x
idemp' STrue  x = x

您可以通过定义一个可以创建SBool表示的类来隐式传递参数，而不是显式地传递参数：

class CBool (b :: Bool) where
  sBool :: SBool b

instance CBool True  where sBool = STrue
instance CBool False where sBool = SFalse

然后：

idemp :: CBool a => proxy (Or a a) -> proxy a
idemp = idemp' sBool

我不认为您可以摆脱CBool约束，但它对于任何a :: Bool来说都是微不足道的，所以这不是一个很强的假设。