哈Ha 前几天，我在寻找如何在Idris中做某事，并且遇到了一篇不错的文章，该文章的免费翻译似乎很合适。 自由和插科打where在必要时，我将表示“在此通过开头和结尾处的这种曲折表达”。
什么时候使用测试，什么时候使用-类型？ 为了编写我们的努力，我们会得到什么信息和什么保证？
我们将看一个用Python，C，Haskell和Idris表示的简单但有些人为的示例。 在每种情况下，我们也将看到在没有任何其他知识的情况下对实现可以说的话。
我们不会考虑允许我们显式违反语言保证的各种后门（例如C扩展，Haskell中的unsafePerformIO ，不安全的类型转换），否则根本不可能得出任何结论，并且这篇文章将很短。 ⟦此外，同一Haskell包含Safe Haskell的子集，该子集明确且可传递地禁止使用这些内容以及许多其他可能破坏语言完整性的技巧。
规格书
让清单和一些含义。 有必要返回该值在列表中的索引或指示该值不在列表中。
该规范的实现很简单，因此很自然地要问，这里通常是测试或类型。 但是，我们今天将讨论的那些属性和推理方法适用于复杂得多的代码。 如果可以帮助实现一万行不可读的意大利面条代码，则有助于查看它们的用处。
巨蟒
def x(y, z):
我们马上注意到，我们对不受限制的⟦和语义不感兴趣-不会影响变量命名和文本文档之类的程序的属性，因此我故意不编写有助于感知的代码。 我们只对以下事实感兴趣：在通过测试和类型检查的情况下， 它一定不能是不正确的 。
在上面的代码中，除了我们有一个带有两个参数的函数外，几乎没有有用的信息。 该函数同样可以很好地在列表中找到该值的索引，或者可以向您的祖母发送侮辱性的信件。
分析方法
我们不仅会获得没有测试和类型的易碎代码，而且了解函数功能的唯一方法就是文档。 而且由于文档是由人而不是机器来检查的，因此很容易被证明是过时的或最初不正确的。
- 该文件
- know我们知道预期的行为
关于此功能的行为，我们无话可说。 你恨你奶奶。 你是个怪物。
- 质保
- ✓内存安全
Python是一种垃圾回收语言，消除了我们的这种担忧。 ⟦但是，据我所知，没有什么可以阻止您将不安全的库或C FFI拉到该函数中。
带有测试的Python
def test_happy_path(): assert x([1, 2, 3], 2) == 1 def test_missing(): assert x([1, 2, 3], 4) is None
现在我们知道函数可以正常工作，如果缺少该元素，则结果为None ？
好吧...不 这只是一个例子。 不幸的是，我们功能的范围是无限的，没有任何例子可以证明我们功能的正确运行。 更多测试-更有信心，但是没有任何测试可以解决所有疑问。
该函数对于4返回5而不返回5的可能性听起来很疯狂，在这种情况下，这很可能是胡说八道。 我们可以对自己的信仰水平感到满意，并在某些示例上进行介绍。 但是话又说回来，那篇文章将很简短，所以让我们想象一下实现不是那么明显。
由于测试无法在一般情况下证明某事，而只能通过特定示例显示其行为，因此测试无法表明没有错误。 例如，没有测试可以表明我们的函数从不抛出异常，从不进入永恒周期或不包含无效链接。 这只能是静态分析。
但是，即使这些示例在证据方面的作用不是很好，但它们至少构成了很好的文档。 从这两个示例中，我们可以在一些其他先验假设下得出完整的规范-这两个示例还满足例如“ counterspec”“查找数组中的元素并返回上一个（如果有的话）”的问题，这花了我十秒钟。
分析方法
尽管测试可以显示如何使用我们的函数，并且至少可以通过一些示例使人确信此函数可以正常工作，但在一般情况下它们无法证明我们的代码有任何作用。 不幸的是，这意味着测试仅部分有助于避免错误。
- 该文件
- ✓ 我们有一个使用示例
- ✓ 我们知道一些可以正确处理的值类别
- ✗我们知道将正确处理的所有类型的值
我们对参数的类型没有任何限制，因此尽管存在函数可以处理的示例，但我们不知道尚未测试哪些类型。 - know我们知道预期的行为
⟦原始文章的作者在此处打勾，考虑到上面的评论，我将允许我自己打叉。
- 规格书
- ✓ 至少在一种情况下有效
- returned返回的索引始终是有效索引
- ✗返回的索引始终指示合适的值
- ing缺少的项目始终返回
None / Nothing
- 常见错误
- ✗没有错别字或名字不正确
静态分析可以提供帮助，但是由于Python是一种动态语言，具有在运行时覆盖各种内容的能力，因此我们永远无法证明没有错误。
尤其是，很难确定方法名称是否正确，因为方法调用的有效性取决于对其进行调用的对象的运行时类型。 - ✗没有意外的
null - case总是处理错误情况
以我的经验，这是最常见的错误来源之一：在我们的示例中，如果缺少元素，该函数将返回None ，但是使用此函数的代码可以假定，例如，它将始终返回一个数字。 另外，这也可能导致未处理的异常。
- 质保
- ✓内存安全
- cannot不能以错误的类型调用函数
- ✗无副作用
- ✗没有例外
- errors没有错误
- ✗无永久循环
哈斯克尔
xyz =
如果您不熟悉语法：这是带有参数y和z的函数x的定义。 在Haskell中，您可以省略类型，因为它们将从实现中推导出来-“当然，除非您使用与现代类型系统扩展不同的高级功能”。
看来这与Python版本没有太大区别，只是因为我们在Haskell中编写了函数并将其平铺，所以我们已经可以讨论一些有趣的属性了。
分析方法
显然，我们在这里不能得出太多结论，但以下几点需要注意：
- 该文件
- 常见错误
- ✓ 没有错别字或名字不正确
由于Haskell是一种编译语言，因此所有名称都必须在编译时解析。 如果出现此错误，程序将不会编译。 - ✓ 没有意外的
null
Haskell只是没有null 。 问题解决了！
- 质保
- ✓内存安全
- ✓ 函数不能以错误的类型调用
- ✓ 没有意外的副作用
article原始文章的作者未指出此项目，但我将允许自己注意，如果有副作用，此函数的推导类型将表明它们的存在，以便调用代码可以了解其功能。⟧
Haskell类型指定
x :: Eq a => [a] -> a -> Maybe Int xyz =
早些时候，我们谈到了对祖母安全性的一种相当令人信服的态度：从测试中可以明显看出，该功能不会损害任何人，但是祖母真的安全吗？ 此功能是否准确发送不发誓的信？
Haskell以纯函数式语言而闻名。 这并不意味着代码不会有副作用，但是所有副作用都必须存在于类型中。 我们知道此函数的类型，我们看到它是干净的，因此我们确定此函数不会修改任何外部状态。
出于其他原因，这是一个非常有趣的属性：由于我们知道没有副作用，因此仅基于其签名，我们就可以了解该功能的作用！ 只需搜索此Hoogle签名并查看第一个结果即可。 当然，这不是具有这种类型的唯一可能的函数，但是对于文档而言，类型为我们提供了足够的信心。
分析方法
- 该文件
- ✓ 我们知道预期的行为
- ✗我们有一个使用示例
- ✓我们知道一些可以正确处理的值类别
- ✓ 我们知道将正确处理的所有类型的值
- 规格书
- in至少在一种情况下有效。
由于缺少测试或证据，我们不知道我们的功能是否按预期工作！ - ✗返回的索引始终是有效索引。
- ✗返回的索引始终指示合适的值。
- missing缺少的项目始终返回
None / Nothing 。
- 常见错误
- ✓没有错别字或名字不正确
- ✓没有意外的
null - ✓ 错误案例始终得到处理
如果我们的函数返回Nothing ，则类型系统确保调用代码正确处理了这种情况。 当然，这种情况可以忽略，但是必须明确地做到这一点。
- 质保
- ✓内存安全
- ✓函数不能以错误的类型调用
- ✓ 无副作用
- ✗没有例外
我分享异常和错误，相信在异常之后可以恢复，并且在错误之后（例如，部分定义的函数）也可以恢复-不。
在大多数情况下，异常以类型进行描述（例如，在IO monad中）。 以一种好的方式，我们应该知道一个函数不会仅基于其类型抛出异常。 但是，Haskell通过允许从纯代码中引发异常打破了这种期望。
⟦此外，值得注意的是，在Haskell中，诸如错误调用部分定义的函数之类的错误也作为可捕获和处理的异常而呈现，因此这两种类别之间的差异不太明显。 - errors没有错误
我们仍然可以使用部分定义的函数，例如零除。 - ✗无永久循环
Haskell进行测试
还记得我之前说过的测试不能证明没有错误吗？ 我撒谎了 当恒星正确会聚，并且如果将测试与类型结合在一起，那么就有可能！ 第一颗星星是我们功能范围的有限性。 第二-定义的范围不仅应该是有限的，而且还应该不是很大，否则这种测试将很难付诸实践。
例如：
not :: Bool -> Bool not x = ...
输入可以是True或False 。 测试这两个选项就足够了，这就是圣杯！ 无异常，永久循环，错误结果，无错误。 ⟦但是，对于稍微复杂的功能，可能尚不清楚要花多少时间来进行测试：如果测试需要很长时间才能完成，那么我们是否会陷入一个永恒的循环，或者仅仅是沉重的循环？ 阻止她的问题。
实际上，就Haskell而言，这也不是完全正确的：在每种Haskell类型中，也都有一个值un（可以通过undefined ， error或在某种意义上以无限递归获得），但Haskellist传统上会闭上眼睛并相信它不存在。
课外阅读： 仅有40亿浮游物-所以全部测试！
无论如何，在我们的原始示例中，范围是无限的，因此测试只能表明我们的代码适用于有限的示例集。
分析方法
在这种情况下，测试可以对类型进行补充，并在Haskell类型系统中插入一些漏洞。 与仅使用测试或类型相比，我们对代码更有信心。
ç
/* C , int */ int x(int *y, size_t n, int z) { /* 10000 */ }
我们认为C对较旧类型的系统不感兴趣。 特别是在C语言中，程序员最有可能不需要类型，而是由编译器来帮助他们生成更快的代码。
在我们的示例中，我们不知道如果找不到该元素，函数将返回什么。 我们将不得不依靠传统或文档（例如，在这种情况下可能是-1 ）。
我们还可以使用out参数：这样，我们可以返回错误并将返回值存储到out参数中。 这是一个更具表达性的选项，但是我们仍然必须依靠文档来了解读取和写入了哪些参数。 在这两种情况下，都很难通过查看类型来理解行为。
/* , out- */ error_t x(int *y, size_t n, int z, size_t *w) { /* 10000 */ }
分析方法
类型系统本身并不能给我们那么多保证。 当然，我们从这些类型中获得了一些信息，但只需将其与Haskell案例进行比较即可。
伊德里斯
x : Eq x => List x -> x -> Maybe Int xyz = ...
该函数与Haskell的类型相同。 但是，使用更具表现力的类型系统，我们可以实现更多目标。 类型的选择可以谈论实现。
%default total x : Eq x => Vect nx -> x -> Maybe (Fin n) xyz = ...
可以将这种类型理解为“给我一个大小为n且有一些值的列表，我将返回小于n或Nothing 。” 这样可以确保函数返回的索引显然不会超出范围。
另外，此功能是总计功能，即计时器已检查其始终结束。 这消除了永久的循环和错误。
分析方法
- 规格书
- in至少在一种情况下有效。
- ✓ 返回的索引始终是正确的索引
- ✗返回的索引始终指示合适的值
- ing缺少的项目始终返回
None / Nothing
- 质保
- ✓内存安全
- ✓函数不能以错误的类型调用
- ✓无副作用
- ✗没有例外
- ✓ 没有错误
- ✓ 无永久循环
伊德里斯与测试
由于Idris的类型语言与其术语⟦（或更确切地说是其可证明的总和）⟧的语言一样具有表现力，因此测试和类型之间的区别变得模糊了：
ex : x [1, 2, 3] 2 = Just 1 ex = Refl
该函数的类型非常奇怪x [1, 2, 3] 2 = Just 1 。 此类型意味着，对于成功的类型检查，键入器必须证明x [1, 2, 3] 2结构上等于Just 1 。 ⟦在这种情况下，证明是微不足道的，因为足以使倾翻者对等号两边的项进行归一化，由于所使用的所有功能的总和，这将在有限的时间内完成，并且由于Church-Rosser而导致独特的结果。 此后，可以使用相等的自反性，即Refl.⟧
实际上，我们写了一个类型级别的测试。
有证据的伊德里斯
为了分析的完整性，我们可以使用依存类型的全部功能并证明我们的实现（因为Idris中的依存类型等效于包含构造性一阶逻辑的逻辑系统）。
特别是，我们可以证明以前无法获得的属性：
-- Eq DecEq x : DecEq a => Vect na -> (y : a) -> Maybe (Fin n) xyz = ... -- , `x` findIndexOk : DecEq a => (y : Vect na) -> (z : a) -> case xyz of Just i => index iy = z Nothing => Not (Elem zy) findIndexOk yz = ...
对于任何类型a ，对于它具有算法上可判定的比较（ DecEq ），对于类型a任何长度y元素y任何向量y和类型a任何值z ：均可将findIndexOk类型理解为：如果xyz返回索引i ，则此索引位于z ，但是如果xyz返回Nothing ，则向量中根本没有这样的元素。”
有趣的是，原始文章的作者给出的类型比上面给出的类型略弱。
现在我们已捕获所有内容！ 缺点是什么？ 好吧，写所有这些证据可能非常困难。
比较方式
意见
我认为，就收到的信息之间的关系而言，使用现代类型的系统本身最为有效，并且可以保证所付出的努力。 如果您想编写相当可靠的代码，则可以通过测试对类型进行调整。 理想情况下-采用QuickCheck的样式。
对于依赖类型，测试和类型之间的界线变得不太明显。 如果您正在为波音或起搏器编写软件，则编写证据可能会很有用。