23

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

{-# 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，但这是作弊。）

是否可以？

4

2 回答 2

15

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

首先，让我注意你的 for 类型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，通常最好替换为。例外情况是在声明中：实例中的头部将匹配任何内容，因此即使该内容尚未明显变为 ，该实例也会触发。但我离题。）tatainstanceat

我声称idemq无法定义，因为我们没有关于b. 唯一可用的数据存在p于某物中，我们不知道是什么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不能简化为Trueor 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来打包事实，而不是抽象使用 uses 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也可能有一个“隐式”变体，其中参数默认保持隐藏。两者分别对应使用单例族和类，但不需要定义数据类型三遍来获得额外的工具包。

It might be worth mentioning that in a total type theory, it is not needed to pass the extra copy of the Boolean b at run time. The thing is, b is used only to make the proof that data may be transported from p (Or b b) to p b, not necessarily to make the data being transported. We don't compute under binders at run time, so there's no way to cook up a dishonest proof of the equation, hence we can erase the proof component and the copy of b that delivers it. As Randy Pollack says, the best thing about working in a strongly normalizing calculus is not having to normalize things.

于 2013-03-03T11:13:46.593 回答
7

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

典型的解决方案是使用单例类型在术语级别上反映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约束，但是对于 any 来说这都是微不足道的a :: Bool，因此这不是一个非常强的假设。

于 2013-03-03T10:53:14.623 回答