BT

你的观点很重要! 快来参与InfoQ调研吧!

依赖类型语言Idris发布1.0版本

| 作者 Sergio De Simone 关注 5 他的粉丝 ,译者 谢丽 关注 3 他的粉丝 发布于 2017年4月14日. 估计阅读时间: 2 分钟 | ArchSummit社交架构图谱:Facebook、Snapchat、Tumblr等背后的核心技术

英国圣安德鲁大学讲师、Idris创建者Edwin Brady写道,在达到alpha阶段几个月之后,Idris 1.0发布。

1.0版本发布,最关键的一点是其核心语言及基础库都被认为是稳定的,就是说,将来的1.x版本应该确保源代码向后兼容。自alpha版本以来,Idris就一直致力于工具和库的支持,同时,该语言添加了新的编译指令和一个新的LinearTypes语言扩展,其中前者是为了让使用稳定性较差的特性成为可能。然而,据Brady介绍,还是有许许多多可以做贡献的地方,尤其是改进编译器和运行时效率,以及修复200多个当前正处于打开状态的Bug。

虽然Brady认为,Idris从根本上讲是一个研究工具,目前还不足以考虑在生产环境中应用,但由Brady写作并于近期出版的Manning of Type-Driven Development with Idris,其GitHub库贡献者数量的增加,以及最近的学术著作,都说明人们对于这门语言的兴趣一直在增长。这些可以看作是Idris社区开始形成的标志,虽然这样说还有点太早。InfoQ请求Brady对此发表评论,他的回复如下:

看到人们对Idris越来越感兴趣当然不错!虽然还有大量的工作要做,但我们已经达到了1.0版本,我们现在已经有了一门可以作为构建基础的稳定语言。我当前的目标是改进内核的效率和健壮性。

我们仍然还有不少处于打开状态的问题,但是,其中有许多是关于工具和可用性,另外还有许多特性请求。如果有人想参与,则可以从那些带有“Low Hanging Fruit”标签的开始。如果任何人有任何问题,Idris社区都会尽量提供帮助。

Idris是一门纯粹的函数式程序设计语言,旨在为更多的程序员提供基于类型的程序验证技术,同时,还能继续专注于成为一门通用语言,并且足够高效,可以用于系统编程。想要学习Idris的读者,可以阅读这个教程。此外,务必要阅读有关依赖类型编程的利弊

查看英文原文Dependent-types Language Idris Reaches 1.0

评价本文

专业度
风格

您好,朋友!

您需要 注册一个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