怎麼從編程語言的角度解釋kan extension？

01-02

謝邀，好多大佬關注這個問題呀，我在此先獻醜了，歡迎大家熱烈討論。

Kan擴展(kan extension)是範疇論中一個非常重要的概念，可以用來統一limit/colimit、end/coend等多個概念，在實際編程中也有人用來優化free monad的性能。

那Kan擴展究竟是什麼呢，我們先從其字面意思來看。擴展一般是指擴展集合或類型到更大的集合或類型，Kan擴展就是將函子F的domain沿著函子K擴展到一個更大的類型(或集合)得到一個新的函子L或R(依左Kan擴展還是右Kan擴展來確定)，而且函子K與這個新函子L或R組合成的函子L . K或R . K具有泛性質（universal property）。當這個當組合函子L . K到函子F的自然變換是所有組合函子M . K到函子F的自然變換構成的範疇的initial對象時，函子L就是左Kan擴展，記為 $Lan_k F$ 。當組合函子R . K到函子F的自然變換是terminal對象時函子R就是右Kan擴展，記為 $Ran_k F$ 。

左Kan擴展和右Kan擴展具體如下圖所示：

函子F : C -&> E 沿著函子K : C -&> D的左Kan擴展 $Lan_k F$ ，即函子L : D -&> E是一個特殊的函子。對任意一個函子M : D -&> E，其與函子K : C -&> D的組合函子M . K，可以得到一個自然變換

$alpha$ : F -&> M . K

這個自然變換可以由自然變換

$eta$ : F -&> L . K

分解得到一個唯一的自然變換

$delta$ K : L . K -&> M . K

自然變換 $delta$ K是由如下兩個自然變換

$delta$ : L -&> M $id_K$ : K -&> K

通過自然變換的水平組合得到的。自然變換 $id_k$ 是唯一的自然變換，因此自然變換 $delta$ 也是一個唯一的自然變換，是特殊函子L到函子M之間的自然變換。函子L.K是一個initial對象，滿足泛性質，因此這些自然變換滿足如下關係：

$alpha = delta K cdot eta$

類似的，函子F : C -&> E 沿著函子K : C -&> D的右Kan擴展 $Ran_k F$ ，即函子R : D -&> E是一個特殊的函子。對任意一個函子M : D -&> E，其與函子K : C -&> D的組合函子M . K，可以得到一個自然變換

$eta$ : M . K -&> F

這個自然變換可以由自然變換

$varepsilon$ : R . K -&> F

分解得到一個唯一的自然變換

$sigma$ K : M . K -&> R . K

自然變換 $sigma$ K是由如下兩個自然變換

$sigma$ : M -&> R $id_k$ : K -&> K

通過自然變換的水平組合得到的。自然變換 $id_k$ 是唯一的自然變換，因此自然變換 $sigma$ 也是一個唯一的自然變換，是函子M到特殊函子R之間的自然變換。函子R.K是一個terminal對象，滿足泛性質，因此這些自然變換滿足如下關係：

$eta = varepsilon cdot sigma K$

若對任意函子F : C -&> E和確定的函子K : C -&> D，函子F的右Kan擴展 $Ran_k F$ 都存在，則函子 $Ran_k -$ 是一個從函子範疇 $E^C$ 到函子範疇 $E^D$ 的高階函子。對任意函子M，從函子組合M . K可以得到另一個函子 $- circ K$ ，這是一個從函子範疇 $E^D$ 到函子範疇 $E^C$ 的高階函子。根據前面介紹的組合函子R . K具有的終極泛性質（terminal property），我們可以確定這是一對伴隨函子，記為 $- circ K dashv Ran_k -$ ，這對伴隨函子的自然同構關係如下所示：

$E^C (M circ K, F) cong E^D (M, Ran_k F)$

同樣的，我們可以根據組合函子L . K具有的初始泛性質（initial property），我們可以得到一對伴隨函子 $Lan_k - dashv - circ K$ ，這對伴隨函子的自然同構關係如下所示：

$E^D (Lan_k F, M) cong E^C (F, M circ K)$

於是我們得到了左Kan擴展、右Kan擴展和組合函子 $- circ K$ 之間的之間的伴隨關係

$Lan_k - dashv - circ K dashv Ran_k -$

更具體的Kan擴展的伴隨關係圖如下所示：

Kan擴展的真正用處體現在當我們用end和coend來表示左/右Kan擴展的時候。當範疇C和D是local small範疇，範疇E是Set範疇時，我們可以用end和coend來表示左/右Kan擴展。

