在 2025 收官前,看清 Data + AI 的真实走向,点击查看 BUILD 大会精华版 了解详情
写点什么

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

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

关注

评论

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

PHP中的错误和异常

书旅

php 异常 常见错误

性能优化-技术专题-top和jstack分析高CPU问题

码界西柚

JVM

PM2 管理node.js开机自启动(非root用户)

不会写诗的王维

node.js

影响音视频延迟的关键因素(二): 采集、前处理、编解码

ZEGO即构

H264 API 3A算法

暴雪员工抗议薪酬不公,部分员工称甚至难以维持生计

程序员生活志

职场

python自动生成一整月的排班表

不会写诗的王维

Python

MySQL视图介绍

Simon

MySQL

史上最强DIY,手工制作一只会说话的机器狗

华为云开发者联盟

聊天机器人 nlp 华为云 语言识别 语言合成

关于自增id 你可能还不知道

Simon

MySQL MySQL自增ID

Linux Page Cache调优在Kafka中的应用

vivo互联网技术

大数据 kafka

他被称为"中国第一程序员",一人之力单挑微软!真牛!

程序员生活志

如何选择一台打印机

别把虾米不当海鲜

90后程序员小姐姐在线征婚!年薪70w!拥有五套房!她却担心自己因为年龄大嫁不出去!

程序员生活志

程序员

芯片破壁者(十三):台湾地区半导体的古史新证

脑极体

IOTA架构下的数据采集

易观大数据

一行错误代码:5 亿美元没了。。。项目关闭。。。

程序员生活志

【数据结构与算法】用动图解说数组、链表、跳表原理与实现

三钻

数组 链表 数据结构与算法 跳表

Spring-技术专题-Bean的生命周期简介

码界西柚

spring

5. JsonFactory工厂而已,还蛮有料,这是我没想到的

YourBatman

Jackson Fastjson JSON库 JsonFactory

MySQL-长事务详解

Simon

MySQL mysql事务

卡丁车的后轴是如何做到差速的?

TGP大跨步

科普 卡丁车 TGP 大跨步 素材

通过波士顿矩阵模型做产品定位

GuOjixIE

数据分析 产品定位 波士顿矩阵模型

揭秘MySQL主从数据不一致

Simon

MySQL 主从复制

哥尼斯堡七桥问题

NashSP

LeetCode题解:66. 加一,倒序遍历+可中途退出,JavaScript,详细注释

Lee Chen

大前端 LeetCode

基于Ambari的大数据平台搭建

数据社

大数据 hadoop ambari

设计模式-技术专题-建造者模式(Builder)

码界西柚

Java 设计模式

因为套用这个模板,我成了公司最佳员工

华为云开发者联盟

网站架构 华为云 网站搭建 匀速建站 SEO

LeetCode题解:11. 盛最多水的容器,双循环暴力法,JavaScript,详细注释

Lee Chen

大前端 LeetCode

更改用户host留下的坑

Simon

MySQL

[8.20]leetcode每日一题,

一起搞稽

算法 DFS

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