BT

如何利用碎片时间提升技术认知与能力? 点击获取答案

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

| 作者 Sergio De Simone 关注 6 他的粉丝 ,译者 盖磊 关注 1 他的粉丝 发布于 2017年11月17日. 估计阅读时间: 4 分钟 | QCon北京2018全面起航:开启与Netflix、微软、ThoughtWorks等公司的技术创新之路!

亲爱的读者:我们最近添加了一些个人消息定制功能,您只需选择感兴趣的技术主题,即可获取重要资讯的邮件和网页通知

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

评价本文

专业度
风格

您好,朋友!

您需要 注册一个InfoQ账号 或者 才能进行评论。在您完成注册后还需要进行一些设置。

获得来自InfoQ的更多体验。

告诉我们您的想法

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我
社区评论

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我

讨论

登陆InfoQ,与你最关心的话题互动。


找回密码....

Follow

关注你最喜爱的话题和作者

快速浏览网站内你所感兴趣话题的精选内容。

Like

内容自由定制

选择想要阅读的主题和喜爱的作者定制自己的新闻源。

Notifications

获取更新

设置通知机制以获取内容更新对您而言是否重要

BT