今天,scheme-langserver( https://github.com/ufo5260987423/scheme-langserver发布了一个最新版本 1.0.11,该版本中加入了 scheme 生态中第一个 gradual typing 实现。
以下内容摘自 scheme-langserver 的相关文档( https://github.com/ufo5260987423/scheme-langserver/blob/main/doc/analysis/type-inference.cn.md(没找到oschina的markdown编辑功能,公式和详情请到原页面查看):
工程直觉:Scheme-langserver如何实现类型推断
包括Java和Typescript等编程语言都有一个类型系统, 能帮程序员尽可能避免代码执行中的错误。这些系统上基于遵循Hindley-Milner Type System或者System F的一些基本理论构建。然而,艰涩的理论不能保证它们的全知全能。
对scheme语言这样一种“非类型语言(untyped language”,很多类型系统需要的信息并不能够轻易的从代码中找到:
(lambda (a (+ 1 a
显然,这段代码无法显式给出参数a的类型。或者说,a的类型是一个包含所有可能类型的全集something?(后续会说明这是啥)。这是因为scheme语言不像许多其他语言一样在字面上给出函数的参数的类型。如果是Typescript,为了给a标明类型number:
function(a: number{return 1+a}
许多scheme语言的同类(比如Typed-racket)会改变它们的语法并且要求像Typescript这样的语言一样在字面上给出类型信息。但是,scheme-langserver认为可能有另外的手段——当下的大多数scheme代码都在尽量遵循r6rs标准,这意味着可以依据标准中给出的函数(或者按照lisp家族的术语来说,过程)所具有的语义来猜测类型信息。回归上面的那段scheme代码,我们有如下推导:
显然+是r6rs标准中规定的一个函数。
- 一般公认这个函数的类型应该是(number? <- (number? ...。其中<-说明这是个函数的类型,它的左边是函数的返回值的类型,右边是函数的参数的类型列表。
- 假定那段scheme代码能够正常运行,那么a的类型就可以确定为number?。
这个推导过程将帮助scheme-langserver找到隐含的类型信息并给出类型推导结果。本文将从如下几个反面进行介绍:
类型的表达式;
- 如何从代码收集类型推断的相关信息;
- 推断并得到结果;
- 用类型推断信息对代码进行诊断。
编程笔记 » scheme-langserver 新版本:scheme 社区第一个可实用的 gradual typing