大家好！
尽管今天讨论的主题有些古怪和抽象-我们希望它可以使您的周末多样化。 在文章的末尾，我们放置了作者的三个链接，使您熟悉Idris，F *和JavaScript的依赖类型。
有时似乎编程语言自60年代以来并没有太大变化。 当他们告诉我这件事时，我经常想起我们现在拥有多少个出色的工具和功能，以及它们如何简化我们的生活。 临时：这些是集成的调试器，单元测试，静态分析器，凉爽的IDE以及类型化数组等等。 语言的发展是一个漫长而渐进的过程，没有这样的“银弹”可以一劳永逸地改变语言的发展。
今天，我想告诉您这个正在进行的过程的最后阶段之一。 我们正在谈论的技术仍在积极探索中，但是一切都表明它将很快在主流语言中扎根。 我们的故事从计算机科学中最基本的概念之一开始：
类型 。
类型世界
打字是与我们的思想密不可分的事情之一，以至于我们甚至根本没有考虑过类型的概念？ 为什么1是一个
int ，但如果仅将此值放在引号中，则它变成
string ？ 本质上，什么是“类型”？ 在编程中通常会遇到这种情况，答案取决于问题的措辞。
类型多样。 在某些类型系统中，类型和值之间有非常清晰的界限。 因此，3、2和1是
integer数值，但
integer不是值。 这种结构在语言中是“嵌入的”，与含义有根本的不同。 但是，实际上，这种区别是没有必要的，只能限制我们。
如果您释放这些类型并将它们转换为另一种值类别，那么就会出现许多惊人的可能性。 值可以存储，转换并传递给函数。 因此，有可能制作一个将类型作为参数的函数，从而创建通用的函数：可以在不重载的情况下处理许多类型的函数。 您可以具有给定类型的值的数组，而不必像在C中那样进行奇怪的指针算术和类型转换。您还可以在程序运行时收集新类型，并提供自动JSON反序列化等功能。 但是，即使您将类型视为值，也仍然无法做到所有类型都可以对值进行处理。 因此，使用用户实例进行操作，例如，您可以比较其名称，检查其年龄或标识符等。
if user.name == "Marin" && user.age < 65 { print("You can't retire yet!") }
但是，当您尝试对
User类型执行相同
User ，只能比较类型名称和可能的属性名称。 由于这是一种类型，而不是实例，因此无法检查其属性的值。
if typeof(user) == User { print("Well, it's a user. That's all I know") }
如果我们具有仅接收非空用户列表的功能，那将有多酷？ 还是仅当电子邮件地址以正确格式记录时才接受电子邮件地址的功能？ 为此，您需要使用“非空数组”或“电子邮件地址”类型。 在这种情况下，它是一个与值相关的类型，即 关于
依赖类型 。 在主流语言中，这是不可能的。
为了可以使用类型，编译器必须检查它们。 如果您声明该变量包含整数，那么如果其中没有
string会更好，否则编译器会发誓。 原则上讲，这很好，因为它不允许我们求爱。 检查类型非常简单：如果一个函数返回一个
integer ，而我们尝试在其中返回
"Marin" ，则这是一个错误。
但是，对于依赖类型，情况会变得更加复杂。 问题是编译器究竟何时检查类型。 如果程序尚未运行，他如何确保数组中恰好有三个值？ 如果尚未分配整数，如何确保它大于3？ 这就是
魔术 ……或者换句话说，
数学 。 如果可以从数学上证明数字集始终大于3，则编译器可以对此进行验证。
工作室里的数学！
数学归纳法用于制定证据。 归纳法使我们能够无条件确认陈述的真实性。 例如，我们想证明以下数学公式适用于任何正数：
1 + 2 + 3 + ... + x = x * (x + 1) / 2
x的数目是无限的，因此我们需要很长时间才能手动检查所有数字。 幸运的是，这不是必需的。 我们只需要证明两件事：
- 在第一天就观察到该陈述。 （通常是0或1）
- 如果此陈述对数字
n为真，则对下一个数字n + 1为真。
由于对于第一个数字和所有随后的数字都遵循该声明，因此我们知道对于所有可能的数字都是正确的。
要证明这一点并不困难：
1 = 1 * (1 + 1) / 2 1 = 1
现在我们还必须证明该语句适用于所有其他数字。 为此，假设它适用于某个数字n，然后确保它也适用于n + 1。
假设以下表达式为真：
1 + 2 + 3 + ... + n = n * (n + 1) / 2
检查出
n + 1 ：
(1 + 2 + 3 + ... + n) + (n + 1) = (n + 1) * ((n + 1) + 1) / 2
因此，我们可以用以上等式替换
"(1 + 2 + 3 + ... + n)" ：
(n * (n + 1) / 2) + (n + 1) = (n + 1) * ((n + 2) / 2)
并简化为
(n + 1) * (n/2 + 1) = (n + 1) * (n/2 + 1)
由于表达式的两个部分相等，因此我们确保此语句为真。 这是无需手动计算每种情况即可验证语句真实性的方法之一，并且基于此原理，依赖类型起作用。 您编写数学语句以确保类型命题正确。
这种方法的优点在于，任何数学证明都可以以计算机程序的形式发布-这就是我们所需要的！
返回编程
因此，我们发现可以先证明某些事情，然后再进行特定值的证明。 为此，需要使用一种编程语言来表达将要写入类型系统本身的代码中的这些语句，也就是说，需要改进类型系统。
考虑一个例子。 在这里，我们有一个append函数，它接受两个数组并将其组合。 通常，此类函数的签名如下所示：
append: (arr1: Array, arr2: Array) -> Array
但是，仅通过查看签名，我们就无法确定正确的实现。 函数返回一个数组的事实并不意味着它做了什么。 检查结果的一种方法是确保结果数组的长度等于参数数组的长度之和。
newArray = append([1], [2, 3]) assert(length(newArray) == 3)
但是，如果可以创建一个在编译时检查的约束，为什么还要在运行时检查它：
append: (arr1: Array, arr2: Array) -> newArray: Array where length(newArray) == length(arr1) + length(arr2)
我们声明
append是一个函数，它接受两个
Array参数并返回一个新的
Array参数，我们称之为
newArray 。 仅在这一次，我们增加了一个警告，新数组的长度应等于该函数所有参数的长度之和。 我们在运行时上面获得的语句在编译时转换为类型。
上面的代码引用类型的世界，而不是值，即
==符号表示返回的类型
length的比较，而不是其值。 为了使这种机制起作用，返回的类型长度必须给我们一些有关实际数字的信息。
为了确保这种机制的运行，您需要确保每个数字都是单独的类型。 一种类型只能包含一个值：1.同样的值适用于2、3和所有其他数字。 当然，这样的工作很累人，但是我们需要进行编程才能完成这样的工作。 您可以编写一个可以为我们完成此任务的编译器。
完成此操作后，您可以为包含1，2，3和不同数量元素的数组创建单独的类型。
ArrayOfOne ，
ArrayOfTwo等。
因此，您可以定义长度函数，该函数将采用上述数组类型之一，并有一个相关的返回类型，
One ArrayOfOne为
One ，
ArrayOfOne为
Two ，
ArrayOfTwo 。 每个数字。
现在，对于数组的任何特定长度，我们都有一个单独的类型，我们可以验证（在编译时）两个数组的长度相等。 为此，比较它们的类型。 并且由于类型与其他任何类型都具有相同的值，因此您可以为其分配操作。 您可以通过指定
ArrayOfOne和
ArrayOfTwo的总和等于
ArrayOfThree来确定两个特定类型的
ArrayOfThree 。
这就是编译器需要确保所编写代码正确的所有信息。
假设我们要创建一个
ArrayOfThree类型的变量：
result: ArrayOfThree = append([1], [2, 3])
编译器可以确定[1]只有一个值，因此您可以分配类型
ArrayOfOne 。 它还可以将
ArrayOfTwo分配给[2，3]。
编译器知道结果的类型必须等于第一个和第二个参数的类型之和。 他还知道ArrayOfOne + ArrayOfTwo等于ArrayOfThree，也就是说，他知道标识右侧的整个表达式的类型为ArrayOfThree。 它与左侧的表达式匹配，并且编译器很满意。
如果我们写以下内容：
result: ArrayOfTwo = append([1], [2, 3])
那么编译器将完全不满意，因为它将知道类型不正确。
依赖打字非常酷
在这种情况下，根本无法允许大量错误。 使用依赖类型，可以避免单位错误，对不存在的数组索引的访问，空指针异常，无限循环和代码损坏。
使用依赖类型，您几乎可以表达任何内容。 阶乘函数将只接受自然数，
login函数将不接受空行，
removeLast函数将仅接受非空数组。 此外，在启动程序之前，请检查所有这一切。
运行时检查的问题是，如果程序已经在运行，则它们将失败。 如果程序仅由您运行，而不由用户运行，这是正常的。 依赖类型允许您对类型级别进行此类检查，因此在程序执行期间出现此类故障是不可能的。
我认为依赖类型化是主流编程语言的未来，我迫不及待地要等待它！
→
伊德里斯→
F *→
将依赖类型添加到JavaScript