函子光学：Tannakian 重构与组合的艺术
Bartosz Milewski 探讨 Tannakian Reconstruction 作为冗余编码的价值，指出其核心优势在于支持组合。文章深入分析范畴论中函子类别与态射组合的规则，适合对函数式编程和数学基础感兴趣的读者。 
Bartosz Milewski 编程咖啡馆
Bartosz Milewski 的编程博客，关于范畴论、Haskell、并发和 C++。
评论
点赞
收藏Tannakian 重构
通过 Alice 和 Bob 隔着河辨认灯光的生动比喻，直观解释 Tannakian Reconstruction 定理的核心思想：如何通过对称性或表示来重构对象。这种将抽象代数几何概念具象化的方式，极大地降低了理解门槛，非常适合数学爱好者和技术人员阅读。
Tambara 结构：用范畴论理解 Haskell 光学
最初，我之所以对范畴论产生兴趣，是因为想弄清哈斯科普斯的原理。我对范·拉霍文的函子表示以及克梅特对塔姆巴拉模的运用感到困惑不已。通过用亚当斯引理来玩俄罗斯方块，我得以取得一些进展，不断攻克越来越深奥的课题。在一群研究人员和学生的支持下[…] 
作用范畴（Actegories）的 Haskell 实现与理论
Milewski 用 Haskell 代码形式化定义了 Actegory（作用范畴），将其作为理解 Optics（透镜、棱镜等）的理论基础。文章详细推导了 Monoidal Category 与 Actegory 在类型系统中的映射关系，包括结合律与自然变换的编码。适合有 Category Theory 基础且关注 Haskell 底层实现的开发者，提供了一手的形式化验证思路。
Tabulation 的麻烦事
Bartosz Milewski 深入探讨范畴论中的 profunctor 与 tabulation 概念，将其视为 proof-relevant relation。文章梳理了从函数图、关系图到 profunctor 的抽象演进，适合对高阶类型理论和范畴论基础感兴趣的开发者。 
Kan Extensions in Double Categories
Previously: Kan extensions in Haskell. In a double category that is also a proarrow equipment, we have the ability to bend arrows. In particular, in the definition of the counit of the right Kan exten...
Kan Extensions in Haskell
Previously: Tabulation Tribulations. If you think of functor composition as a form of multiplication, Kan extensions are an attempt to construct inverses of this multiplication. But unlike multiplicat...
Bending, Yanking, and Cartesian Squares in Double Categories
Previously: Profunctor Equipment in Haskell. The major advantage of string diagrams is that they provide surprisingly natural language for complex diagram manipulations. The fact that two traditional ...
Profunctor Equipment in Haskell
Previously: Profunctor Equipment. To make things more palatable for programmers, I decided to provide a toy implementation of some of the equipments in Haskell. The advantage of this encoding is that ...
Profunctor Equipment
The fundamental premise of category theory is that it’s possible to fully capture the nature of objects by describing their interactions with other objects of the same type. Those interactions are enc...
The Axiom of Univalence
Previously: Modeling Identity Types. On first viewing, the identity type seems odd. Does it make sense to replace the traditional yes/no equality predicate with an elaborate type of equality proofs? I...