理解产品和余积图表的内容

3

这是关于编程的一些内容解释,链接为https://www.youtube.com/watch?v=V10hzjgoklA。从15分钟开始。 - Bogdan Vakulenko
我冒昧地将“draw”这个词(我想你指的是“绘画”)替换为“diagram”这个术语,在范畴论中,这些图片就是被称为“diagram”。 - dfeuer
3个回答

6
据我所知,这些图表的想法是给你:
  • 类型ABZ
  • 指定类型的函数fg(在第一个图中,f :: Z -> Ag :: Z -> B,在第二个图中箭头会“反过来”,因此f :: A -> Zg :: B -> Z)。

现在我将集中讨论第一个图,这样我就不必用稍微有些变化的方式说两遍了。

无论如何,根据以上内容,想法就是有一种类型M以及函数fst :: M -> Asnd :: M -> Bh :: Z -> M,使得,正如数学家所说的那样,图表“交换”。这只是表示,在给定图表中的任意两点上,如果您按任何方式从其中一个点沿着箭头走到另一个点,结果的函数都是相同的。即,ffst . h相同,而gsnd . h相同。

很容易看出,无论Z是什么,都可以使用配对类型(A, B)及通常的Haskell函数fstsnd实现这一点——再加上适当的h选择,即:

h z = (f z, g z)

这两个要求在图表中形成交换所必须满足的特定条件,是很容易得到满足的。

这是有关图表的基本解释。但您可能会对其中Z的角色略感困惑。这是因为实际上陈述的是相当强的内容。也就是说,给定ABfg,存在一个M以及函数fstsnd,可以为任何类型Z(这意味着还需要提供一个函数h::Z->M)构造出这样的图表。并且进一步说明只有一种函数h能够满足所需的属性。

一旦您玩弄它并理解各种要求,就很清楚了,配对(A,B)以及其他与之同构的类型(基本上意味着定义了data MyPair a b = MyPair a bMyPair A B)是唯一满足此条件的东西。而且还有其他类型的M也可以起作用,但会产生不同的h,例如:将M作为三元组(A, B, Int),其中fstsnd分别从第一个和第二个组件提取(在数学术语中称为“投影”),然后对于任何您要命名的x :: Inth z = (f z, g z, x)都是这样的一个函数。

距我学习数学,特别是范畴论已经太长时间了,无法证明(A,B)是唯一满足我们所讨论的“通用性质”的类型。但可以放心地说它确实是唯一的,而且您真的不需要理解这个(或者实际上任何内容)才能在Haskell中使用积类型和和类型。

第二个图表与第一个图表基本相同,只是所有箭头都被反转了。在这种情况下,AB的“余积”或“和”M实际上是Either a b(或其等价物),并且定义为:h::M->Z将被定义为:

h (Left a) = f a
h (Right b) = g b

5

一个产品(在Haskell中为Tuple)是一个具有两个投影的对象。这些函数将产品投影到它们各自的因子fstsnd

相反,一个余积(在Haskell中为Either)是一个具有两个注入的对象。这些函数将单独的和式leftsrights 注入到总和中。

需要注意的是,产品和余积都需要满足一种通用属性。我建议参考Bartosz Milewski的介绍以及他的讲座


4
这些图表没有传达的一件事是哪些部分是输入,哪些部分是输出。我将从产品开始,并特别注意哪些东西是交给您的,哪些必须由您自己完成。
因此,一个产品表示:
1. 您给我两个对象A和B。 2. 我给您一个新对象M和两个箭头fst:M->A和snd:M->B。 3. 您给我一个对象Z和两个箭头f:Z->A和g:Z->B。 4. 我给您一个箭头h:Z->M,使图表成为圆形(...这个箭头是由到目前为止所做的选择唯一确定的)。
我们经常假装有一个类别Hask,其中对象是具体(单态)类型,并且箭头是适当类型的Haskell函数。让我们看看上面的协议如何运作,并证明Haskell的在Hask中是一个产品。
  1. You give me two objects (types), A=a and B=b.
  2. I must produce an object (type) and two arrows (functions). I pick M=Pair a b. Then I must write functions of type Pair a b -> a (for the arrow fst : M -> A) and Pair a b -> b (for the arrow snd : M -> B). I choose:

    fst :: Pair a b -> a
    fst (P a b) = a
    
    snd :: Pair a b -> b
    snd (P a b) = b
    
  3. You give me an object (type) Z=z and two arrows (functions); f will have type z -> a and g will have type z -> b.
  4. I must produce a function h of type z -> Pair a b. I choose:

    h = \z -> P (f z) (g z)
    

    This h is required to make the diagram commute. This means that any two paths through the diagram that begin and end at the same object should be equal. For the diagrams given, that means we must show that it satisfies two equations:

    f = fst . h
    g = snd . h
    

    I'll prove the first; the second is similar.

    fst . h
    = { definition of h }
    fst . (\z -> P (f z) (g z))
    = { definition of (.) }
    \v -> fst ((\z -> P (f z) (g z)) v)
    = { beta reduction }
    \v -> fst (P (f v) (g v))
    = { definition of fst }
    \v -> f v
    = { eta reduction }
    f
    

    As required.

协和产品的情况类似,但需要稍微调整下面描述的协议:
  1. 您给我两个对象A和B。
  2. 我给你一个新对象W,并且有两个箭头:左箭头:A -> W和右箭头:B -> W。
  3. 您给我一个对象Z和箭头f:A -> Z和g:A -> Z。
  4. 我给你一个箭头h:W -> Z,使图表对应(...这个箭头是由到目前为止所做的选择唯一确定的)。
很容易根据上述关于乘积和Pair的讨论来适应余乘积和data Copair a b = L a | R b。

网页内容由stack overflow 提供, 点击上面的
可以查看英文原文,
原文链接