Indexed Initial algebras for GADTs

Question

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 allows to build a function ∀ x . Algebra x → (Nat → x) which to any algebra gives the unique algebra morphism to it 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 ?

Landside

Answer 1

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.

Middlebrow

Explicitly, RepF maps a type constructor m : * -> * to a type constructor RepF m : * -> * where we can't choose the index, unlike, say, (m + m) a = m a + m a. It's a bit odd. Or we can choose the index and we have to see the types as discrete categories themselves (sometimes empty, for say, Rep Bool), making that a 2-functor (?). If we get rid of GADT and have explicit type equation (Leibniz equality or :~: ) in the constructors, does this interpretation holds ? – Landside

What do you mean by "choose the index"? – Middlebrow

I was confused. By choosing the index I meant applying the type constructor Rep at a particular type, say Char. Rephrasing your solution (hopefully) : we can always talk about types Rep Char, although we can't construct a value for it. Since it has no values, we have functions from it to any other types. So this separates the types from how we construct values of that type. Notably (that was probably the source of my puzzle) we can't just write a simple ordinary polynomial functor (?). Do you mind if I expand your answer separately to make sure I have it right ? (feel free to copy) – Landside

Sure feel free to edit my answer. – Middlebrow

Answer 2

Here is an expanded version of the answer by Li-yao Xia. Any mistake mine, etc..

Beside the algebras, the Generics for the masses paper by Hinze involves lifting them to typeclasses so that computation is done statically. That correspondance is straightforward and independant from the encoding as algebras themselves.

The paper is extended in Extensible and Modular Generics for the Masses which decomposes the (static) computation to better approximate a solution to the "expression problem".

U-Indexed version

We declare the type U (an object of *) with

data U where
  UPair :: U -> U -> U
  UInt :: U

