Idris 趋近发布 1.0 版

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

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

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

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

编译器可以检测到上面代码段中所涉及类型的误用。例如，下面的 vapp的实现就破坏了依赖性：

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

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

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

查看英文原文： Idris Getting Close to Version 1.0

感谢冬雨对本文的审校。

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