10 月 23 - 25 日,QCon 上海站即将召开,现在购票,享9折优惠 了解详情
写点什么

依赖类型语言 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:007245
用户头像

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

关注

评论

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

系统设计 | "胖瘦" BFF:常见的两种微服务形态

少个分号

系统设计

系统设计 | 术语管理初探讨

少个分号

系统设计

C++中的语法知识虚继承和虚基类

芯动大师

Go 条件

小万哥

Go 开源 程序员 后端 开发

构建高效实时数据流水线:Flink、Kafka 和 CnosDB 的完美组合

CnosDB

flink kafka 时序数据库 CnosDB

系统设计 | 数据字典方案

少个分号

系统设计

基于状态模式: 没有实践,再多的理论都是扯淡!!!

Immerse

ARTS 打卡第 3 周

atom

ARTS打卡第3周

Johnson

ARTS 打卡计划

重识Flutter状态管理 — 探索Flutter中的状态

编程的平行世界

flutter android 前端

ARTS打卡第三周

请务必优秀

CloudEon欢迎每一位开源贡献者加入!

CloudEon开源

系统设计 | 应用系统缓存策略

少个分号

系统设计

2023-09-03:用go编写。给你一个 n 个节点的无向无根树,节点编号从 0 到 n - 1 给你整数 n 和一个长度为 n - 1 的二维整数数组 edges , 其中 edges[i] =

福大大架构师每日一题

福大大架构师每日一题

探索图像数据中的隐藏信息:语义实体识别和关系抽取的奇妙之旅

汀丶人工智能

关系抽取 命名实体识别 智能文档

QEMU之CPU虚拟化(三):虚拟机的创建

Linux内核拾遗

Linux Kenel 虚拟化 qemu kvm VT-x

万里路,咫尺间:汽车与芯片的智能之遇

脑极体

智能汽车

ARTS 打卡第 3 周

AI帅辉

ARTS 打卡计划 AI算法

Amazo S3 是如何实现 99.999999999% 的持久性和可用性的?

亚马逊云科技 (Amazon Web Services)

人工智能 负载均衡 生成式人工智能

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