据Idris开发团队，基于依赖类型的Idris语言即将完成0.99版本，该版本可被看成是1.0版的Alpha版本。Idris 1.0版有望于2017年2月左右发布。

Idris是一种纯函数式编程语言，目标在于注重语言通用性及满足系统编程所需效率的同时，让更多的编程人员使用基于类型的程序验证技术。

Idris的主要理念是。正如函数表述了值之间依赖性，依赖类型旨在表示类型与值之间的依赖性。，我们可以定义一类返回值为一个列表的函数，要求列表中的元素值依次递减，只有满足了该属性，才会去编译该函数所采用的任何具体实现。对于可被Idris所表示的软件属性，还包括数组范围验证以及，譬如确保所有程序遵循特定的协议访问文件句柄。下面所示的代码段使用Idris定义了Vect向量的依赖类型，并向vapp函数中添加了两个向量：

\infixr 5 ::;\data Vect : Set -\u0026gt; Nat -\u0026gt; Set where\   VNil : Vect a O\ | (::) : a -\u0026gt; Vect a k -\u0026gt; Vect a (S k);\vapp : (Vect A n) -\u0026gt; (Vect A m) -\u0026gt; (Vect A (plus n m));\vapp VNil ys = ys;\vapp (x :: xs) ys = x :: vapp xs ys;\

编译器可以检测到上面代码段中所涉及类型的误用。例如，下面的vapp：

\vapp : Vect a n -\u0026gt; Vect a m -\u0026gt; Vect a (plus n m);\vapp VNil      ys = ys;\vapp (x :: xs) ys   = x :: vapp xs xs; -- BROKEN\

据Idris核心开发人员介绍，决定发布1.0版的主要原因是该语言正步入稳定。这并不意味着Idris已“可用于生产环境”，因为开发团队还不可能做到提供长期支持或是保证实现的质量。即使如此，作为一种探究如何使用依赖类型编程的研究工具而言，Idris还是颇具价值的。

与类似，Idris也支持交互定理证明，其中包括了，但是在用于定理证明之前，Idris意在首先成为一种通用的编程语言。Idris程序将被编译为C语言，其内存管理依赖于并使用了垃圾回收机制。

查看英文原文：

感谢对本文的审校。

给InfoQ中文站投稿或者参与内容翻译工作，请邮件至。也欢迎大家通过新浪微博（，），微信（微信号：）关注我们。