写点什么

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

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

关注

评论

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

NOSQL - 第六周总结

孙志平

学会使用Vue JSX,一车老干妈都是你的

前端有的玩

Java Vue 大前端 技巧 React

CAP原则

熊威

架构师训练营」第 6 周作业

edd

极客大学架构师训练营

架构师训练营第6周作业

饶军

CAP

Kiroro

我学会了用Python预测股票价格

博文视点Broadview

Python 读书笔记 算法 数据分析

最右JS2Flutter框架——渲染机制(二)

刘剑

flutter 大前端 跨平台 探索与实践

NOSQL - 第六周作业

孙志平

Doris 临时失效 UML 时序图(训练营第六周)

看山是山

Doris

架构师训练营第六周总结

sunnywhy

学习总结 - 第 6 周

饶军

天猫小店、京东小店的问题分析

石云升

价值网络 新零售 天猫小店

一个成都程序猿写于离开北京一周年与26岁生日的这一天

why技术

生活 程序人生 北漂 成都

总结

Kiroro

架构师训练营第六周

大丁💸💵💴💶🚀🐟

图解:有向环、拓扑排序与Kosaraju算法

淡蓝色

Java 数据结构 算法

程序员的眼界真的不要,也不能只局限于技术

非著名程序员

极客时间 程序员 提升认知

GaussDB for DWS:内存自适应控制技术总结

华为云开发者联盟

大数据 数据湖 内存管理 sql 华为云

MySQL 高可用和分布式数据库(训练营第六课)

看山是山

zookeeper CAP 主从复制 主主复制 MySQL 高可用

static关键字真能提高Bean的优先级吗?答:真能

YourBatman

spring springboot SpringCloud 极客大学架构师训练营 Spring Bean

Apache Flink 是什么?

Apache Flink

flink

蟒周刊-429-Python 3.8.4 可用ed

ZoomQuiet大妈

Python 大妈 蟒周刊

CAP 原理及Doris 临时失效的处理过程

Acker飏

极客大学架构师训练营 CAP

架构师训练营第六周作业

sunnywhy

探秘 Spring 的 PropertyEditor

CoderLi

Java spring 后台

架构师训练营第六周作业

王铭铭

猿灯塔:spring Boot Starter开发及源码刨析(六)

猿灯塔

week6 学习总结 Nosql

Z冰红茶

CAP 原理

Z冰红茶

「1.4万字」玩转前端 Video 播放器 | 多图预警

阿宝哥

大前端 流媒体 Video播放器 HLS

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