BT

如何利用碎片时间提升技术认知与能力? 点击获取答案

Idris趋近发布1.0版

| 作者 Sergio De Simone 关注 17 他的粉丝 ,译者 Rays 关注 3 他的粉丝 发布于 2016年12月30日. 估计阅读时间: 3 分钟 | QCon上海2018 关注大数据平台技术选型、搭建、系统迁移和优化的经验。

据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)关注我们。

评价本文

专业度
风格

您好,朋友!

您需要 注册一个InfoQ账号 或者 才能进行评论。在您完成注册后还需要进行一些设置。

获得来自InfoQ的更多体验。

告诉我们您的想法

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我
社区评论

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我

讨论

登陆InfoQ,与你最关心的话题互动。


找回密码....

Follow

关注你最喜爱的话题和作者

快速浏览网站内你所感兴趣话题的精选内容。

Like

内容自由定制

选择想要阅读的主题和喜爱的作者定制自己的新闻源。

Notifications

获取更新

设置通知机制以获取内容更新对您而言是否重要

BT