今天,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找到隐含的类型信息并给出类型推导结果。本文将从如下几个反面进行介绍:
- 类型的表达式;
- 如何从代码收集类型推断的相关信息;
- 推断并得到结果;
- 用类型推断信息对代码进行诊断。