InfoQ技术大会年底储值活动来袭,单张门票最高省3240元 了解详情
写点什么

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

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

关注

评论

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

软件测试 | 测试开发 | 想测试入门就必须要懂的软件开发流程

测吧(北京)科技有限公司

测试

微信Windows端IM消息数据库的优化实践:查询慢、体积大、文件损坏等

JackJiang

sqlite 微信 网络编程 即时通讯 IM

云游戏产业链深度解析

Finovy Cloud

云计算 5G 云渲染 云游戏

小六六学Netty系列之Java 零拷贝

自然

Netty 网络 9月月更

Spring源码分析(九)lazy-init 在Spring中是怎么控制加载的

石臻臻的杂货铺

spring 9月月更

软件测试 | 测试开发 | 如何模拟真实使用场景?mock 技术来帮你

测吧(北京)科技有限公司

测试

软件测试 | 测试开发 | 抓包分析 TCP 协议

测吧(北京)科技有限公司

TCP 抓包分析

软件测试 | 测试开发 | app自动化测试(Android)--显式等待机制

测吧(北京)科技有限公司

测试

软件测试 | 测试开发 | app自动化测试(Android)-- 特殊控件 T识别oast

测吧(北京)科技有限公司

自动化测试 Android;

软件测试 | 测试开发 | 数据持久化技术(Java)

测吧(北京)科技有限公司

测试

软件测试 | 测试开发 | Jenkins 踩坑(三)| Email 配置与任务邮件发送

测吧(北京)科技有限公司

测试

主流定时任务解决方案全横评

阿里巴巴云原生

阿里云 Serverless 云原生

leetcode 104. Maximum Depth of Binary Tree 二叉树的最大深度(简单)

okokabcd

LeetCode 算法与数据结构

软件测试 | 测试开发 | RPC接口测试技术-Tcp 协议的接口测试

测吧(北京)科技有限公司

2022年8月国产数据库大事记-墨天轮

墨天轮

数据库 opengauss 国产数据库 达梦 polarDB

易周金融分析 | 多家银行试水特色网点揽客;自动驾驶颠覆传统车险模式

易观分析

自动驾驶 金融 银行 网点

软件测试 | 测试开发 | 一文带你了解K8S 容器编排(上)

测吧(北京)科技有限公司

测试

小六六学Netty系列之Java NIO(二)

自然

Netty 网络 9月月更

小六六学Netty系列之Netty群聊

自然

Netty 网络 9月月更

软件测试 | 测试开发 | 基于Requests与mitmproxy打造迷你接口测试框架

测吧(北京)科技有限公司

测试 Request

软件测试 | 测试开发 | 接口管理工具YApi怎么用?颜值高、易管理、超好用

测吧(北京)科技有限公司

测试 Mock

软件测试 | 测试开发 | 一文搞懂测试左移和测试右移的 Why-How-What

测吧(北京)科技有限公司

测试 安全测试

依赖类型语言Idris发布1.0版本_函数式编程_Sergio De Simone_InfoQ精选文章