我弄错的地方:类型

2020-09-27 16:28:33

假定受众:关心实际学习的人(在本例中,尤其是软件开发人员)。而且,我的妻子非常喜欢听我说,我错了。“😂。

认知状态:这些都是我目前认为我错了的地方。但我已经改变主意一次了,所以…。

至少在我的经验中,人们讨论他们过去错误的事情是相当罕见的。甚至当我们发帖子的时候,我也在想这个新东西!“。我们很少确切地说出我们改变主意的是什么。因此,在这个系列 - 中,作为我在这个网站 - 上公开学习建模的持续练习的一部分,我将深入挖掘目前我认为自己完全错了的事情。主题将从软件(就像今天一样)到神学,以及脑海中浮现的任何其他东西!

如果你在六七年前跟我谈过编程语言中的类型,你很快就会知道我不是一个迷。前几年我一直在Fortran和C中工作,外加了一点Java,我对类型的经验是它们增加了大量的管理费用,而且根本不会为自己买单。我使用的是Python和JavaScript,不会错过。所有的,即使在相当复杂的系统中也是如此。我一度告诉一位同事,我认为类型基本上一文不值。

2015年,这一切都改变了。那年春天,我在飞机上读到了“也许哈斯克尔”,大约两个月后,我遇到了铁锈,突然之间,我对类型有了非常不同的看法。毫不夸张地说,在这两个月的时间里,我职业生涯的整个轨迹发生了变化。从那时起,我运行了一个关于Rust的播客,其中包括大量关于类型理论的讨论,帮助引导整个子社区使用另一种类型编程语言(这现在是我日常工作的一部分),并撰写了大量关于类型及其如何提供帮助的搞笑文章。

我理解为什么从2012年 - 2014年开始我认为类型一文不值。事实上,对于到那时为止我已经使用过的特定语言,我仍然认为这些类型并不真正值得。但我对更一般的类型系统有了很大的改变。一些类型系统可以在您可以编写的程序类型上产生实质性的差异,并且您从它们中获得的价值程度与您为获得该价值所付出的努力相比要高得多。

我不重视的类型系统和我现在使用 - 的类型系统之间的关键区别是:所有类型系统一文不值的想法和我目前认为一个好的类型系统等同于黄金 - 的观点之间的关键区别是:

类型推断:因为必须写出每种类型,无论多么明显,都是难以置信的浪费时间。人我=新人();太荒谬了。Let me=new Person();可能看起来是一个小小的改进,但是扩展到整个程序主体并推广到各种上下文意味着类型注释成为您使用的工具,因为它们是用于与他人通信的有用 - ,或者用于以特定方式约束程序的 - ,而不仅仅是因为编译器对您大喊大叫它应该非常清楚的事情。

SUM/TAG联合类型:因为我们在软件中解决的很多问题都归结为定义良好的选项:A、B或C,以及A、B和C中每一个对应的数据的离散选项。很多问题也不适合这个领域,但是足够了,缺少一个工具来表达它会让人感到痛苦。事实上,多年来我一直在尝试自己用C和Python语言构建SUM类型的方法,直到最终发现这个想法已经存在,围绕它的工具都是非常棒的…。用其他语言写的。具有对SUM类型的一流支持的语言也会对这些类型进行详尽的检查,这一事实更是锦上添花。这意味着我最终可以告诉电脑我的意思,让它检查我的 - ,也意味着如果我后来改变主意,我可以告诉电脑,让它告诉我需要更新假设的每个地方。

健全性:我厌倦了NULL和NullPointerException,并且unfined不是函数,TypeError:类型为';NoneType';的对象没有len()。但至少在非类型化语言中,我只能将这些错误归咎于我自己。让它们使用具有类型的语言是非常令人恼火的:为什么编译器不能告诉我我遗漏了一个可能为空的大小写?这个问题很普遍:无论我在类型上做了多少工作,编译器都无法告诉我我的程序是否真的遵循了我希望它遵循的规则。健康改变了这一切。这并不意味着我没有逻辑缺陷。(在一般情况下,没有什么能做到这一点!)。不过,这确实意味着经过类型检查的程序不会以类型检查器说不应该的方式崩溃。

这三个不同让我可以把文字变成思考的工具,也就是与其他程序员和计算机沟通的手段。它让我指定我想要保持为真的不变量,确保编译器会告诉我它们是否真的保持为真,并保证编译器不会只是在这方面对我撒谎。

类型并不完美。他们仍然有权衡之处。有些类型系统不值得这么做。但五年前,我改变了对类型系统总体价值的看法,因为我了解了以前不知道的类型系统。而且,至关重要的是,这教会了我在编程语言和软件开发中对思想的价值不那么教条。如果聪明人看到了一些东西的价值,而我没有,那很可能是我错过了一些东西,有什么东西可以从他们身上学到!