AICon上海|与字节、阿里、腾讯等企业共同探索Agent 时代的落地应用 了解详情
写点什么

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

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

关注

评论

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

区块链加持,鉴定溯源双保险,科技赋能茅台老酒成零售数字化标杆

CECBC

区块链 大数据 防伪溯源

字节跳动内部授课课件:附图讲解MySQL底层索引结构算法实现

小Q

Java MySQL 学习 编程 面试

区块链赋能医疗行业,区块链医疗应用场景开发

13530558032

贼好用,冰河开源了这款精准定时任务和延时队列框架!!

冰河

redis 中间件 消息队列 延时队列 Zset

新图灵测试背后,智能交互点燃了哪些产业可能性?

脑极体

Java踩坑记系列之线程池

Java老k

Java 线程池

贞炸了!上线之后,消息收不到了!

楼下小黑哥

Java RocketMQ MQ

2021年全球公有云终端用户支出将增长18% ;EMNLP 2020最佳论文:无声语音的数字发声

京东科技开发者

程序人生

一次浪费时间的面试

escray

程序员 面试 面经

“新鲜出炉”阿里面试终极指南V3.0,符合一线大厂面试点需求

小Q

Java 学习 编程 架构 面试

第十周作业

Geek_4c1353

极客大学架构师训练营

一位Java程序员在上家公司CRUD了3年,金九银十想要跳槽面试却屡屡碰壁,感觉很迷茫!网友:这是你安逸太久技术能力跟不上了!

Java架构之路

Java 程序员 架构 面试 编程语言

MySQL选错索引导致的线上慢查询事故

Zhendong

Java MySQL

字节面试数据结构与算法:B+树的删除和插入,不够详细你打我

小Q

Java MySQL 学习 面试 算法

《码出高效:Java开发手册》,每一位想要成为优秀开发工程师的程序员必须要看的一本小册!

Java架构之路

Java 程序员 架构 面试 编程语言

架构设计:高并发读取,高并发写入,并发设计规划落地方案思考

互联网应用架构

高并发读,高并发写

怎么做好一场分享或者培训

fq

前端如何实现一键截图功能?

徐小夕

Java 大前端 React

高速二维码报警定位系统开发,智能报警系统

13530558032

上周我面了个三年 Javaer,这几个问题都没答出来

yes

面试 RPC HTTP

奉劝各位Java工程师都要学习这份阿里内部绝密《百亿级并发系统设计》实战教程,大厂面试官可“不讲武德”!

Java架构之路

Java 程序员 架构 面试 编程语言

乘上这艘“智能体”之舟,即刻前往智慧未来

脑极体

JVM Metaspace内存溢出排查与总结

Java老k

Java OOM 内存溢出 metaspace

五年Java开发经验,裸辞准备半月面试阿里,阿里巴巴却“不讲武德”,居然面了我7轮,历经千辛万苦终于斩获P7及Offer

Java架构之路

Java 程序员 架构 面试 编程语言

甲方日常 55

句子

工作 随笔杂谈 日常

《华为数据之道》读书笔记:第1章 数据驱动的企业数字化转型

方志

数据中台 数据湖 数据治理

Python进阶——如何正确使用魔法方法?(下)

Kaito

Python

OAuth 2.0授权框架详解

程序那些事

OAuth 2.0 程序那些事 Oauth 授权框架 安全框架

训练营第五周作业

爱码士

训练营

《华为数据之道》读书笔记:序言

方志

数据中台 数字化转型 数据治理

架构师训练营第 1 期第 10 周作业

业哥

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