haskell - 余积与求和类型相同吗?

标签 haskell type-theory

我正在看this lecture from Bartosz Milewski他正在解释余积和求和类型。

在讲座中,他从一个转到另一个。

余积与求和类型相同吗?

最佳答案

基本上是的。副积原则上更一般,但这并不需要 就 Haskell 而言,您一定会关心。

余积不是总和类型的类别示例category of vector spaces以线性映射作为箭头。在这个类别中,不相交和类型没有多大意义,因为它们会给您两个不同的零向量元素。

相反,事实证明乘积类型(在线性代数中称为 direct sums ,但在实现方面它们是元组,而不是替代品)是此类别的余积:

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

(此类别的标准产品是 tensor product 。尽管可以忽略这一点并使用普通元组作为产品类型,即实际的余产品。我认为这与以下事实有关:任何希尔伯特空间都与其对偶空间同构。在我的 constrained-categories/linearmap-category 库中,乘积是元组,而 Mike Izbicki has not done this 在主题相似的 SubHask 库中。)请参阅德里克·埃尔金斯的评论。

<小时/> 我从数据意义上理解“和类型”,即具有标记联合结构的代数数据类型。

关于haskell - 余积与求和类型相同吗?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/43572970/

相关文章:

scala - 类型论中的种类与等级

haskell - 在 Haskell 中,是否有一种有效的方法来生成给定泛型(尤其是 monads)类型签名的函数?

haskell - 参数类型类名

coq - 任何额外的公理都能使 Coq Turing 完备吗?

haskell - 为什么我们需要 Sum 类型?

haskell - ghc - 命令行上的方括号?

haskell - 使用 Data.Comp.Unification 在 Haskell 中找到最通用的统一器(初学者问题)

ruby - hubris 无法安装 : Missing C libraries: ruby, ruby​​, ruby

haskell - 理解 Yesod Persistent TH 生成的代码

Haskell - 也许算术