AI实践哪家强?来 AICon, 解锁技术前沿,探寻产业新机! 了解详情
写点什么

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

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

关注

评论

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

5G网络行业切片SLA初探

鲸品堂

5G 网络切片

开发者有话说|一名高中生的编程之路

Loken

个人成长

融云x白鲸《2022社交泛娱乐出海白皮书》

融云 RongCloud

互联网 白皮书 融云

龙湖千丁基于 ACK@Edge 的云原生智慧停车系统架构实践

阿里巴巴云原生

阿里云 Kubernetes 云原生

天猫精灵DIY--技能应用

六月的雨在InfoQ

天猫精灵 功能模型 9月月更 公共实体 语音交互

PLG SaaS 案例:如何实践外链自动增长策略?

程序员泥瓦匠

SaaS

IP地址和MAC地址都可以确定目标地址,为什么二者都在使用,舍弃一个是否可行?

阿柠xn

Mac IP 网络 协议族 9月月更

软件开发正确打开方式:低代码+微服务

力软低代码开发平台

数据产品经理那点事儿三(合集)

松子(李博源)

大数据 深度思考 高效工作 数据产品经理

手写vue-router核心原理

hellocoder2029

Vue

面试了一位4年Java的程序员,张口就要35K,还什么都不会...

收到请回复

Java 语言 & 开发 八股文

bootstrap input框回车后重新刷新页面问题

六月的雨在InfoQ

bootstrap Input 9月月更 表单提交

开发者测评:相比 Harbor,我选择 ACR 的三点原因

阿里巴巴云原生

阿里云 Kubernetes 容器 云原生 ACR

精品!阿里P7爆款《K8s+Jenkins》技术笔记,高质量干货必收藏

程序知音

旷世巨作!20多位架构师携手打造的“Java 面试核心宝典”限时开源

Geek_0c76c3

Java 数据库 开源 程序员 架构

中心化决议管理——云端分析

字节跳动终端技术

ios 研发效能 CocoaPods 制品库 云化服务

概述数据交换的构建策略

穿过生命散发芬芳

数据交换 9月月更

开发者有话说|成长之路

六月的雨在InfoQ

个人成长 开会 996 007 9月月更

2022秋招最新整理上千道Java面试攻略,近500页PDF文档

收到请回复

程序员 Java 面试 跳槽 语言 & 开发 秋招

Java | this和super关键字【深入理解子类和父类的继承关系】

Fire_Shield

super this 9月月更

【编程基础】利用Python实现阿姆斯特朗数的求解

迷彩

Python 9月月更 阿姆斯特朗数 水仙花数

信创升级 | 秒云与人大金仓完成兼容性互认证

MIAOYUN

数据库 信创 国产数据库 信创云 容器云平台

数据产品经理那点事儿二(合集)

松子(李博源)

大数据 深度思考 高效工作

com.alibaba.fastjson 对象转json剔除字段

六月的雨在InfoQ

问题处理 Fastjson index Elastic Search 9月月更

SAE 助力贵州酒店集团从容支撑贵州特产抢购

阿里巴巴中间件

阿里云 Serverless 云原生 SAE

Fluid 助力阿里云 Serverless 容器极致提速

阿里巴巴云原生

阿里云 Serverless 云原生 Fluid ASK

你用对了么?对象文件网关 VS 分布式文件存储

焱融科技

云计算 分布式系统 对象存储 高性能 文件存储

NFTScan 与 Banksea Finance 在 NFT 源数据层面达成战略合作

NFT Research

区块链 NFT 合作 web3

字节、美团、滴滴以及蚂蚁金服Java后端面试过程

收到请回复

Java 程序员 面试 项目 语言 & 开发

不会还有程序员不知道跳槽季靠这1700道java面试题就能平淌大厂吧

程序知音

Java java面试 后端技术 秋招 Java面试题

一比一手写迷你版vue,彻底搞懂vue运行机制

hellocoder2029

JavaScript

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