写点什么

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

  • 2017-04-13
  • 本文字数:764 字

    阅读完需:约 3 分钟

英国圣安德鲁大学讲师、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

2017-04-13 19:007350
用户头像

发布了 1008 篇内容, 共 444.7 次阅读, 收获喜欢 346 次。

关注

评论

发布
暂无评论
发现更多内容

【最佳实践】修改Anaconda中的Jupyter Notebook默认工作路径

迷彩

Python Anaconda Jupyter Notebook 6月月更

低代码实现探索(四十二)数据+方法+组件

零道云-混合式低代码平台

OpenHarmony 官网文档有哪些上新?上篇:应用开发文档上新

OpenHarmony开发者

OpenHarmony

java培训 | Mybatis的特性

@零度

mybatis JAVA开发

Archiva 运行时提示 JAXBException 错误

HoneyMoose

NodeJS 5分钟 连接MySQL 增删改查 🥇

德育处主任

node.js MySQL 6月月更

文档管理系统应该具备哪些功能?

小炮

【高并发】高并发环境下构建缓存服务需要注意哪些问题?

冰河

并发编程 多线程 高并发 异步编程 6月月更

交友app源码未来的发展趋势是什么?

开源直播系统源码

NLP论文领读|缺少有标注的数据集怎么训练文本检索模型?来看看 LaPraDoR怎么做的吧

澜舟孟子开源社区

人工智能 自然语言处理 神经网络 深度学习 nlp

直播倒计时1天!天翼云HPC解决方案助力企业腾飞

天翼云开发者社区

今天 3 点!Intel Arch 和高性能存储技术两大 SIG 核心成员在线分享|第 21-22 期

OpenAnolis小助手

容器 镜像 直播 内核 龙蜥大讲堂

如何使用 API 的方式消费 SAP Commerce Cloud 的订单服务

汪子熙

node.js SAP commerce 电商云 6月月更

EasyNLP带你玩转CLIP图文检索

阿里云大数据AI技术

数据挖掘 存储 算法框架/工具 机器学习/深度学习

Linux开发_介绍目录编程、标准文件编程、Linux系统文件接口编程、GDB调试

DS小龙哥

6月月更

签约喜报 | 月财生态签约旺链科技,区块链溯源让有机产品“有迹可循”

旺链科技

区块链 产业区块链 食品溯源 有机食品

如何在 Django 中使用 MVT 创建基本项目?

海拥(haiyong.site)

django 6月月更

Python代码自动提取Win10内置的锁屏壁纸

宇宙之一粟

Python 6月月更

【sql语句基础】——查(select)(合并查询+连接查询)

写代码两年半

sql 查询 MySQL 数据库 数据库· 6月月更

C#入门系列(十四) -- 结构体应用

陈言必行

C# 6月月更

从社恐到社牛,多亏了这款私人学习成长暗器!

博文视点Broadview

如何在 Vue 项目中,通过点击 DOM 自动定位VSCode中的代码行?

vivo互联网技术

Vue 前端 vscode vite webpack

Push还是Pull,这是个问题么?

MatrixOrigin

push Pull MatrixOrigin MatrixOne 数据库·

实战模拟│揭秘为啥年会你抽不到特等奖

随机 概率 抽奖系统 6月月更

spring4.1.8扩展实战之三:广播与监听

程序员欣宸

Java spring Spring Framework 6月月更

推荐的十个Flutter插件

坚果

6月月更

ZooKeeper进阶(二):ZooKeeper的运行

No Silver Bullet

zookeeper 6月月更

【Python技能树共建】scrapy 上手篇

梦想橡皮擦

Python 爬虫 Python爬虫 6月月更

InfoQ 极客传媒 15 周年庆征文 | Kettle实现ES到ES循环增量抽取

写程序的小王叔叔

架构 kettle ELK Stack InfoQ极客传媒15周年庆

了解 Session、LocatStorage、Cache-Control、ETag

CRMEB

依赖类型语言Idris发布1.0版本_后端_Sergio De Simone_InfoQ精选文章