AI实践哪家强?来 AICon, 解锁技术前沿,探寻产业新机! 了解详情
写点什么

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

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

关注

评论

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

鸿蒙开发笔记之Preview Kit在美颜相机中的应用

yimapingchuan

HarmonyOS NEXT

鸿蒙开发实战之Weather Service Kit实现美颜相机智能场景优化

yimapingchuan

HarmonyOS NEXT

YashanDB数据库与云服务的深度集成方案

数据库砖家

鸿蒙开发日记之Push Kit实现美颜相机消息推送

yimapingchuan

HarmonyOS NEXT

YashanDB数据库与微服务架构集成最佳实践分享

数据库砖家

YashanDB数据库与云计算平台的完美融合

数据库砖家

HPE OneView 10.0 OVA 部署

sysin

OneView

Nexpose 8.10.0 for Linux & Windows - 漏洞扫描

sysin

Nexpose

鸿蒙开发实战之Asset Store Kit实现美颜相机素材智能管理

yimapingchuan

HarmonyOS NEXT

YashanDB数据库与云平台的无缝集成指南

数据库砖家

AI数据分析训练营毕业总结

hunk

AI数据分析训练营毕业总结

JEB Pro v5.30 (macOS, Linux, Windows) - 逆向工程平台

sysin

JEB

鸿蒙Next仓颉语言开发实战教程:设置页面

幽蓝计划

鸿蒙开发实战之Car Kit实现美颜相机车载互联方案

yimapingchuan

HarmonyOS NEXT

Burp Suite Professional 2025.6 发布,新增功能简介

sysin

burp

鸿蒙开发实战之Scenario Fusion Kit实现美颜相机多场景联动

yimapingchuan

HarmonyOS NEXT

鸿蒙开发实战之Wallet Kit实现美颜相机会员卡券功能

yimapingchuan

HarmonyOS NEXT

鸿蒙开发实战之Basic Services Kit实现美颜相机基础能力筑基

yimapingchuan

HarmonyOS NEXT

YashanDB数据库与主流编程语言集成方法

数据库砖家

F5 BIG-IP 17.5 LTS - 多云安全和应用交付

sysin

F5

F5 BIG-IP 下载汇总 - 业界领先的应用交付与安全服务

sysin

F5

HarmonyOS开发实战之Reader Kit实现美颜相机文档预览

yimapingchuan

HarmonyOS NEXT

HarmonyOS开发实战之Share Kit实现美颜照片分享

yimapingchuan

HarmonyOS NEXT

YashanDB数据库与微服务架构的结合应用

数据库砖家

一文搞懂SEO优化之站点robots.txt

村头的猫

搜索引擎 Google SEO 建站 robots.txt

YashanDB数据库与云服务集成实用教程

数据库砖家

这个 361K Star 的项目,一定要收藏!

Immerse

《HarmonyOSNext超能手册:一篇文章搞定Node-API跨语言!》

Turing_010

HarmonyOSNext性能核弹:用Node-API引爆ArkTS/C++跨语言

Turing_010

鸿蒙开发实战之Connectivity Kit实现美颜相机多网融合传输

yimapingchuan

HarmonyOS NEXT

鸿蒙开发实战之Crypto Architecture Kit构建美颜相机安全基座

yimapingchuan

HarmonyOS NEXT

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