写点什么

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

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

关注

评论

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

Go: g0, 特殊的goroutine

陈思敏捷

原理 Go 语言

《零基础学 Java》 FAQ 之 12-理解引用

臧萌

Java

k8s上运行我们的springboot服务之——cloud gateway

柠檬

k8s Spring Cloud

其实你就是我羡慕的别人

小天同学

个人成长 感悟 日常思考

我是如何拿下PMP认证和系统架构设计师考试的?

Nick

Flask-SQLAlchemy 多表对单模型

Leetao

Python flask 编程语言 flask-sqlalchemy

区块链2.0--以太坊概述

皮卡丘的猫

prometheus中honor_labels配置项的源码分析

陈思敏捷

Prometheus Go 语言

我的编程之路 -5(停滞)

顿晓

网络编程 操作系统 编程之路 停滞 三年

python实现·十大排序算法之快速排序(Quick Sort)

南风以南

Python 排序算法 快速排序

2020 年 5 月 23 日 Java 集合专题

瑞克与莫迪

Java

JUC整理笔记一之细说Unsafe

JFound

Java

圆圈正义 - 读后感

石云升

读书笔记 法律 公平 现实

new() 和 make的区别

陈思敏捷

源码 源码分析 Go 语言

《零基础学 Java》 FAQ 之 11-为什么构造方法中调用重载的构造方法必须得是在第一行

臧萌

利与弊-传统框架要不要部署在Serverless架构上

刘宇

Serverless Web

Go: 应该使用指针还是结构体副本?

陈思敏捷

struct 原理 pointer Go 语言

云直播平台的选型与使用

音视频专家-李超

Go: Trace包探秘

陈思敏捷

原理 Go 语言

Java环境搭建

编号94530

Java java8 Java环境 环境安装 jdk安装

工作=投资=创业?

二鱼先生

个人成长 工作思路 工作方式 创业心态 创业者

python实现·十大排序算法之插入排序(Insertion Sort)

南风以南

Python 排序算法 插入排序

《零基础学 Java》 FAQ 之 10-Scanner里nextInt的小坑

臧萌

Java

Mysql增量更新-ON DUPLICATE KEY UPDATE

BerryMew

MySQL 增量更新 ON DUPLICATE KEY UPDATE

谈谈控制感(8):元控制感

史方远

职场 心理 成长

看完这篇 Session、Cookie、Token,和面试官扯皮就没问题了

苹果看辽宁体育

https

RocketMQ - 什么是RocketMQ

Java收录阁

RocketMQ

游戏夜读 | 怎么让游戏跑起来?

game1night

你是个伪工作者么?

池建强

个人成长 伪工作者

Tekton 的工作原理

张晓辉

Kubernetes cicd 云原生

除了直接看余额,谁更有钱还能怎么比(一)

石君

零知识证明 多方计算 同态加密

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