GADT 的索引初始代数

Question

Hinze在他的论文Generics for the Masses中回顾了数据类型的编码。

\n

从...开始Nat

\n

data Nat :: \xe2\x8b\x86 where \n   Zero :: Nat\n   Succ :: Nat \xe2\x86\x92 Nat\n

\n

NatF Nat -> Nat它可以被视为初始代数NatF a = 1 + a

\n

它的教会代表\xe2\x88\x80 x. ( NatF x \xe2\x86\x92 x ) \xe2\x86\x92 x是初始代数所赋予的普遍财产的见证

\n

因此他重新定义了一个等价的Nat

\n

newtype Nat = Nat{fold :: \xe2\x88\x80 nat . Algebra nat \xe2\x86\x92 nat } \ndata Algebra nat = With{\n  foldZero :: nat,\n  foldSucc :: nat \xe2\x86\x92 nat }\n

\n

这允许构建一个函数\xe2\x88\x80 x . Algebra x \xe2\x86\x92 (Nat \xe2\x86\x92 x)，该函数对于任何代数都从初始代数中赋予其独特的代数态射。（我们也可以将其视为Nat健忘函子的极限锥体，并且该函数在代数范畴中的每个对象处产生该锥体的分量）。这很经典。

\n

但他随后提到了以下数据类型的 Church 编码，即 GADT，旨在成为类型化的类型表示

\n

data Rep :: \xe2\x8b\x86 \xe2\x86\x92 \xe2\x8b\x86 where\n  Int :: Rep Int\n  Pair :: \xe2\x88\x80\xce\xb1 \xce\xb2 . Rep \xce\xb1 \xe2\x86\x92 Rep \xce\xb2 \xe2\x86\x92 Rep (\xce\xb1, \xce\xb2)\n

\n

其编码为

\n

data Rep \xcf\x84 = Rep{fold :: \xe2\x88\x80rep . Algebra rep \xe2\x86\x92 rep \xcf\x84 } \ndata Algebra rep = With{\n  foldInt :: rep Int,\n  foldPair :: \xe2\x88\x80\xce\xb1 \xce\xb2 . rep \xce\xb1 \xe2\x86\x92 rep \xce\xb2 \xe2\x86\x92 rep (\xce\xb1, \xce\xb2) }\n\nint:: Rep Int\nint = Rep (\xce\xbbc \xe2\x86\x92 foldInt c)\n\npair :: \xe2\x88\x80\xce\xb1 \xce\xb2 . Rep \xce\xb1 \xe2\x86\x92 Rep \xce\xb2 \xe2\x86\x92 Rep (\xce\xb1, \xce\xb2)\npair a b = Rep (\xce\xbbc \xe2\x86\x92 foldPair c (fold a c) (fold b c))\n

\n

这种编码是什么类型的代数？\n由于索引的原因，它不是普通代数。\n某些 Kan 扩展符是否允许将其表示为普通代数？

\n

Answer 1

区别在于类别。Nat是类型范畴中的初始代数。Rep是索引类型范畴中的初始代数。索引类型的类别具有 kind 的对象类型构造* -> *函数和f ~> gtype 的函数的态射forall t. f t -> g t。

那么Rep函子的初始代数RepF定义如下：

data RepF rep :: * -> * where
  Int :: RepF rep Int
  Pair :: forall a b. rep a -> rep b -> RepF rep (a, b)

类似地，教会编码

newtype Rep t = Rep { fold :: forall rep. Algebra rep -> rep t }
type Algebra rep = RepF rep ~> rep
type f ~> g = forall t. f t -> g t

对于每个Algebra rep，都会产生一个映射forall t. Rep t -> rep t。