写点什么

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

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

关注

评论

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

张宏江谈AI创业:人工智能亟需工程化,创业者大有可为

硬科技星球

技术分享| 应急指挥调度平台需要这些技术支撑

anyRTC开发者

音视频 快对讲 语音对讲 调度系统 视频对讲

湖南省株洲市有等保测评机构吗?咨询电话多少?

行云管家

网络安全 等保测评 等级测评 株洲

MySql主从同步介绍

京东科技开发者

MySQL 数据库 主从同步

买家手册:企业在选择 SBOM 供应商时需要注意什么?

SEAL安全

DevSecOps 开源软件供应链 软件物料清单 SBOM 软件供应链安全

程序员常用的IDE工具,你了解哪些?

Speedoooo

小程序 ide 开发者工具 前端开发工具

使用 HTML、CSS 和 JavaScript 的简单模拟时钟

海拥(haiyong.site)

开源 8月月更

跟我学Python图像处理丨基于灰度三维图的图像顶帽运算和黑帽运算

华为云开发者联盟

人工智能 图像处理 图像 三维

教你如何轻松实现多队伍排队管理【必看】

天天预约

微信小程序 排队 排队工具 #SaaS应用

ARMS助力羽如贸易打造全链路可观测最佳实践

阿里巴巴中间件

阿里云 云原生 可观测 Arms 客户案例

传媒数字化转型思考:小程序是音视频内容的更优载体技术

Speedoooo

小程序 数字化转型 小程序生态 传媒

数字人民币如何影响传统支付?支付厂商数字人民币应用案例征集

易观分析

金融 数字人民币 传统支付

极盾·析策,XDR的正确打开方式

极盾科技

网络安全 安全 数据安全 xdr

基于DevCloud进行黑白棋实时对战游戏开发实践

科技怪咖

推荐 | 移动开发主流热更新技术

Speedoooo

小程序 APP开发 热更新

转转风控「违禁物品识别」 背后的那些事儿

转转技术团队

人工智能’

秒验丨使用简介与应用创建

MobTech袤博科技

android iOS SDK 秒验

Louvain算法在反作弊上的应用

百度Geek说

大数据 算法

小企业自动化运维管理用什么软件好?有便宜的吗?

行云管家

IT运维 行云管家 自动化运维 小企业

火热与争议并行,XDR路在何方?

极盾科技

网络安全 安全 信息安全 数据安全 xdr

重磅发布!阿里云全链路数据湖开发治理解决方案

阿里云大数据AI技术

大数据 阿里云 数据湖 数据分析

让GitHub炸锅的深入理解MySQL实战手册,竟出自阿里云“藏经阁”

冉然学Java

Java MySQL 高可用 阿里 构架

用小程序打造超级App,助力社交电商扩大“留量池”

Speedoooo

小程序 社交电商 超级app 用户留存

SpringBoot进阶(叁):Spring Boot启动过程分析

No Silver Bullet

spring-boot 8月月更

直播系统源码——重视哪些功能的开发?

开源直播系统源码

软件开发 直播系统源码 直播功能

企业实践|基于软件研运一体化DevOps平台的应用解析

云智慧AIOps社区

DevOps 自动化 敏捷开发 研发管理 代码托管

汉诺塔(递归+ 非递归版)

Five

算法题 8月月更

Android进阶(十七)Android 布局

No Silver Bullet

android android布局 8月月更

什么是IP 欺骗以及如何防范?

郑州埃文科技

网络安全 IP

带你玩转“超大杯”ECS特性及实验踩坑

科技怪咖

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