联产品与总和类型相同吗？

Question

我正在观看Bartosz Milewski的这个讲座,他正在解释副产品和总和类型.

在演讲中,他从一个到另一个.

副产品与总和类型相同吗？

Answer 1

基本上,是的.副产品原则上更为通用,但就Haskell而言,这并不一定与您有关.

联产品不是和类型^†的类别的示例是具有线性映射作为箭头的向量空间的类别.在这个类别中,不相交和类型没有多大意义,因为它们会给你两个不同的零向量元素.

相反,事实证明,产品类型(在线性代数中称为直接和,但实现方面,它们是元组,而不是替代品)是此类别的副产品:

type LFun v w = v -> w

initial :: VectorSpace w => LFun () w
initial () = zeroV

(+++) :: VectorSpace w => LFun u w -> LFun v w -> LFun (u,v) w
(f+++g) (u,v) = f u ^+^ g v

(该分类标准的产品是那么的张量积.虽然它可能忽略了这一点,并使用普通的元组作为产品类型,即实际副产品.我觉得这做的事实,任何希尔伯特空间是同构于它的双重空间.在我的constrained-categories/linearmap-category库中,产品是元组,而Mike Izbicki 没有在局部相似的SubHask库中完成此操作.)_{请参阅Derek Elkins的评论.}

^† _{我理解数据意义上的"和类型",即作为具有标记联合结构的代数数据类型.}