Tag: Idris

Swift有一个漏洞—一种类型驱动的开发

我喜欢Swift的类型系统。 首先，当我从大约两年前的Objective-C切换到时，我被它的前身所采用的动态方法所宠坏了，以至于我感到非常不舒服。 在写了几个小时的Swift之后，我很累。 我不得不遵循它的规则并投身于类型系统，但是直到我停止与它抗争并遵循它的建议才不久。 我们建立了联系。 如今，我觉得我们是好朋友。 自从我对Swift有了更多经验以来，我对静态类型语言的评价一直在稳定增长。 我无法想象在没有静态分析和编译时间检查的情况下编写任何代码。 即使使用Python编写脚本，编写一些Bash实用程序，我也害怕在没有任何证据证明其正确性的情况下运行该东西。 最近，我偶然发现了埃德温·布雷迪（Edwin Brady）的一本奇妙的书— Idris的类型驱动开发 。 Edwin是纯函数式语言Idris的创建者。 在本书的第一章中，他解释了本书的名称不是巧合，而且确实是在流行测试驱动开发方法。 在TDD中，我们首先编写测试。 测试使我们能够设计数据流，而无需过多地关注实现细节。 Edwin的想法也是如此，但与其编写测试，我们首先编写接受和返回类型的函数。 Idris具有强大的字体系统，并且对Type-DD的重视不足为奇。 其销售功能是依赖类型 。 埃德温（Edwin）提出了一些非常简单的示例，在这些示例中正确使用类型可以使我们实现功能，而类型系统则使我们紧绷，因此我们不会做任何蠢事。 为了满足类型系统而不完成我们的实现，他引入了一个漏洞。 Hole是一个占位符，可以是您需要的任何类型，并且其类型由类型系统推断。 其目的是让您起草一个函数并快速跳转到下一个上下文并仅推迟其实现。 在编写Swift的一段时间里，我一直在使用一种非常相似的模式，在该模式中，我将使用fatalError来使编译器静音。 func numberOfChildren（inRooms rooms：[Room]）-> Int { 致命错误（） } 上面的代码编译，编译器不会抱怨，因为fatalError调用abort（）并且它知道程序的终止。 但是，如果我们可以满足编译器并继续运行该怎么办？ 我认为这是一个很好的主意，并尝试模仿Idris的孔概念。 我创建了AHole 。 这是一个非常简单的孔实现。 只有一个公共协议AHoleType和一个公共函数_hole_（） func _hole_ （文件：StaticString = #file， 行：UInt = #line）-> A { 打印（“ AHole：在文件\（file）的行\（line）上为类型\（A.self）使用孔”） 返回A.holed（） } 在存储库中，有第二个文件，该文件具有一些符合AHoleType的 […]

Swift中的总编程

编辑：在这个主题上，我接受了Corecursive播客的采访。 您可以在这里找到播客插曲，以及大量其他采访https://corecursive.com/007-total-programming-using-swift-with-andre-videla Swift是一种非常好的语言，因为它试图使程序员从一开始就做正确的事情。 它鼓励的好处之一就是整体性。 总计多少？ 总体程序是一种不会卡住，崩溃或陷入无限循环的程序。 它始终会在有限的时间内正确终止。 如果您的程序是完整程序且类型正确，则不会出现程序崩溃或卡住的情况¹。 程序有多种可能是不完全的。 这里有一些例子： 由于死锁或无限循环而陷入困境 边缘情况不予处理，将使程序崩溃 输入格式错误会使程序处于损坏状态 因此，总体上体现了“打字正确的程序不会出错”的短语²。 此属性在日常编程中非常有用，因为它可以减轻（但不能消除）对测试的需求，可以增加对代码的信心，并可以将代码库视为可信任的小块。 大多数正在使用的程序都不是完整的，例如，大多数程序旨在永久运行（Web服务器，移动应用程序，恶魔）。 但是，即使整个程序不是全部，将部分内容汇总也是很有用的。 尽管我将讨论“全部程序”，但实际上它们将是“全部功能”，因此我将可互换地使用两个词。 在这篇文章中，我将介绍空指针和未检查的异常如何针对整体性工作，然后，我将展示Swift如何通过解决这两个问题来鼓励整体性。 之后，我们将看到如何使用!默默地打破Swift的承诺! 运算符在不同的上下文中，并给出一些如何避免编写简单安全代码的示例! 。 尽管总体主题与非终止有着深深的联系，但我不会谈论它。 （注1：这一切都很好，但是Swift绝对不会检查您的程序是否完整。它只是鼓励几乎偶然地使程序完整的做法。Swift不检查整体性有很多原因，但最引人注目的是从数学上讲这是不可能的。 实际上，检查整体性意味着检查程序将始终终止（无无限循环），并终止于“良好”状态（无崩溃）。 终止问题通常被称为“停止问题”，该问题已被推广，并被艾伦·图灵（Alan Turing）使用其图灵机证明无法解决。 现有的编程语言具有有限的终止检查形式，例如Idris或Agda，但是给定了任意程序，他们无法决定它是否终止。 因此，他们将无法判断该程序是否完整。） （脚注2：此短语的原始来源 来自Milner的 这篇论文 。此声明的上下文是该特定类型系统存在健全性证明，因此，任何类型良好的表达都是声音。） 空引用在低级语言中找到其起源，程序员在该语言中操纵指向内存³中值的指针。 这种语言大量使用指针来访问内存中的地址，这些地址保存了程序中使用的所有数据结构。 例如，在链接列表中，通常将每个节点表示为一对指针：指向当前保存的值的指针和指向列表中下一个节点的指针。 此外，这也使得在列表末尾添加元素变得更加麻烦，因为您将不得不创建一个中间节点，将最后一个节点的值放在新的中间节点中，并使最后一个节点的前任指向新的中间节点，用新值替换最后一个节点中的值，使新的中间节点指向最后一个节点。 实现最后一个元素的另一种方法是使最后一个指针“悬空”而不指向任何东西。 例如，它可以指向未在内存中初始化的特殊保留值（例如0）。 由于所有这些“悬挂”指针都是相同的，因此我们可以轻松地对其进行比较。 因为我们经常使用此类指针，所以我们给它指定了一个名称，并将其称为null 。 现在，我们可以通过简单地将最终空指针替换为指向新的最后一个元素的指针，并将最后一个元素的尾部指针设置为null来在列表的末尾添加元素。 这使我们的LinkedList API更简单，更优雅，但代价是安全。 实际上，取消引用这样的指针通常会导致程序崩溃，因为您正在访问未初始化的内存。 空引用继承给其他编程语言（如Java，C＃和其他语言），以便以与C完全相同的方式表示诸如链表之类的数据结构。在这些语言中，指针不再是一等公民，但我们仍然可以拥有NullPointerException或尝试使用引用而没有意识到它为null NullReferenceException 。 （注3：空指针被Tony Hoare称为“十亿美元的错误”，他于1965年在Algol W中引入了空引用。我鼓励您在 https：//www.infoq 上听听他关于空引用的论述 。 […]