haskell - 除了安全之外，强打字还有其他好处吗？

Question

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

对于函数式编程语言中的大多数程序，有一种方法可以将其表示为无类型的 lambda 演算术语，无论类型多么先进。那是因为打字只会消除程序，而不是启用新程序。

强打字为我们赢得了安全。在运行时发生的错误类别如何不再在运行时发生。这种安全性相当不错。除了这种安全性，强类型还能给你什么？

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

(请注意，我并不是说强类型毫无值(value)。安全性本身就是一个巨大的好处。我只是想知道是否还有其他好处。)

Answer 1

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

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

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

当 Haskell Curry 描述 lambda 演算时，类型是放在术语上的注释。

所以我们有 lambda 演算 a la Church 和 lambda 演算 a la Curry。见 https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus#Intrinsic_vs._extrinsic_interpretations更多。

具有讽刺意味的是，以 Curry 命名的 Haskell 语言是基于 lambda 演算的，就像 Church 一样!

这意味着类型不仅仅是为您排除不良程序的注释。他们也可以“做事”。这种类型不会删除而不留下残留物。

这体现在 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以上，比手动构建 LexicographicComparator<List<Char>> 简洁得多。通过传递一个 IComparator<Char>到它的构造函数并使用额外的第二个参数调用函数，如果我要比较调用这样的 sort 的复杂性Haskell 中的函数以在 C# 或 Java 中调用它。

这向我们表明，使用类型进行编程可以显着减少冗长，因为隐式和类型类等机制可以在类型检查期间为您的程序推断出大部分代码。

在更简单的基础上，即使参数的大小也可能取决于类型，除非您想支付相当大的成本来将您的语言中的所有内容装箱以使其具有同质表示。

这向我们表明，使用类型进行编程可以显着提高效率，因为它可以使用专用的表示，而不是为代码中的任何地方的盒装结构付费。一个 int不能只是机器整数，因为它必须以某种方式看起来像系统中的其他所有内容。如果您愿意在运行时放弃一个数量级或更多值(value)的性能，那么这对您来说可能无关紧要。

最后，一旦我们有类型为我们“做事”，考虑仅仅安全提供的重构好处通常是有益的。

如果我重构剩下的较小的代码集，它将为我重写所有类型类管道。它将找出重写代码以拆箱更多参数的新方法。我不拘泥于手工阐述所有这些东西，我可以将这些平凡的任务留给类型检查器。

但即使我确实更改了类型，我也可以相当随意地移动参数，让编译器很可能会捕捉到我的错误。类型为您提供“自由定理”，类似于针对此类错误的整个类的单元测试。

另一方面，一旦我用 Python 这样的语言锁定了一个 API，我就非常害怕改变它，因为它会在运行时默默地破坏我所有的下游依赖项!这导致巴洛克式的 API 严重依赖于容易被贬低的关键字参数，并且随着时间的推移而演变的 API 很少类似于你重新构建的开箱即用的 API。因此，一旦您希望人们在您的工作之上构建，而不是在它变得过于笨重时简单地替换它，即使仅仅是安全问题也会对 API 设计产生长期影响。