2025上半年,最新 AI实践都在这!20+ 应用案例,任听一场议题就值回票价 了解详情
写点什么

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

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

关注

评论

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

瞧瞧人家用SpringBoot写的后端API接口,那叫一个优雅

程序知音

Java spring 编程 程序员 后端

性能测试如何创造业务价值

老张

性能测试 技术与业务

Web侧防御指南

穿过生命散发芬芳

7月月更 Web防护

服务可见可观测性

阿泽🧸

微服务 7月月更

scrcpy这款软件解决了和同事分享手机屏幕的问题| 社区征文

尼露

Python XML-RPC实现简单的远程调用过程

宇宙之一粟

Python 7月月更

JDBC

武师叔

7月月更

Modbus协议通信异常

神农写代码

好玩的免费GM游戏整理汇总

echeverra

游戏

深刻理解 Linux 进程间七大通信(IPC)

C++后台开发

网络编程 linux开发 Linux服务器开发 C++开发 进程通信

Vuex(一)

小恺

7月月更

leetcode 650. 2 Keys Keyboard 只有两个键的键盘(中等)

okokabcd

LeetCode 动态规划 数据结构与算法

煮饺子与docker、kubernetes之间的关系

字母哥哥

Docker 容器化 #Kubernetes#

电商系统微服务架构

极客土豆

Mall电商实战项目全面升级!支持最新版SpringBoot,干掉循环依赖

程序知音

Java spring 编程 程序员 后端

【愚公系列】2022年07月 Go教学课程 001-Go语言前提简介

愚公搬代码

7月月更

疫情封控65天,我的居家办公心得分享 | 社区征文

程序员海军

远程办公 远程开发 初夏征文

关于我

程序员半支烟

【算法刷题日记之本手篇】组队竞赛与删除公共字符

未见花闻

7月月更

linux-riscv-5.17 纯净源码

贾献华

7月月更

王者荣耀商城异地多活架构设计

Fan

架构实战营

Web2.0的巨头纷纷布局VC,Tiger DAO VC或成抵达Web3捷径

鳄鱼视界

L3立法试水,为自动驾驶产业带来什么?

脑极体

「Docker 那些事儿」容器很难理解?带你从头到尾捋一遍

Albert Edison

7月月更

Django 表单

海拥(haiyong.site)

django 7月月更

Python|语言元素、分支结构和循环结构

AXYZdong

7月月更

大话云原生之负载均衡篇-小饭馆客流量变大了

字母哥哥

Docker 负载均衡 云原生

秒杀系统设计

库尔斯

架构实战营

毕业总结

Dean.Zhang

如何优雅的写 Controller 层代码?

程序知音

Java 编程 程序员 后端

旧的Spring Security OAuth已停止维护,全面拥抱最新解决方案

程序知音

Java spring 程序员 微服务 后端

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