gat*_*ado 10 type-theory covariance contravariance category-theory
我刚刚开始阅读有关类别理论的内容,如果有人能够解释CS逆变/协方差和类别理论之间的联系,我将非常感激.一些示例类别会是什么(即它们的对象/态射是什么？)？提前致谢？
从$ C $ A逆变算符为$ d $是完全相同的事情作为一个正常的(即,协变)函子从$ C $到$ d ^ {运算} $,其中$ d ^ {运算} $是相反类别的$ d $.因此,最好先了解相反的类别 - 然后你会自动理解逆变函子!
逆变函子并不常见于CS,尽管我可以想到两个例外:
您可能已经听说过子类型的逆转.虽然这在技术上是相同的术语,但连接确实很弱.在面向对象的编程中,类形成一个部分顺序; 每个偏序都是一个带有"二元同形"的类别 - 给定任意两个对象$ A $和$ B $,只有一个态射$ A \到B $ iff $ A\leq B $(注意方向;这个略微混乱的方向是我不会在这里解释的原因的标准),否则没有态射.
参数化类型,比如Scala的PartialFunction [-A,Unit]是从这个简单类别到它自己的仿函数......我们通常关注它们对对象所做的事情:给定一个类X,PartialFunction [X,Unit]也是一个类.但是,仿函数也保留了态射; 在这种情况下,如果我们有一个子类Dog of Animal,我们会有一个态射Dog $\to $ Animal,而functor会保留这个态射,给我们一个态射PartialFunction [Animal,Unit] $\to $ PartialFunction [Dog,单位],告诉我们PartialFunction [Animal,Unit]是PartialFunction [Dog,Unit]的子类.如果你考虑一下,这是有道理的:假设你有一种情况,你需要一个适用于狗的功能.适用于所有动物的功能肯定会在那里工作!
也就是说,使用全面的类别理论来谈论部分有序的集合是一个很大的过度杀伤力.
不常见,但实际上使用类别理论:考虑类别类型(Hask),其对象是Haskell编程语言的类型,并且态射$\tau_1\to\tau_2 $是$\tau_1 $ - >类型的函数$\$ tau_2.还有一个类别判断(Hask),其对象是打字判断列表$\tau_1\vdash\tau_2 $,其态射是一个列表上所有判断的证据,使用另一个列表上的判断作为假设.从类型(Hask)到判断(Hask)有一个仿函数,它将类型(Hask) - 同态$ f:A \到B $带到证明中
B |- Int
----------
......
----------
A |- Int
这是一个态射$(B\vdash Int)\到(A\vdash Int)$ - 注意方向的变化.基本上这就是说,如果你有一个将A变成B'a的函数,以及一个带有B类自由变量x的Int类型的表达式,那么你可以用"let x = fy in"包装它. .."并且得到一个仍然是Int类型的表达式,但其唯一的自由变量是$ A $类型,而不是$ B $.
在Microsoft Channel9的Going deep频道中有关于逆变/协方差的非常好的视频.你可以从这里开始: