写点什么

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

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

关注

评论

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

传统企业转型之路:制造业的跨境出海实战思考

Wolink

企业出海 海外社媒营销 海外营销推广 品牌推广

同城洗车小程序系统:一站式洗车服务解决方案

微擎应用市场

openresty中filter_by_lua使用

天翼云开发者社区

API网关

央企智变新实践,网易灵动助力世界500强集团打造无人化标杆

网易伏羲

网易伏羲 具身智能 网易灵动 工程机械智能化 无人装载机

真实故事分享|从全职宝妈到备考学生,他们用“碎片时间”灵活兼职、月入千元

网易伏羲

网易伏羲 数字游民 群体智能 智能货柜 网易有灵众包

用Dify工作流打造你的AI测试智能体,效率提升500%

测吧(北京)科技有限公司

万丈高楼平地起:从“输入-处理-输出”第一性原理,看懂系统架构的演进

poemyang

高并发系统 高并发架构

用Dify工作流打造你的AI测试智能体,效率提升500%

测试人

Databend 十月月报:存储过程正式可用,数据流程全面自动化

Databend

一款AB实验分析智能体是如何诞生的

京东零售技术

蒲公英异地组网路由器全新固件:4G联网、策略路由、日志管理全面升级

科技经济

知识付费网盘变现微信小程序系统:资源变现与流量裂变解决方案

微擎应用市场

2026跨境出海新趋势:社交电商、AI赋能与可持续性成破局关键

Wolink

跨境电商 品牌营销 海外社媒营销 海外营销推广 达人营销

面试官狂问的 28 个 RAG 问题全解析:从基础到架构优化,一次讲透!

测吧(北京)科技有限公司

标准文库与评审管理系统:为技术团队装上“最强大脑

上海拔俗

别被“万能”忽悠了!超融合选型忽视这2点,未来升级可能“寸步难行”!

智驱前线

【FAQ】HarmonyOS SDK 闭源开放能力 — Push Kit

HarmonyOS SDK

HarmonyOS SDK应用服务

KCD 杭州站 x OpenInfra Days China 首次联手!华为云云原生团队与您共探Karmada多模板工作负载多集群管理方案

华为云原生团队

云计算 容器 云原生

盘点企业级远程控制方案,哪一款最安全?

科技经济

党建学习一体化解决方案:答题积分 + 学习管理微擎应用详解

微擎应用市场

AI 相片大师小程序:智能影像黑科技,解锁娱乐与变现双重价值

微擎应用市场

荣耀应用市场《应用隐私高频问题及自检指南 (第一期)》丨开发加油站

荣耀开发者服务平台

应用审核 荣耀开发者服务平台 荣耀应用市场 应用隐私合规 应用违规场景解读

「从画面生成到叙事生成:PrompTale的内容生产新范式」

极客天地

谷云科技深度参与编制《多源异构数据融合技术规范》团体标准,共创数据融合技术标准

谷云科技RestCloud

技术标准 数据安全 数据融合 ETL 多源异构

当搜索遇见 AIGC:京东零售的“千人千面”素材生成实践

京东零售技术

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