写点什么

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

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

关注

评论

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

智能商品计划管理系统:服装品牌精准决策与高效运营的秘密武器

第七在线

创纪录:英伟达市值一日增 2770 亿美元;Xiaomi 14 Ultra 正式发布丨 RTE 开发者日报 Vol.150

声网

Alibaba Cloud Linux 解锁云算力-软硬协同构建云上最佳操作系统体验

OpenAnolis小助手

Java Linux 阿里云 操作系统 龙蜥社区

TimechoDB v1.3.1 发布 | 新增多种内置函数、脚本工具等功能,集群可观测性持续提升

Apache IoTDB

六大新兴技术助力未来工作效率提升

不在线第一只蜗牛

区块链 人工智能 云计算 物联网

面试官:什么是Java内存模型?

不在线第一只蜗牛

Java 程序员 面试 内存

互联网人的副业探索指南

老张

第二曲线 码农副业

2024 年的第一次见面!这场开源数据技术沙龙不容错过

Apache IoTDB

蓝戟英特尔锐炫A770驱动对比测评,游戏性能迎来全面提升!

E科讯

快手商品数据采集神器,助你轻松获取商品详情数据

tbapi

快手商品详情数据接口 快手API接口 快手API 快手商品详情数据采集

2024年,技术圈的热点会是什么?

伤感汤姆布利柏

HUAWEI Pocket 2亮相 HarmonyOS 4软硬件结合再掀智慧风潮

极客天地

性价比拉满!英特尔锐炫新驱动,提升可达418%!

E科讯

NOW 闹个元宵?与亚信安慧AntDB一起猜灯谜,抽奖品

亚信AntDB数据库

数据库 AntDB AntDB数据库

Runaway Queries 管理:提升 TiDB 稳定性的智能引擎

PingCAP

MySQL 数据库 TiDB

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