Tag: 依赖类型
依赖类型（在Swift中）拯救世界！
依赖类型（有时称为约束类型）使代码更安全，更易于使用。 使用从属类型是最有用和鲜为人知的编程概念之一。 我希望阅读完这篇文章后，您会觉得自己像个机械师，刚刚学会了如何加工自己的零件。 我将提供一些背景知识，然后向您展示依赖类型如何拯救世界。 什么是从属类型？ 在计算机科学和逻辑中， 从属类型是其定义取决于值的类型。 “整数对”是一种类型。 由于对值的依赖性，“第二对大于第一对的整数对”是从属类型。 —有关相关类型的维基百科文章 由于在Swift中基本类型和用户类型之间几乎没有区别，因此您很有可能已经使用了依赖类型。 考虑无符号整数类型： UInt UInt（正好：1）// 1 UInt（正好：1.0）// 1 UInt（正好：-1）//无 是否能够创建UInt取决于 a）您传递给初始化程序的值为正，并且 b）可解析为整数的值 使用UInt ，是在传达要处理的正整数的信息。 这是有帮助的。 是时候拯救世界了！ 假设我们的工作是为核电厂编写软件。² 如果反应堆过热，则可能引发气候事件并导致地球生命的尽头。 我们需要一个函数来冷却它： func addCoolantToNuclearPowerPlant（加仑：整数） 可能您可以用负数来称呼它： func doEmergencyStuff（）{ addCoolantToNuclearPowerPlant（加仑：-1000000） } 您已经排干了所有水，并引发了核灾难。 很容易看出为什么UInt类型将是此参数的更安全选择。 func addCoolantToNuclearPowerPlant（加仑：UInt） 现在，假设发电厂过热时至少需要一万加仑的冷却液。 在当前的定义中，我们不能偶然排放冷却剂，但是仍然可以将不足量的填料传递给冷却功能。 让我们通过在函数内添加检查来解决此问题，以免意外导致反应堆开销。 您会从检查中注意到，该参数的值存在隐式依赖性。 我们可以并且应该通过定义新的Dependent Type使隐式显式。 我们称它为Coolant 。 对Coolant此定义使用一个可失效的初始化程序来确保除非存在至少一万个Coolant否则它不会存在。 现在，我们可以重新定义冷却功能，如下所示。 现在，除了所需的最小Coolant剂量外，不可能用其他任何方法调用此功能。
协议编程，第2部分：依赖向量
在上一部分中，我们使用了协议以便对我们感兴趣的某些属性进行建模，并找到了适合该模型的多个示例（2D矢量，复数和线性函数）。 但是这些仅限于二维类型。 这太局限了，我们想操纵2个以上的维度。 这将需要确保我们正在操纵相同尺寸的值。 像第1部分一样，您可以在一个快速的游乐场中跟随，您可以在此处下载iPad或在Mac下载 免责声明 紧随其后的内容被视为“请勿在家中尝试”，纯粹是出于学术兴趣而非在Swift中的实际应用。 我们将使用协议来实现依赖类型。 N维向量，第一次尝试 为了更好地理解该问题，我们将尝试使用一个简单的数组来实现n维向量。 现有的大多数实现都使用数组来表示n维向量，但是它们有很大的缺陷： 不幸的是，我们无法实现NVector Additive ，因为它没有携带有关其大小的足够信息。 我们需要以某种方式对向量的大小进行编码。 这将使我们既可以重用代码，又可以避免出现以下错误： 为了解决此问题，我们将需要使用Size类型参数及其所持有的值的类型声明NVector结构。 我们的+函数看起来像这样： 由于第一个类型参数是数组的大小，因此我们强制要求两个加法向量的值相同。 事实证明，Swift已经拥有足够的技术来实现这种功能。 首先，我们将定义一个新的类型Nat以表示自然数 纳兹世界 “ Nat”是“自然数”的简写，自然数是从0到无穷大的整数的名称。 使用这两个定义来递归定义它们： 零是自然数。 自然数的任何后继也是自然数。 可以这样用Swift编写： 现在，我们可以定义几个自然数： 如您所见，数字是根据先前的数字递归定义的。 您还可以看到我们正在使用没有值的空enum声明。 这意味着Nat仅作为类型而不是value存在。 类型Three没有值 。 但是，我们可以创建一个函数，给定类型为Nat的函数可以返回它表示的Int值。 这样我们就可以从类型Three获得值3 （类型为Int ）。 方法如下： 1.首先我们需要一个协议，该协议将声明符合它的类型具有Int表示形式 该协议声明符合它的类型具有与之关联的静态Int值。 2.然后，我们需要为Zero类型和Succ类型实现此协议。 Zero直接实现： Zero由数字0表示。 3.最后，我们需要为Succ实现相同的协议。 Succ有点棘手，因为它是递归定义的。 因此，我们需要利用条件一致性来要求内部N类型也具有Int表示形式。 包装的类型N实际上是我们当前正在计算的类型的前身。 因此， Succ返回1加N的Int值，它是前身。 这样，类型Two返回1加上1整数值，后者本身返回1 + Zero整数值0 。 总计为1 […]
