haskell - GADT 的索引初始代数

Question

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

data Nat :: ⋆ where 
   Zero :: Nat
   Succ :: Nat → Nat

可以看成一个初始代数 NatF Nat -> Nat对于 NatF a = 1 + a它的教会代表 ∀ x. ( NatF x → x ) → x是作为初始代数所赋予的普遍属性的见证
因此，他重新定义了等价的 Nat

newtype Nat = Nat{fold :: ∀ nat . Algebra nat → nat } 
data Algebra nat = With{
  foldZero :: nat,
  foldSucc :: nat → nat }

这会产生一个函数 ∀ nat . Algebra x → (Nat → x)它给出了初始代数的唯一代数态射。 (也可以将 Nat 看作是健忘仿函数的极限锥，该函数在代数类别中的每个对象处产生该锥的分量)。这是经典。
但他随后提到了以下数据类型的 Church 编码，即 GADT，旨在成为类型化类型表示

data Rep :: ⋆ → ⋆ where
  Int :: Rep Int
  Pair :: ∀α β . Rep α → Rep β → Rep (α, β)

编码为

data Rep τ = Rep{fold :: ∀rep . Algebra rep → rep τ } 
data Algebra rep = With{
  foldInt :: rep Int,
  foldPair :: ∀α β . rep α → rep β → rep (α, β) }

int:: Rep Int
int = Rep (λc → foldInt c)

pair :: ∀α β . Rep α → Rep β → Rep (α, β)
pair a b = Rep (λc → foldPair c (fold a c) (fold b c))

这种编码是什么代数？
由于索引，这不是一个简单的代数。
一些 Kan 扩展符是否允许用普通代数来表达这个？

Answer 1

区别在于类别。 Nat是类型范畴中的初始代数。 Rep是索引类型类别中的初始代数。索引类型的类别具有作为对象的类型构造函数 * -> * , 并作为 f ~> g 的态射, 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)

同样是 Church 编码

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 .