证明类型级别分离的幂等性

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只是两次命名相同的东西.以下typechecks:

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,我们不知道是什么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库,可以为您提供这些系列和类.SHE也可以构建它们并让你写

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

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

但它就是这样一个角色.这就是为什么我的团队正在努力pi向Haskell 添加一个实际的东西,它是一个非参数量词(与foralland 不同->),可以通过Haskell类型和术语之间现在非常重要的交集中的东西进行实例化.这pi也可能有一个"隐式"变体,默认情况下参数保持隐藏状态.这两个分别对应于使用单例族和类,但是没有必要将数据类型定义三次以获得额外的工具包.

这可能是值得一提的是,在总共型理论,是不是需要通过布尔的额外副本b在运行时.问题是,b只用来做证明,数据可以被传输p (Or b b)到p b,不一定使正在传输的数据.我们不会在运行时根据绑定器进行计算,因此无法编制方程式的不诚实证据,因此我们可以删除证明组件及其副本b.正如兰迪波拉克所说,在强正规化计算中工作的最好方法就是不必对事物进行标准化.

Answer 2

正如John L在他的评论中所说,据我所知,目前没有办法在没有额外限制的情况下做到这一点.你不能利用的事实,Bool是一个封闭的一种在长期水平,而且也没有办法做案例分析上那种类型的变量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约束,但对于任何人来说都是如此a :: Bool,所以这不是一个非常强大的假设.