Idris趋近发布1.0版

摘要： 基于依赖类型的Idris语言即将完成0.99版本，其1.0版有望于2017年2月左右发布。Idris是一种纯函数式编程语言，目标在于注重语言通用性及满足系统编程所需效率的同时，让更多的编程人员使用基于类型的程序验证技术。

作者： Sergio De Simone

正文：

据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