把强而静态的打字打到极致？

Question

在强的、静态的类型中，使用不同的类型是很常见的，即使对于简单的、原始的类型的变量也是如此，这样可以简化静态分析并向程序员表示意图。三维空间中的颜色和点都可以用3块浮点数的数组来表示，但是给出了不同的类型名称。在C中，许多常见的类型都是类型简单的类型。

我在想:这到底有多实际呢？如果您正在编写一个在0到1之间使用浮点数的函数(也许它代表一个概率分布)，那么是否创建一个单独的类型？那么一个必须接受非零整数的函数呢？创建一个类型nonZeroInt是否合理，不是为了封装的目的，而是为了类型安全？

您可以任意地将函数的所有先决条件编码到类型系统中。例如，您可以为只接受素数的函数的输入定义一个"primeNumber“类型。如果一个函数必须包含两个没有公共因素的整数，则可以将其更改为接受一个类型为“coprimePair”的参数。

上述两个假设函数可能是库的一部分，其中包括生成素数和互质对的函数，并以适当的类型返回它们。如果我想在库中调用一个需要素数的函数，而我没有从包含的素数生成函数中得到它，我就必须显式地转换一个int，本质上迫使我做一个现实检查，并问自己，“我确定这个变量永远是素数吗？”

我的具体问题是:这种哲学在实践中成功地走了多远？是否有编程语言，或受人尊敬的编程文本，鼓励这样一种哲学:每一个不能容纳任何现有类型的全部类型的函数作为其输入，并为所有可能的输入返回有意义的结果，而是应该定义一种新的类型？

Answer 1

Jack和tp1的评论(实际上应该是答案)已经解释了如何在函数式语言中实现这一点。

我的回答增加了一个关于非功能语言的观点，特别是在开发行业中非常流行的语言: C#。

在C#或Java等语言中，在需要限制值时创建类型确实是当前的一种做法。如果您只需要一个正整数，那么您将得到一个PositiveInt类，但一般来说，这些包装器将更多地反映业务逻辑(ProductPrice、RebatePercentage等)，以及内部验证(产品价格应该高于零，折扣百分比不接受大于100的值等)。

最近讨论了这里的优点和缺点，以及在这类类型上做得太过分的风险。

一旦有了包装器，就可以开始向其添加逻辑，特别是验证。基本上，由于包装器隐藏了它包装的值，验证逻辑将位于构造函数中，并且可以基本如下所示：

if (value > 100)
{
    throw new ArgumentOutOfRangeException("value", "The allowed range is (0..100].");
}

C#提供的另一种可能性是使用代码契约，这提供了几个好处：

• 静态检查捕捉到在运行时遇到错误之前对这些包装的误用，
• 在运行时也要强制执行代码契约，您可以肯定，即使禁用了静态检查(或者其警告被开发人员拒绝)，契约也不会被滥用，
• 使用检查包装值的不变量，无法分配无效的值(有一个限制，即检查是在方法开始或结束时完成的，而不是在方法执行过程中的每一步)，
• Visual集成通过向调用方提供有关合同的提示，使代码自文档化。

它在实践中成功了吗？嗯，在.NET框架本身中有数千种方法，其中包含代码契约。对于业务代码来说，最主要的问题是代码有多重要。如果失败的后果是昂贵的，那么使用代码契约是非常有吸引力的。另一方面，就开发人员的时间而言，代码契约有很大的成本(确保所有合同都能很好地工作在一个除小项目之外的所有项目上都需要大量时间)，对于不一定需要这种可靠性的项目来说，这可能不是一个好主意。

这也回答了你的另一个问题：

我在想:这到底有多实际呢？

这是一个严格和灵活的问题。

• 如果您需要非常快的开发，并承担运行时错误的风险，您将选择一种弱类型语言。编写较少的代码(例如print(123) )的好处超过了调试问题的风险，例如123 + "4" (会导致127或"1234"吗？)在这种情况下，类型要么不存在，要么由语言/框架隐式地管理。虽然您仍然可以进行范围验证(例如对用户输入进行消毒)，但是在与外部世界的接口之外进行这样的验证看起来很奇怪。
• 如果您正在开发生命关键软件，您将使用正式的证明，这将花费大量的时间，但将确保代码中没有错误。在这种情况下，类型将有严格的验证:数值的范围和精度，字符串的长度和允许的字符，等等。
• 在此期间，您将选择最符合您需要的方法。对于大多数软件来说，代码契约将是一种过度的扼杀。但是对于大多数软件来说，在类型包装器(如Percentage)中进行基本检查可能是个好主意。在不进入为所有事物创建类的极端(如上面已经提供的链接中所讨论的)的情况下，有一些泛型类型(如Range<T>或LengthLimitedString )在C#或C#等语言中实现并不那么困难，这可能是一个很好的折衷方案。

Answer 2

我曾经用这种方式在Ada为军用飞机编写现实世界的软件。我们不仅对范围，而且对单位和数组索引使用单独的类型。例如，以米为单位的距离与以英尺为单位的距离不同。100元素数组中的索引与10元素数组中的索引类型不同.

首先是好事。相当多的bug确实在编译时被捕获。运行时bug通常是在离源更近的地方捕获的。例如，一个超出界限的数组索引将在首次分配索引时捕获，而不是当您试图取消它时。此外，还有一些速度优势，因为运行时不需要检查类型系统静态检查的内容。

还有一些缺点：

• 大量编译错误，通常带有奇怪的消息。这是在编译时捕获bug的副作用。你觉得自己总是在和编译器斗争。另一方面，当您第一次修复所有编译器错误时，它通常是有效的。
• 大量的类型注释。
• 大量使用仿制药。当我第一次查找语法来创建我自己的模板类时，我已经做了两年的C++工作了。我每天都做类似的Ada。
• 需要有一个健壮的编码标准和同行评审流程，以防止程序员采取不那么安全的捷径。
• 要让新的程序员跟上习惯松散类型的人是很困难的。

对于安全来说，这绝对是值得的。但是，我想我更喜欢一种具有类型推理和强大的程序员控制能力的语言，比如Scala，在这种语言中，使用较少的输入可以获得很大的安全性。

Answer 3

这是在haskell所做的事情：

data Prime = Prime Int
primeFromInt :: Int -> Maybe Prime
primeFromInt a | isPrime a = Just (Prime a)
primeFromInt _ = Nothing

请注意，它仍然允许声称int是素数：

Prime 10

即使10不是素数，编译器也无法检测到这个问题。相反，如果你把它写成另一种方式

primeFromInt 10

这将很好地拒绝10和给我们任何东西。