节能设备

它能够是另一个态射的始点或起点

作者:admin 来源: 本站原创 时间: 2019-11-27 浏览次数:

  Haskell 的多态函数取 C++ 的泛型函数之间存正在很大的区别,次要表现为函数的实现体例以及类型查抄体例上。正在 Haskell 中,一个多态函数必需对于所有类型是独一的。一个公式必需合用于所有的类型。这就是所谓的参数化多态(Parametric polymorphism)。

  我们曾经会商过,函子能够正在维持范围布局的前提下实现范围之间的映照。函子能够将一个范围嵌入到另一个范围,它也能够让多个范围坍缩为一个范围且不会范围的布局。凭仗函子,我们能够正在一个范围之内建立另一个范围。源范围可视为方针范围的部门布局的模子或蓝图。

  我们还控制了函数类型,它们对于它们的前往类型而言具有着函子性。我们能够利用它们来构制函子(例如Reader函子),易发游戏斗地主,并为这些函子构制天然变换——更高阶的函数。

  再一次沿用 Mac Lane 的记法,我利用小圆圈来暗示横向复合。正在它呈现的上,你也可能看到的是星号。

  故事方才说了一半。函子所映照的不止是对象,它们也能映照态射,天然变换该当若何看待这种映照?谜底是,态射的映照是固定的——正在F取G之间的任何一个天然变换下,F f必需变换成G f。也就是说,两个函子对态射所构成的映照会完全取之相适的天然变换的定义。来考虑正在范围C中的两个对象a取b之间的态射f,它被映照为范围D中的两个态射F f取G f:

  当函子之一是微不脚道的Const函子的时候,会发生一件风趣的事。一个以Const函子为始点或起点的天然变换,看上去就像一个函数,它即面向它的前往类型多态,也面向它的参数类型多态。

  往常,我们从C中的一个对象a起头。它为两个D中的对象:F a取F a。还有一个态射,α的一个分量,毗连这两个对象:

  你可能还记得,为了构制一个指数,需要起首定义积。正在Cat里,定义积相当容易,由于小范围是对象的调集,而我们又晓得如何定义调集的笛卡尔积。因而,积范围C × D里的一个对象,是两个对象形成的序对(c, d),一个来自C,一个来自D。雷同地,正在如许的序对(c, d)取(c, d)之间的态射是一个态射序对(f, g),此中f :: c - c,g :: d - d。因为这些态射序对由C取D中态射构成,因而老是会有一个由C和D中的恒等态射形成的序对。长话短说,Cat是一个完全的笛卡尔闭范围,对于肆意一对范围(译注:例如C取D),它里面存正在着响应的指数对象D^C。因为我说过,Cat里的对象是范围,因而D^C是范围,它就是C取D之间的函子范围。

  之前我提到过,正在 Haskell 里,能够将函子视为泛型容器。我们能够继续这个类比,将天然变换视为一种沉组方式,即将一个容器里的工具取出来放到另一个容器里。我们不会触碰这些工具:不点窜,也不创制。我们只是将它们(或它们的一部门)复制到新的容器里,正在这个过程中有时候会对它们做几回乘法。

  它是面向a的函数多态化。它能够不受地感化于肆意一品种型a,因而它是一个参数化多态的例子。从而,它就是两个函子之间的一个天然变换。不外,现正在这只是我们正在自命不凡,下面来验证它能否合适天然性前提。

  于是,天然性前提就是,起首它不关怀我们是先通过fmap点窜这些工具,然后再将它们放到新容器里,仍是先把它们放到新容器里再用合用于这个容器的fmap去点窜它们。沉组取fmap,它们是正交的,『你走你的阳关道,我过我的独木桥』。

  这是对这本书第一部门的总结。我们曾经领会了范围论的根基术语。你可能会如许认为:对象取范围是名词;态射、函子以及天然变换是动词。态射毗连了对象,函子毗连了范围,天然变换毗连了函子。

  例如,考虑有时会被忽略的仅有一个值()的 unit 类型()。函子Reader ()接管任何一品种型a,将它射入函数类型() - a。这些函数能够从调集a中拮取一个元素。这些函数的数量取a中元素的数量一样多。现正在,来看一下从这种函子到Maybe函子的天然变换:

  有一个范围化的经验:每次拿到复应时,该当去找一个范围。我们有天然变换的竖向复合,它是函子范围的一部门。那么,横向复合呢?它身居什么范围里?

  天然性前提很是有用。例如,若是态射F f是可逆的,天然性决定了以 α_a 形式暗示的α_b。通过f,基于天然性前提可将α_a变换为:

  请记住,这是由a参数化的一个函数族。这是 Haskell 语法简练性的又一个示例。正在 C++ 中,取之雷同的构制要麻烦一些:

  现正在,我们有了函子之间的映照——天然变换——因而很天然地就会想到,函子能否可以或许构成范围?没错,它们能够。对于每对范围而言,仅存正在一个函子范围。正在这个范围里,对象是从 C 到 D 的函子,而态射就是这些函子之间的天然变换。

  现正在,我们便有了两个从F a到G b的路子。为了这两种路子等价,必需引入天然性前提(Naturality condition):

  从分量的角度来看天然变换,您能够认为它将对象映照为态射。可是,从天然性前提的角度来看,你也能够认为它将态射映照为四方形的互换图(Commuting squares)—— C 中的每个态射都被映照为 D 中的一个互换图。

  寻找一个以Const函子为始点的参数化多态函数有点难,由于这需要创制一个值出来。我们所能想到的最好的法子是:

  我们必需得定义两个天然变换的复合,不外,这相当容易。天然变换的分量是态射,而我们晓得如何实现态射的复合。

  因为正在统一范围中的对象映照该当不会离开该范围,并且我们不想人工成立F a取G a的联系,因而很天然的考虑利用既有的联系——所谓的态射。天然变换素质上是若何拔取态射:对于肆意对象 $a$,天然变换就是拔取一个从F a到G a的态射。若是将一个天然变换称为α,那么这个态射就被称为正在a上的α分量(Component ofαata),记做α_a:

  天然性前提之所以正在 Haskell 里会从动被满脚,这是『免费的』的天然成果。正在 Haskell 里,参数化多态,将其用于定义天然变换,会引入很是强的前提——一个公式顺应所有类型。这些前提会变成面向这些函数的方程一样的。对于可以或许对函子进行变换的函数,免费的是天然性前提。(做者注:你能够阅读我写的另一篇文章《Parametricity: Money for Nothing and Theorems for Free》,会让你对这些免费的可以或许领会得更多一些。)

  我们用 Hom-范围——函子范围D^C来取代范围C取D之间的 Hom-集。我们有常规的函子复合:来自D^C的函子F取来自E^D的函子G复合,能够获得来自E^C的函子G ∘ F。可是,正在每个 Hom-范围内部,也存正在着复合——函子之间天然变换或 2-态射的竖向复合。

  范围 C 取 D 之间的函子范围记为Fun(C, D)或[C, D],有时也写成D^C。最初这种记法暗示了可将函子范围本身视为其他范围里的一个函数对象(指数)。现实上是如许吗?

  这个更丰满的布局是 2-范围的一个例子。2 -范围是一个广义的范围,此中,除了对象和态射(这里该当叫它 1-态射)之外,还有 2-态射,它就是态射之间的态射。

  问题处理了,我们现正在近不雅一下Cat。按照定义,Cat里的肆意 Hom-集都是函子调集。可是,就像我们见识过的,两个对象之间的函子有着比调集更丰满的布局。它们构成一个范围,以天然变换为态射。因为正在Cat里,函子被认为是态射,天然变换就是态射之间的态射。

  为了构制一个天然变换,我们从一个对象起头,也就是一品种型,设为a。一个函子F,能够将a映照为类型F a。另一个函子G,能够将a映照为G a。正在a上的天然变换alpha的分量是一个从F a到G a的函数。利用用伪 Haskell 代码,可将其暗示为:

  现正在我们手里有α取β,可不克不及够定义一个从G ∘ F到G’∘ F’的天然变换?我们画个草图看看:

  对于范围C取D之间的两个函子F取G,若是我们只关心C中的一个对象a,它被映照为D中的两个对象:F a取G a,那么该当存正在一个函子映照,它能够将F a映照为G a。

  函子,将对象映照为对象,因而我们将其做为类型构制子,或者做为一种参数化的类型。函子,也能将态射映照为态射,因而它也是高阶函数——fmap。有一些简单的函子,例如Const、积以及余积,它们能够发生大量的代数数据类型。函数类型也具有函子性,协变性取逆变性,它们能够用于扩充代数数据类型。

  当前还会有更多的记法。正在这个从侧面看Cat的新注释里,从一个对象到另一个对象存正在两种方式:利用函子或利用天然变换。然而,我们能够将函子箭头从头注释为一种特殊的天然变换:恒等天然变换感化于这个函子。因而,你将会经常碰到这种记号:

  这不是一个函子,由于统一类型的a呈现正在负(逆变)位取正(协变)位上。对于这品种型,fmap或contramap都无法实现。因而,函数签名:

  此中,F是从D到E的函子,而α是从C到D的两个函子之间的天然变换。由于你不克不及将用一个天然变换去取一个函子进行复合,所以这个记号需要解读为恒等天然变换1_F位于α之后的横向复合。

  译注:做者后面还有两部门内容,可是我决定只翻译到这里。别的,这篇文章的原文下面的评论区,一位网名「benjaminy」的人的评论,也值得思虑。别的,做者正在这第一部门所讲述的这些范围论概念,曾经脚以让你正在必然程度上领会票据——自函子范围上的一个幺半群。

  译注:α_a暗示 $\alpha_a$。用 HTML 标识表记标帜来暗示,就是αsuba/sub。因为很多号称支撑 Markdown 文档格局的网坐,它们不支撑正在 Markdown 里利用 HTML 标识表记标帜。虽然这些网坐有一些也支撑 TeX 公式,可是又没法正在代码排版中嵌入 TeX 公式。因而,我不得晦气用下划线来暗示公式里的下标。鄙人文,我也会利用^来暗示上标,趁便说一句,我对现正在几乎任何一个由用户自行发布内容的网坐都不合错误劲。

  我们也有一个从C到C的恒等箭头。它是C上的恒等函子本身的恒等天然变换。留意,横向复合的恒等也是竖向复合的恒等,可是反过来却不是。

  说一说记法。取 Saunders Mac Lane 一样,我利用小圆点(dot)来暗示各类天然变换的复合。问题是存正在两种天然变换的复合体例。一种叫竖向复合,由于正在示企图里,函子凡是是往下堆砌的。竖向复合对于定义函子范围很主要。下面我简短引见一下横向复合。

  将一个范围嵌入到另一个范围可能有很多种体例。有时这些体例是等价的,有时它们不等价。你能够将整个的范围坍缩为另一个范围中的一个对象,也能够将一个范围中的每个对象映照为另一个范围中分歧的对象,将前者中的每个态射映照为后者中的分歧的态射。同样的设法能够有多种分歧体例的实现。天然变换能够帮帮我们对比这些实现。天然变换是函子之间的映照——能够连结函子性质不变的特殊映照。

  两个函子之间的参数化多态函数(包罗Const函子这种鸿沟环境)必定是天然变换。由于所有的尺度代数数据类型都是函子,正在这些类型之间的任何一个多态函数都是天然变换。

  看一下我们到现正在为止所建立的笼统层。我们从一个范围起头,它由一组对象取态射形成。范围本身(或严酷地说是小范围,它们的对象构成调集)是更高层的范围Cat里的对象。正在Cat里,态射是函子。Cat里的 Hom-集是函子形成的调集。例如,Cat(C,D)是范围 C 取 D 之间的函子调集。

  之前讲过函子(更切当的说,是自函子)正在编程中所饰演的脚色。它们相当于类型构制子——将类型映照为类型。不外,函子也能将函数映照为函数,这种映照是通过一个高阶函数fmap(正在 C++ 中则是transform,then之类的行为)。

  还有一个分歧寻常的函子,我们之前曾经见过它了,它正在 Yoneda 引理中饰演了主要的脚色。这个函子就是Reader函子。下面我用newtype来沉写一下它的定义:

  很多多少态射。我们的方针是寻找从G (F a)到G(Fa)的态射。一个候选解是毗连两个函子G ∘ F取G’∘ F’的天然变换的分量。现实上,从

  C++ 默认供给的是特设多态(Ad hoc polymorphism),这意味着模板不必然涵盖所有类型。一份模板能否合用于某种给定的类型需要正在实例化时方能确定,彼时,编译器会用一种具体的类型来替代模板的类型参数。类型检测是以推导的形式实现的,编译器经常会给出难以理解的错误消息。

  留意,我们不克不及对这两个天然变换使用竖向复合,由于α的起点取β的始点不沉合。现实上,它们别离属于两个分歧的函子范围D^C取E^D。不外,我们可以或许复合函子F取G,由于F的起点取G的起点沉合——它就是范围D。函子G’∘ F’取G ∘ F之间有什么关系呢?

  函子F取G从动满脚天然性前提。这里,我们再回到范围论的概念(f是一个函数,f::a-b):

  最初,天然变换可用于定义函子的同构。若是说两个函子是天然同构的,差不多是正在是说它们是不异的函子。天然同构是以天然变换的形式定义的,这种天然变换的各个分量都是同构的(可逆的态射)。

  正在 C++ 中,还有一种函数沉载取模板特化机制,通过这种机制可认为分歧的类型定义函数的分歧版本。Haskell 也有雷同的机制,即类型类(Type class)取类型族(Type mily)。

  这仍然不是实正的 Haskell 代码——正在代码中无法暗示函数等式——不外,上式是恒等的,法式员正在等式推导中能够利用这个公式,此外,编译器也能够操纵这个公式对代码进行优化。

  还有,现实上按照 Yoneda 引理的说法,这些取Maybe ()类型的两个元素相符,即Nothing取Just ()。呆会儿我们就会再回到 Yoneda 引理上来——以上的说法有些不庄重。

  天然变换的这一性质能够让良多范围便于构制,这些范围往往包含着这类的互换图。正在准确选择函子的环境下,大量的互换前提都可以或许转换为天然性前提。当前正在讲到极限、上极限(Colimit)以及陪伴(Adjunction)时会给出一些例子。

  现正在,我们把留意力放正在Cat里的两个对象上,即范围C取D。存正在着由天然变换形成的调集,这些天然变换交往于毗连C取D的函子之间。这些天然变换就是我们从C到D的新箭头。同理,也有一些天然变换交往于毗连D取E的函子之间的天然变换,我们将它们视从D到E的新箭头。横向复合,就是这些箭头的复合。

  此中f是肆意函子,这个函数不是天然变换。风趣的是,存正在着一种广义的天然变换,叫做双天然变换,它们可以或许处置这些环境。正在我们会商端(End)的时候会碰到它们。

  函子范围[C, D]也是两个范围之间的函子调集(加上天然变换为态射)。它里面的对象也是Cat(C,D)里的工具。此外,函子范围是范围,它本身必需得是Cat里面的对象之一(也就是说,两个小范围之间的函子范围本身也很小)。一个范围里的 Hom-集取统一个范围里的对象之间存正在联系。这种环境就像我们正在上一节里所看到的指数形式的对象。现正在来看一下,Cat里若何构制后者。

  要获得谜底,需要从侧面来看Cat。不要将天然变换当作函子之间的箭头,而是将它们当作范围之间的箭头。一个天然变换位于两个范围之间,而这两个范围本来是由这个天然变换所变换的函子毗连的。我们能够认为这个天然变换毗连着这两个范围。

  不外,对于参数类型而言,函数类型不具备协变性,它们具备逆变性。当然,逆变函子就是相反范围中的协变函子。正在范围意义上,两个逆变函子之间的多态函数仍然可视为天然变换,除了它们只能感化于 Haskell 类型所形成的两个相反的范围里的函子。

  来看一下 Haskell 里的天然变换。起首来看列表取Maybe这两种函子之间的天然变换,它的功能是,当且仅当列表非空时前往列表的首元素:

  函子正在函子范围里能够视为对象。如许,它们就变成了态射的始点取起点,于是有了天然变换。天然变换就是特定形式的多态函数。

  我们适才曾经定义了从G ∘ F到G’∘ F’的天然变换的一个分量。倘若你脚够有耐心,那么这个变换的天然性证明相当曲不雅。

  因为这两个函子不具备协变性,它并非Hask范围中的天然变换。不外,因为它们都具备逆变性,所以它们满脚『相反的』天然性前提:

  正在此,我援用 Saunders Mac Lane 的说法:读者可能感觉绘制显而易见的示企图要比去证明它更风趣。

  可是我们曾经看到了,一个笼统层上的一个动做,鄙人一个笼统条理上就变成了一个对象。态射的调集变成了函数对象。做为对象,它能够是另一个态射的始点或起点。这就是高阶函数背后的思惟。

  正在 Haskell 中,函子G感化于一个态射f是通过fmap实现的。可利用 Haskell 伪码将上述概念暗示为:

  若是两个对象之间存正在多个可逆的态射,上述变换也都成立。虽然态射凡是是不成逆的,可是我想说的是两个函子之间的天然变换并非必然存正在。因而,取天然变换相关的函子的多寡,可正在很大程度上这些函子所的范围的布局。正在讲极限取 Yoneda 时,我会给出一些例子。

  对于每品种型e,都能够定义从Reader e到任何其他函子的天然变换家族。当前会看到,这个家族的老是取f e的元素壹壹对应(Yoneda 引理)。