2

自然数的著名 Church 编码可以推广到使用任意函子F。结果是类型，称为它C，定义为

  data C = Cfix { run :: forall r. (F r -> r) -> r }

在这里和下面，为简单起见，我们将假设它F是一个固定的、已经定义的函子。

众所周知，类型C是函子的固定点F，也是C初始F代数。例如，如果函子F a定义为

 data F a b = Empty | Cons a b

然后是F ais的固定点[a]（类型的值列表a）。另外，[a]是初始代数。列表的 Church 编码是众所周知的。但是我找不到这些陈述中的任何一个的严格证明（C是一个固定点，并且C是初始代数）。

问题是，如何严格证明两个陈述之一：

  1. 该类型C是类型 isomorphism 的固定点F C ≅ C。换句话说，我们需要证明存在两个函数，fix :: F C -> C并且unfix :: C -> F C使得fix . unfix = id和unfix . fix = id。
  2. 类型C是函子的初始代数F；即-F代数范畴中的初始对象。换句话说，对于任何给定A函数p :: F A -> A的类型（即是-A代数F），我们都可以找到一个唯一的函数q :: C -> A，它是 F-代数态射。这意味着，q必须使法律q . fix = p . fmap q成立。我们需要证明，给定A和p，这样q的存在并且是唯一的。

这两个语句不等价；但证明（2）意味着（1）。（Lambek 定理说初始代数是同构。）

fix函数的代码unfix可以相对容易地编写：

 fix :: F C -> C
 fix fc  = Cfix (forall r. \g -> g . fmap (\h -> h g) fc )
 unfix :: C -> F C
 unfix c = (run c) (fmap fix)

给定一个函数p :: F A -> A，函数的代码q写成

 q :: C -> A
 q c = (run c) p

然而，似乎很难直接证明函数fix, unfix,q满足所需的性质。我找不到完整的证明。

C证明它是一个初始代数，即它q是唯一的，比证明它更容易fix . unfix = id吗？

在这个问题的其余部分，我将展示一些我能够为证明fix . unfix = id.

仅通过使用给定的函数代码来证明 (1) 或 (2) 是不可能的。我们需要额外的假设。与米田身份相似，

 forall r. (A -> r) -> F r   ≅   F A   ,

我们需要假设函数的代码是完全参数化的（没有副作用，没有特别选择的值或固定类型），以便可以应用参数化定理。所以，我们需要假设类型只包含满足适当自然法则C的类型函数。forall r. (F r -> r) -> r

参数化定理为这种类型签名给出了以下自然法则：对于任何类型Aand B，以及对于任何函数p :: F B -> Aand f :: A -> B，函数c :: forall r. (F r -> r) -> r必须满足等式

  c (f . p) = f . c (p . fmap f)

Using this naturality law with appropriately chosen pand f, one can show that the composition fix . unfixis a certain function of type C -> Cthat must be equal to \c -> (run c) fix.

然而，证明的进一步进展似乎是不可能的。不清楚为什么这个函数必须等于id。

让我们暂时定义函数m：

 m :: (F C -> C) -> C -> C
 m t c = (run c) t

然后我得到的结果写成

fix . unfix  = m fix

也可以证明这一点unfix . fix = fmap (m fix)。

这还有待证明m fix = id。一旦证明了这一点，我们就证明了F C ≅ C。

相同的自然规律c与不同的选择p并f赋予了奇怪的身份

 m fix . m (m fix . fix) = m (m fix . fix)

但不知如何从这个身份中推导出来m fix = id。

4

0 回答 0