Indexed Initial algebras for GADTs-CodePudding

In his paper Generics for the Masses Hinze reviews encoding of data type.

Starting from Nat

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

It can be viewed as an initial algebra NatF Nat -> Nat for NatF a = 1 a

Its Church representation ∀ x. ( NatF x → x ) → x is a witness of the universal property conferred by being an initial algebra

He thus redefines an equivalent Nat

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

This yields a function ∀ nat . Algebra x → (Nat → x) which gives the unique algebra morphism from the initial algebra. (One can also view Nat as a limit cone for the forgetful functor, and this function yields the components of that cone at each object in the category of algebras). This is classic.

But he then mentions a Church encoding of the following datatype, which is a GADT, intended to be a typed type representation

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

Which is encoded as

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))

What kind of algebra is this encoding ? It's not a plain algebra, due to the indices. Does some Kan extension-fu allow to express this an ordinary algebra ?

CodePudding user response：

The difference is the category. Nat is an initial algebra in the category of types. Rep is an initial algebra in the category of indexed types. The category of indexed types has as objects type constructors of kind * -> *, and as morphisms from f ~> g, functions of type forall t. f t -> g t.

Then Rep is the initial algebra for the functor RepF defined as follows:

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

And similarly the Church encoding

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

yields, for every Algebra rep, a mapping forall t. Rep t -> rep t.