我們先從右Kan擴展開始，來看右Kan擴展是如何通過函子K來擴展函子F的domain的。首先，函子K是一個從範疇C到範疇D的嵌入函子，函子F是一個從範疇C到E的普通函子。對所有範疇C中的對象b，我們有函子K的像（範疇D的子範疇）中的對象K b，我們可以構造一個函子M將K b映射為範疇E中的M (K b)。因為函子M同時也映射範疇D中的態射g，因此我們可以將範疇D中且在函子K的像之外的對象a也映射到範疇E的對象M a。從所有這些函子M中我們可以得到一個特殊函子R，使得組合函子R . K具有終極泛性質，其到函子F的自然變換是所有組合函子M . K到函子F的自然變換構成的範疇的terminal對象。這個函子R就是右Kan擴展 $Ran_k F$ ，其將函子F的domain從範疇C擴展到整個範疇D。

下面我們就來構造這個特殊的右Kan擴展 $Ran_k F$ 。我們來看最自然的一個從範疇D到範疇E的函子Hom函子，給定一個範疇D中的對象a，我們可以得到一個協變Hom函子D(a, -)，作為一般的函子M。由前面提到的伴隨函子的同構關係，於是有

$E^C (D(a, -) circ K, F) cong E^D (D(a, -), Ran_k F)$

等號左側將D(a, -)和函子K的組合融合起來，等號右側根據米田引理，我們可以變換得到

$E^C (D(a, K -), F) cong Ran_k F a$

於是根據end的定義，我們可以將右Kan擴展用end表示為：

$Ran_k F a = int_{b} Set(D (a, k b), F b)$

通過類似的推導，我們可以將左Kan擴展用coend表示為：

$Lan_k F a = int^{b} D (k b, a) imes F b$

從實際的編程語言來看，用Haskell的代碼則可以有如下表示：

-- 左Kan擴展 data Lan k f a = forall b. Lan (k b -&> a) (f b)

-- 右Kan擴展 newtype Ran k f a = Ran { getRan :: forall b. (a -&> k b) -&> f b }

當函子k是Id函子時，我們就從Kan擴展得到了米田引理

-- 從左Kan擴展到Coyoneda data Lan_id f a = forall b. Lan_id (Id b -&> a) (f b) data Coyoneda f a = forall b. Coyoneda ( b -&> a) (f b)

-- 從右Kan擴展到Yoneda newtype Ran_id f a = Ran_id { getRan_id :: forall b. (a -&> Id b) -&> f b } newtype Yoneda f a = Yoneda { runYoneda :: forall b. (a -&> b) -&> f b }

當函子k是一個值為Unit的常量函子時，我們就從Kan擴展得到了極限（limit）和余極限（colimit）

-- 從左Kan擴展到余極限 data Lan_u f a = forall b. Lan_u (Const () b -&> a) (f b) data Colimit f a = forall b. Colimit (Const () b -&> a) (f b)

-- 從右Kan擴展到極限 newtype Ran_u f a = Ran_u { getRan_id :: forall b. (a -&> Const () b) -&> f b } newtype Lim f a = Lim { getLim :: forall b. (a -&> Const () b) -&> f b }

當函子k和f相同時，我們就從Kan擴展得到了density和codensity

-- 從左Kan擴展到codensity data Lan_f f a = forall b. Lan_f (f b -&> a) (f b) data Density k a = forall b. Density (k b -&> a) (k b)

-- 從右Kan擴展到codensity newtype Ran_f f a = Ran_f { getRan_f :: forall b. (a -&> f b) -&> f b } newtype Codensity m a = Codensity { runCodensity :: forall b. (a -&> m b) -&> m b }

其中Codensity m是一個單子（Monad），當m是一個自由單子時（Free Monad），Codensity m這個單子可以提高自由單子m的計算效率，是自由單子的優化形式。如同List的Dlist結構形式，DList可以極大的提高兩個List的++運算效率。

左Kan擴展還可以將任意一個類型構造子k變換為一個函子FreeF k，即得到一個基於k的自由函子。

-- 從左Kan擴展得到自由函子FreeF k data Lan_j k a = forall b. Lan_j (b -&> a) (k b) data FreeF k a = forall i. FMap (i -&> a) (k i)

instance (FreeF k) where fmap f (FMap g ki) = FMap (f . g) ki

Kan擴展和伴隨函子是有著緊密聯繫的，我們可以從Kan擴展得到伴隨函子。當函子F是一個Id函子時，Kan擴展和函子K組成了一對伴隨函子，其中左Kan擴展 $Lan_k Id$ 是函子K的右伴隨函子，右Kan擴展 $Ran_k Id$ 是函子K的左伴隨函子。