除了安全之外,还有强大打字的好处吗？

Question

在Haskell社区中,我们正在慢慢添加依赖类型的功能.依赖类型是一种高级类型功能,类型可以依赖于值.像Agda和Idris这样的语言已经拥有它们.它似乎是一个非常高级的功能,需要一个高级类型系统,直到你意识到python 已经有依赖类型从一开始就具有依赖类型的动态类型版本,可能是也可能不是实际的依赖类型.

对于函数式编程语言中的大多数程序,无论打字有多高级,都有一种方法可以将其作为无类型lambda演算术语重复出现.这是因为打字只会删除程序,而不会启用新程序.

强大的打字赢得了我们的安全.运行时发生的错误类别在运行时不再发生.这种安全性非常好.除了这种安全性之外,强力打字能带给你什么？

除安全性之外,强类型系统还有其他好处吗？

(请注意,我并不是说强打字是没有价值的.安全本身就是一个巨大的好处.我只是想知道是否还有额外的好处.)

Answer 1

首先,我们需要谈谈简单类型的lambda演算的历史.

简单类型的lambda演算有两个历史发展.

• 当Alonzo Church描述lambda演算时,这些类型作为术语的含义/操作行为的一部分被烘焙.

• 当Haskell Curry描述lambda演算时,类型是对术语的注释.

因此,我们有lambda演算教堂和lambda演算la Curry.有关更多信息,请参阅https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus#Intrinsic_vs._extrinsic_interpretations.

具有讽刺意味的是,以库里命名的Haskell语言基于一个lambda演算教堂!

这意味着类型不仅仅是为您排除糟糕程序的注释.他们也可以"做事".这种类型不会擦除而不留下残留物.

这表现在Haskell的类型类概念中,这就是为什么Haskell是一种教会语言的原因.

在Haskell中,当我创建一个函数时

sort :: Ord a => [a] -> [a]

我们将一个对象或字典Ord a作为第一个参数传递.

但是你并没有被迫在代码中探讨自己的论点,编译器的工作就是构建它并使用它.

instance Ord Char
instance Ord Int
instance Ord a => Ord [a]

因此,如果你去对字符串列表进行排序,这些字符串本身是字符列表,那么这将通过将Ord Char实例传递给Ord a => Ord [a]的实例来获得Ord [Char]来构建字典],与Ord String相同,然后您可以对字符串列表进行排序.

sort上面调用,比手动构建a LexicographicComparator<List<Char>>通过将其传递IComparator<Char>给它的构造函数并使用额外的第二个参数调用函数要简单得多,如果我要比较sort在Haskell 中调用这样的函数到在C#或Java中调用它的复杂性.

这向我们展示了使用类型进行编程可能会明显减少冗长,因为像implicits和类型类这样的机制可以在类型检查期间推断出程序的大部分代码.

在更简单的基础上,甚至参数的大小也可以取决于类型,除非你想支付相当大的成本来装箱你的语言中的所有东西,以便它具有同质的表示.

这向我们展示了使用类型编程可以显着提高效率,因为它可以使用专用表示,而不是在代码中的任何地方支付盒装结构.一个int不能只是一个机器整数,因为它必须看起来像系统中的其他所有东西.如果您愿意在运行时放弃一个数量级或更高性能,那么这对您来说可能无关紧要.

最后,一旦我们为我们提供类型"做事",考虑仅仅安全提供的重构效益通常是有益的.

如果我重构剩下的较小代码集,它将为我重写所有类型类管道.它将找出它可以重写代码以取消更多参数的新方法.我不会卡住手工详细说明所有这些东西,我可以将这些平凡的任务留给类型检查器.

但即使我确实改变了类型,我也可以毫不犹豫地调整参数,使编译器很可能发现我的错误.类型为您提供"自由定理",就像整类此类错误的单元测试一样.

另一方面,一旦我用Python这样的语言锁定API,我就会害怕改变它,因为它会在运行时默默地为所有下游依赖项而破坏!这导致了巴洛克式的API,这些API很容易依赖于容易被腐蚀的关键字参数,并且随着时间的推移,随着时间的推移而发展的API的内容很少类似于你开箱即用的内容.因此,即使仅仅是安全问题,一旦您希望人们在您的工作之上进行构建,而不是简单地在它过于笨重时更换它,那么在API设计中就会产生长期影响.

Answer 2

这是因为打字只会删除程序,而不会启用新程序.

这不是一个正确的陈述.类型类使得可以从类型级信息生成程序的一部分.

考虑两个表达式:

1. readMaybe "15" :: Maybe Integer
2. readMaybe "15" :: Maybe Bool

我在这里使用模块中的readMaybe功能Text.Read.在术语级别,这些表达式是相同的,只有它们的类型注释是不同的.但是,它们在运行时产生的结果不同(Just 15在第一种情况下,Nothing在第二种情况下).

这是因为编译器会根据您拥有的静态类型信息为您生成代码.更确切地说,它选择一个合适的类型类实例并将其字典传递给多态函数(readMaybe在我们的例子中).

这个例子很简单,但有更复杂的用例.使用该mtl库,您可以编写在不同计算上下文(也称为Monads)中运行的计算.编译器将自动插入大量管理计算上下文的代码.在动态类型语言中,您将没有静态信息来实现此目的.

如您所见,静态类型不仅会切断不正确的程序,还会为您编写正确的程序.

Answer 3

重构。通过拥有强大的类型系统，您可以安全地重构代码，并让编译器告诉您现在所做的是否有意义。打字系统越强大，就越能避免重构错误。这当然意味着您的代码更易于维护。