在他的論文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 擴展符是否允許用普通代數來表達這個？

uj5u.com熱心網友回復：

區別在于類別。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。

uj5u.com熱心網友回復：

這是夏立耀的答案的擴展版本。我的任何錯誤等等。

除了代數之外，Hinze的大眾論文泛型涉及將它們提升到型別類，以便靜態完成計算。這種對應是直截了當的，并且獨立于代數本身的編碼。

該論文在可擴展和模塊化泛型中進行了擴展，它分解了（靜態）計算，以更好地逼近“運算式問題”的解決方案。

U 索引版本

我們用U_*

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

我們把它提升為一種，用{-# LANGUAGE DataKinds #-}. 這意味著我們將其視為一個離散類別，其物件由型別建構式歸納定義，'UInt并且'UPair

這是一個（歸納定義的）函子，從中U將Hask每個物件映射U到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

這是型別之間的純映射，我們可以在型別簽名中使用它

類別(U->Hask)

該類別(U->Hask)有

• 對于物件 m :: U -> * 索引型別

• 對于態射m ~> n = forall (i :: *). m i -> n i ，索引型別之間的索引函式

• 明顯的身份和組成

這是一個（歸納定義的）物件(U->Hask)

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

請注意，它只是具體化（“理解”）Uin的現有結構* ：對于 的每個索引U，它是一種型別，作為一個集合，它對于 in 的每個物件都有一個元素U，由建構式定義。我們可以使用普通函式來消費或產生這些型別的值。 *本身可以被視為索引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 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 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 such 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.

標籤：哈斯克尔 类型 代数 代数数据类型 范畴论

上一篇：闡明HaskellRecord上的通用量化

下一篇：Ubuntu下交換Alt和Ctrl (適用于任何按鍵修改)