InfoQ技术大会双节活动折上折,限时特惠,满10000-1000>> 了解详情
写点什么

Racket 6.11 提供了稳定的细化类型和依赖函数特性

2017 年 11 月 16 日

Typed Racket 是 Racket 语言的一种静态类型方言。 Racket 6.11 为 Typed Racket 提供了细化类型(Refinement Type)和依赖函数(Dependent Function)特性。

细化类型是一种关联了谓词(Predicate)的类型,所关联的谓词对于该类型的任一成员都成立。表述细化类型的通用语法是(Refine [v : t] p),定义了所有类型为 t 的值 v 满足谓词 p。

下面的函数给出了一个细化类型的基本例子,该函数确保了函数的返回值至少不小于每个输入值:

(-> ([x : Integer] [y : Integer]) (Refine [z : Integer] (and (>= z x) (>= z y))))在 Racket 中,也可以设置细化谓词(Refinement Predicate)为一些程序条件(Term),使得细化类型依赖于这些条件的值。例如,下面定义的细化类型中,只包括整数 42:

> (ann 42 (Refine [n : Integer] (<= n 42)))依赖函数类型(Dependent Function Type)使用类似于细化类型的语法,指定了函数参数间的依赖关系,或参数与函数范围间的依赖关系。在依赖类型中,不允许存在循环依赖关系。例如,下面定义的函数,可在不越界条件的情况下访问向量中的成员:

复制代码
(: safe-ref1 (All (A) (-> ([v : (Vectorof A)]
[n : (v) (Refine [i : Natural]
(< i (vector-length v)))])
A)))

当然,在函数签名中定义先决条件(Precondition)也可以达到同样的效果:

复制代码
(: safe-ref2 (All (A) (-> ([v : (Vectorof A)]
[n : Natural])
#:pre (v n) (< n (vector-length v))
A)))

Typed Racket 的创立者和维护者 Sam Tobin-Hochstadt 在 InfoQ 的访谈中,对此给出了如下解释:

依赖类型特性使 Typed Racket 可以检查程序的属性,这是几乎所有其它的语言都做不到的。我们正使用这些新信息,探索可能对程序做出的这类改进。希望使用 Typed Racket 中的细化类型和依赖类型,能给出更快、更可靠的软件。

在前期版本的 Racket 中,细化类型和依赖函数是以实验性特性提供的,现在已是默认提供。为获得最新的修复,建议用户定期更新到快照构建(snapshot build)。如果用户想要进一步了解Racket 6.11 中依赖类型的使用信息,一定要看一下 Andrew Kent 给出的介绍。正是 Kent 在 Tobin-Hochstadt 的指导下完成了这些特性的主要工作。

依赖类型是类型系统中的一个特性,它允许创建更具表达力的类型,以在编译时捕获更多软件缺陷。其它支持依赖类型的语言有 Idris、Coq 和 F*。同时, Haskell 对依赖类型的支持也在推进中

查看英文原文: Refinement Types and Dependent Functions Stable in Racket 6.11

2017 年 11 月 16 日 18:005744
用户头像

发布了 381 篇内容, 共 99.9 次阅读, 收获喜欢 231 次。

关注

评论

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

面试官:开发过Maven插件吗?我:开发过啊。。。

冰河

maven 插件开发 互联网工程

基于链表的有界阻塞队列 —— LinkedBlockingQueue

程序员小航

Java 源码 AQS 源码阅读 LinkedBlockingQueue

架构师训练营第三周作业

四夕晖

设计模式 极客大学架构师训练营

单例设计模式之枚举实现

A p7+

架构师训练营 1 期 - 第三周总结(vaik)

行之

极客大学架构师训练营

架構師訓練營 week3 作業

ilake

极客大学架构师训练营

周练习3

何毅曦

CSS 选择器 — 重学CSS

三钻

CSS 前端

组合设计模式编写程序

石头

极客大学 极客大学架构师训练营

架构师训练营 1 期 -- 第三周作业

曾彪彪

极客大学架构师训练营

[架构师训练营第 1 期] 第三周命题作业

猫切切切切切

极客大学架构师训练营

【架构师训练营第 1 期 03 周】 作业

Bear

极客大学架构师训练营

[架构师训练营第 1 期] 第三周学习总结

猫切切切切切

极客大学架构师训练营

深入理解Java虚拟机1——内存区域

超超不会飞

Java JVM

SQL 是什么

Rayjun

sql

架构师训练营第一周作业

四夕晖

架构师训练营 - week03 - 作业1

lucian

极客大学架构师训练营

Mac 配置环境变量未生效

hepingfly

Mac 环境变量 配置文件不生效

架构师训练营第三周总结

xs-geek

极客大学架构师训练营

编程的本质和未来

小宋头

架构师训练营 1 期 - 第三周作业(vaik)

行之

极客大学架构师训练营

学习笔记:架构师训练营-第一周

四夕晖

4+1架构视图 通用设计模型

架構師訓練營 week3 總結

ilake

Linux安装软件方法总结

MySQL从删库到跑路

Linux 源码 RPM安装 安装 yum

架构师训练营第三周课程笔记及心得

Airs

我导师推荐的经典之作——《数学之美》第二版-吴军

计算机与AI

架构师训练营 - week03 - 学习总结

lucian

极客大学架构师训练营

3.手写单例模式设计

博古通今小虾米

学习笔记:架构师训练营-第三周

四夕晖

设计模式 OOD

架构师训练营 1 期 -- 第三周总结

曾彪彪

极客大学架构师训练营

架构师训练营第三周作业

我是谁

极客大学架构师训练营

Racket 6.11提供了稳定的细化类型和依赖函数特性-InfoQ