👁 Image
数学 » 讨论
关于所有权和垃圾回收

有点神奇，原来gc 和 ownership也是遗忘-余自由伴随关系

U ⊣ !
(forget ⊣ cofree cocommutative comonoid)

Hom(U(B),A) ≅ Hom(B,!A)
i.e. 任何从 GC 类型到 Ownership 类型的态射，都能唯一地扩展为 GC 系统内部的结构保持态射。这正是 !A 的 cofree 性质。  (这里态射即为"编程语言"的函数。)

rust 的Arc Rc这类引用计数智能指针就像一个bang like的构造。