and we lift it to a kind, with {-# LANGUAGE DataKinds #-}. This means we consider it as a discrete category, whose objects are inductively defined by the type constructor 'UInt and 'UPair

Here is a (inductively defined) functor from U to Hask which maps every object of U to an object of Hask

data Pair α β = Pair {outl :: α, outr :: β}

data Unit = Unit

type family Star (u :: U) :: * where
  Star (UPair a b) = Pair (Star a) (Star b)
  Star UInt = Int

This is a pure mapping between types, and we can use it in type signatures

Category (U->Hask)

The category (U->Hask) has

• for object m :: U -> * the indexed types

• for morphisms m ~> n = forall (i :: *). m i -> n i the indexed functions between indexed types

• obvious identity and composition

Here is a (inductively defined) object of (U->Hask)

data DRep :: U -> * where
  DPair :: DRep a -> DRep b -> DRep (UPair a b)
  DInt :: DRep UInt

Note that it merely reifies ("comprehend") the existing structure of U in * : For each index of U, it is a type, which, seen as a set, has one element for each object in U, defined by the constructors. We can consume or produce values of those types using ordinary functions. * itself can be viewed as indexed by 1

This illustrate both type signature and computation with "reified U"

toStar :: DRep a -> Star a
toStar DInt = 0
toStar (DPair a b) = Pair (toStar a) (toStar b)

Functor (U->Hask) -> (U->Hask)

A functor maps objects to objects, arrows to arrows, and more generally compositions to compositions

-- Object mapping of the endofunctor RepF :: (U->Hask) -> (U->Hask)
-- object of the source category (U->Hask) are transported to
-- object of the target category (U->Hask)
data RepF (m :: U -> *) :: U -> * where
  FPair :: m a -> m b -> RepF m (UPair a b)
  FInt :: RepF m UInt

-- Morphism mapping of endofunctors :: (U->Hask) -> (U->Hask)
-- morphisms of the source category (U->Hask) are transported to
-- morphisms in the target category (U->Hask)
-- between the transported objects
class UFunctor (h :: ((U -> *) -> U -> *)) where
  umap :: (forall (i :: U). m i -> n i) -> h m i -> h n i

-- Morphism mapping (implicit form) of the endofunctor RepF :: (U->Hask) -> (U->Hask)
instance UFunctor RepF where
  umap n = \case
    FPair ma mb -> FPair (n ma) (n mb)
    FInt -> FInt

-- We call repF the explicit action on morphism of RepF
repF :: (forall i. m i -> n i) -> RepF m i -> RepF n i
repF = umap

Algebras

An h-algebra "at m" or "of carrier m", where m belongs to (U->Hask) is a morphism (in (U->Hask))

      h m ~> m      

between the transported object h m and m. More generally, an h-algebra at m, where m is a functor A -> (U->Hask) is a collection of morphisms (in (U->Hask))

     α_a :: h (m a) ~> m a 

indexed by the objects a of A, verifying the naturality condition α_a;m f = h m f; α_b for any f: a -> b in A

type UAlg h m = forall (i :: U). h m i -> m i

-- rep is an RepF-algebra of carrier DRep
rep :: forall (x :: U). RepF DRep x -> DRep x
rep (FPair ra rb) = DPair ra rb
rep FInt = DInt

Initiality for algebras

An initial f-algebra is an initial object in the category of algebras. It is the left adjoint of the trivial functor !: f-Alg -> 1 to the trivial category 1 and represents the functor 1(1, ! _) = f-Alg(I,_): f-Alg -> Set.

For any f-algebra, an initial algebra determines a f-algebra morphism from it, which is moreover the only morphism between the two.

This property is equivalent to the carrier being a final cone (a limit cone) for the functor U : f-Alg -> C. (any cone has to map to the carrier of the initial algebra, and mapping to other algebras will factorize by this mapping by the cone property. conversely being a final cone is having a representation of f-alg, C::C^op->Set, which is witnessed by an element f-alg, C (a collection of morphism between algebras), terminal in the category of elements so that any cone f-alg, C comes from precomposition by a unique morphism)

-- This algebra rep is initial

-- This is a witness of initiality -- using the functor instance repF
foldRep :: (forall a. RepF m a -> m a) -> DRep x -> m x
foldRep halg = halg . repF (foldRep halg) . repinv
  where
    repinv :: DRep x -> RepF DRep x
    repinv (DPair ma mb) = FPair ma mb
    repinv DInt = FInt

A witness of that universal property of being a final cone is the Church representation (I think)

type UChurch t x = forall (m :: U -> *). (forall (i :: U). t m i -> m i) -> m x

Hinze encoding is

-- Church Encoding de Hinze
newtype Rep x = Rep {eval :: forall rep. ChurchAlg rep -> rep x}

data ChurchAlg (rep :: * -> *) = ChurchAlg
  { pair_ :: forall a b. rep a -> rep b -> rep (Pair a b),
    int_ :: rep Int
  }

We can verify that this is a specialization

type URep x = UChurch RepF x
-- = forall m. (forall (a :: U). RepF m a -> m a) -> m x
-- = forall m. (
--    pair_ :: RepF m (UPair a b) -> m (UPair a b)
--    int_ :: RepF m UInt -> n UInt ) -> m x
-- = forall m. (
--    pair_ :: m a -> m b -> m (UPair a b)
--    int_ :: m UInt ) -> m x

So that Rep is the carrier of the initial RepF-algebra determined by the final cone. rep is the initial RepF-algebra at Rep.

Hask-indexed version

When we replace U by *, we get an algebra

-- rep is an RepF-algebra of carrier Rep
rep :: forall x. RepF Rep x -> Rep x
rep FInt = Int
rep (FPair ra rb) = Pair ra rb

How can that be an algebra, which require a definition at every type a :: *, when rep is only defined for two indices ?

In reality, rep does defines, for each index of our choice, a morphism of Hask at that index. Let's pick an index which is not Int or (a,b)

repChar (v :: RepF Rep Char) = rep @Char v

This morphism is a valid one, and it is equal to

repChar (v :: RepF Rep Char) = error "impossible"

This is due to the specific definition of Hask whose morphisms are functions between pairs of type viewed as a pair of set of values.

The set of values of type RepF Rep Char is empty : it is initial in Hask. there is a unique function from RepF Rep Char to any other type, "for free", which maps nothing.

Landside