3

这算不算是静态类型系统的缺憾

 1 year ago
source link: https://www.v2ex.com/t/863142
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.

V2EX  ›  程序员

这算不算是静态类型系统的缺憾

  fpure · 9 小时 29 分钟前 · 3956 次点击
img20220630105453.png

以这段 typescript 代码为例,f 期待一个类型为 10 的参数,x 等于 10 ,但是因为 x 的类型为 number ,所以不匹配

第 1 条附言  ·  7 小时 13 分钟前

无关 typescript ,这里只是用 typescript 举个例子,主要是为了了解类型系统研究中对于此类问题的一些解决方案和成果

第 2 条附言  ·  6 小时 23 分钟前

许多人没理解我的问题,我当然知道什么是静态类型,这里需要做类型断言,我的问题是有没有可能制造一种类型系统在实际类型匹配的情况下自动地做这个类型断言

第 3 条附言  ·  4 小时 42 分钟前

我举另外一个例子:rust为了防止未定义行为,会默认在运行时对数组访问进行边界检查,越界就panic(可关闭)。毫无疑问如果有大量的数组访问的操作发生将会影响性能。考虑下面这段代码:

let mut x: [i32; 10];
x[y]

那么如果能在编译时y的范围,即如果确定y小于10则通过检查,如果不确定则要求用户添加范围守卫

let mut x: [i32; 10];
if y < 10 {
  x[y]
}

就可以取消边界检查且不产生未定义行为

92 条回复    2022-06-30 20:10:42 +08:00
liyang5945

liyang5945      9 小时 25 分钟前   ❤️ 1

类型为 10 是什么鬼
Trim21

Trim21      9 小时 24 分钟前 via Android   ❤️ 1

什么叫做类型是 10…
tsanie

tsanie      9 小时 24 分钟前

是要参数默认值?那是 function f(x: number = 10),类型为 10 属实是没看懂。
cmdOptionKana

cmdOptionKana      9 小时 22 分钟前

楼主不如说说最终想实现怎样的效果。
idealhs

idealhs      9 小时 22 分钟前   ❤️ 6

我都不知道你在讲什么东西
LonelyShadow

LonelyShadow      9 小时 21 分钟前

这是考验 v 友们的 typescript 功底吗?😂
ryougifujino

ryougifujino      9 小时 21 分钟前   ❤️ 1

你给 x 声明一个显式类型 10 就可以了。这个代码的原因是 TypeScript 在 x 那里类型推断的是 number 类型。
jspatrick

jspatrick      9 小时 20 分钟前

如果 x 的值必须是 10 ,那 x 就没有传参的必要吧
Carseason

Carseason      9 小时 18 分钟前

```
let x: 10
x = 10
function f(x: 10) { }
f(x)
```
fpure

fpure      9 小时 18 分钟前

@jspatrick 一个例子罢了,这里的 x 还可以为 10|11 、全体偶数、全体能被 10 整除的数,如果类型系统可以表达的话
gydi

gydi      9 小时 17 分钟前

x 的值是 10 ,但是它的类型是 number ,意味着它的值可能是 0123456789 ,所以不匹配
IvanLi127

IvanLi127      9 小时 15 分钟前   ❤️ 2

我寻思,这不是很合理吗? 你的形参都要求类型是 10 了,number 里那么多数字,你不显式强转的话,那类型检查岂不是很没有面子?
ljsh093

ljsh093      9 小时 14 分钟前

入参的类型与 number 类型不同当然会报错
fpure

fpure      9 小时 13 分钟前

其实我是想讨论关于类型收窄、依值类型等话题,我在想这里 x 的类型可不可能随着实际取值完美收窄,然后程序通过这样的类型系统自动证明程序的正确性
TWorldIsNButThis

TWorldIsNButThis      9 小时 13 分钟前 via iPhone

字面量类型不是 number 类型的子类型
4196

4196      9 小时 12 分钟前   ❤️ 4

type x = 10 | 11;
let X: x = 10
function f(arg: x) { }
f(X)
TWorldIsNButThis

TWorldIsNButThis      9 小时 12 分钟前 via iPhone

@TWorldIsNButThis 说反了 是 number 类型不是字面量类型的字类型
Trim21

Trim21      9 小时 12 分钟前 via Android

没记错的话 10|11 在 ts 里面就个合法类型,你把 12 传进去是会报错的
Trim21

Trim21      9 小时 10 分钟前 via Android   ❤️ 2

const x=10 as const;

f(x) 就不会报错了

至于类型收窄等等等等 ts 也是会做的
mxT52CRuqR6o5

mxT52CRuqR6o5      9 小时 10 分钟前 via Android

不算
真正的静态类型语言的类型系统整不出这种操作
这个只能算 ts 类型系统,算不算遗憾还另说
4196

4196      9 小时 9 分钟前

我这个算你说的类型收窄吗?@fpure
chendy

chendy      9 小时 9 分钟前

没写过 ts ,试了一下还挺神奇,10 还真是个类型,而且唯一合法的值就是 10
但是什么叫静态类型系统的缺憾,把流程逻辑写在参数声明上感觉并不是什么好主意
yolee599

yolee599      9 小时 8 分钟前

看样子你是想设计一个万能函数,输入所有东西都能输出答案?
Jooooooooo

Jooooooooo      9 小时 7 分钟前

像是符合直觉的报错

难道你希望这个运行期再报错吗? 或者根本不报错?
stein42

stein42      9 小时 3 分钟前

如果 x 的值来自一个复杂函数,函数运行时间可能很久甚至无限。
如果 x 的值来自用户输入。
类型检查是在不运行程序的情况下对程序进行分析,能够在有限的时间给出结果。
类型检查是保守的,通过检查代表没有类型错误,不通过不代表一定有问题,ts 不通过检查也可以继续运行。

ps: ts 里面 10 是一个合法的类型,它只有一个值。
cheng6563

cheng6563      9 小时 1 分钟前

类型为 10 ,活久见。。。
nulIptr

nulIptr      8 小时 59 分钟前

类型不就是用来静态分析的吗,你给静态分析分析你这个 x 变量为啥是 10
wenzichel

wenzichel      8 小时 59 分钟前

小类型可以给更大范围的类型赋值,但反过来就不行了。

number 的范围很大,但 10 的范围就只有 10 。
chenmobuys

chenmobuys      8 小时 58 分钟前

虽然不是很喜欢 ts ,但是你这个吐槽也没到点子上去啊。
rrfeng

rrfeng      8 小时 56 分钟前

1. 逻辑没错
2. 问题存在
3. 毫无意义
aguesuka

aguesuka      8 小时 56 分钟前   ❤️ 3

是 ts 的, 但不是 type throery 的, 你需要的是 Refinement type
Envov

Envov      8 小时 52 分钟前

ts 里面宽的不能给窄的,f 函数只能接受 x 为 10 ,你传入的 x 类型 number ,它可能是 10 也可能是别的数
dcsuibian

dcsuibian      8 小时 48 分钟前

类型 10 和 number 可能会让其它与语言的用户产生困扰。换种说法:
现在有基类 A 和派生类 B ,函数 f() 只能接收一个派生类 B 的对象。此时变量 x 被声明为基类 A ,但实际里面放的是 派生类 B 的对象。
于是 f(x) 时报错了,因为编译器认为 x 不一定属于派生类 B 。
gzf6

gzf6      8 小时 44 分钟前 via Android

as const
dcsuibian

dcsuibian      8 小时 18 分钟前

你说“缺憾”的话也确实可以说是,但更准确地说就是“做不到的事”。就像人不会飞一样。

虽然在我们看来,x 必然是 10 ,因为里面只隔了一行无意义的函数定义。但对于编译器来说,要做出这种判断,隔一行与隔一千、一万行代码相同。它要做的是“理解中间的代码干了什么,会有什么影响”。而这的要求就太高了,基本可以踢掉一些低级程序员了。
CokeMine

CokeMine      8 小时 12 分钟前 via Android

10 是 number 的子集。。。
Pythoner666666

Pythoner666666      8 小时 10 分钟前

10 | 11 | 12 ....这些 只能算作 number 的子集
yazinnnn

yazinnnn      8 小时 3 分钟前

能编译通过才是类型系统的悲哀
imKiva

imKiva      8 小时 0 分钟前   ❤️ 1

@fpure #14 这是显然可以的,但是在 ts 里不行。可以试试用 dt 语言
比如 agda: https://tio.run/##XY09DoJAEIX7PcUrpYCopUQLo60xXoBMEMgmyywuS4GEzsYDeACvxkFcl/gTYzMzee@b96g4knO6yhiyrLSx2JClaEcWTS25wGS43GKcM6Nj1E0aiF/2kCmyUnO0lkymjfZGV7qWo0Rqe2pISdt@gpLhek9imCxXMVLNhQ9sy0CIHAtM2A9fFaCr/MXwMGbTHuFqlD3D6MbXHkuwEMkL93uJ3INv89@Yfw3nHmmuqKhdGLIOS5L8BA
imKiva

imKiva      7 小时 59 分钟前

@imKiva #42 补充一下:“但是在 ts 里不行” 除非 as const
uni

uni      7 小时 58 分钟前

目前为止人类的的程序静态分析的技术还没到这个水平吧,那只能期待未来的科研成果了
baobao1270

baobao1270      7 小时 45 分钟前

1. Python 不是静态类型,但是又 type hint ,在 Python 里是可以指定 literal value 的,比如类型为 str 且仅取值 "month" 和 "day"。支持泛型的语言,也大多支持泛型查询( where T : SomeClass )。
2. 如果要对函数输入的数据进行验证(比如“只能输入全体偶数”),正确的做法是在函数内验证,如果不通过就抛 Exception 。
3. 如果参数值的集合是有限可数的,比如 ACTIVE = 0, HIDDEN = 1, DELETED = 2, 那么应该使用 enum 而不是 int 。
abcbuzhiming

abcbuzhiming      7 小时 43 分钟前

类型系统不就是为了限制有些人啥也不管的往函数里任意传参的吗?改动楼主说的,那不又变成想传啥就传啥了?
zhuweiyou

zhuweiyou      7 小时 40 分钟前

什么场景会这么写
ifdef

ifdef      7 小时 35 分钟前

建议多读读 typescript 的文档,虚心一点,反复读几遍 union type 和 type narrowing 的相关内容。
fpure

fpure      7 小时 10 分钟前

@aguesuka 我了解了一下 Refinement type ,有点意思,学到了👍
Mexion

Mexion      7 小时 8 分钟前

这根本不是什么问题,参数类型为 10 ,那就一定得传 10 ,number 类型可以是任何数,凭什么让你传
haolongsun

haolongsun      7 小时 3 分钟前

。。能问出这个问题也是极品,你都定义类型只能是 10 ,你还要传进去 Number ,Number 可是 any ,定义域范围都不一样。
Kawa

Kawa      6 小时 55 分钟前 via Android

这算什么缺憾…
没有 runtime type check 才是 typescript 最大的缺憾, 作为一个所谓的强类型语言结果在运行时类型全给抹除掉, 然后该报错还得报错.
typescript 在编译期为了保证所谓的静态类型, 程序员不得不为了过编而编写更多的屎代码, 比如 document.append 完一个元素再 query 他需要判空, 不然不给过编.

这还不算, 这个例子比较极端.
你用 ts, 但是你用的模块是纯 js, 或者模块的 ts 类型写得跟屎一样, 那你这个模块就会用得特别痛苦, 如果处理不好, 这份痛苦就会在整个代码仓库里蔓延.

写了这么久 ts, 我还是觉得 ts 只配当一个文档工具, 在类型检查上 ts 只会让程序员浪费更多的时间跟 ts 编译器打架.
cenbiq

cenbiq      6 小时 50 分钟前 via iPhone

编译器没错,这是因为你的 let x 的声明类型是 number ,虽然你后期赋值为 10 ,但它的类型不是 10 而是 number 。
cenbiq

cenbiq      6 小时 47 分钟前 via iPhone

@cenbiq 噢看错了你的问题
nothingistrue

nothingistrue      6 小时 42 分钟前

给换一个简单的强类型语言来描述:

// 类型关系:Child extend Base

// 定义
void oneMethod(Child x){}

// 使用
Base y = new Child();
oneMethod(y); // 出现编译错误

然后你就会发现问题在哪里了,你给 y 定义了类型是 Base ,但用得时候却期望它是根据运行时推测出来的 Child 。

这怎么会是静态类型系统的缺憾,这正是强类型语言的基本特性。研究一个东西的特性是不是它的缺憾,这形同与研究人吃饭是不是有缺憾。楼主应该先学习一下强类型语言是什么。
fpure

fpure      6 小时 27 分钟前

@nothingistrue 你没理解我的问题,我当然知道什么是静态类型,这里 typescript 需要做类型断言,放到 Java 里面就是强制类型转换,我的问题是有没有可能制造一种类型系统在实际类型匹配的情况下自动地做这个类型断言、类型转换
Leviathann

Leviathann      6 小时 26 分钟前

这里的原因难道不是用户的手动标注优先级高于 tsc 的自动推断吗?而且 let 天然就是倾向宽松的推断
const a = 10
f(a)
就没问题

就算这么写
后面加一个
if ( x === 10 ) {
f(x)
}
也行,利用 tsc 的控制流分析
zsxeee

zsxeee      6 小时 22 分钟前

我猜你想要检查器在每次赋值的时候自动 smart cast 收缩类型。比如赋值为 10 相当于直接后面直接有了 (x === 10) 为 true 。可以理解但是是不可行的,这是让检查器猜测人的意图。

譬如 y 变量显式生命为 number ,赋值为 10 。但我逻辑上不允许将其传入 f() 中,这不是又回到人自己判断类型了吗?

正确的做法是:
1. 使用 const 且不显式声明类型
https://imgur.com/fud80Cr

2. 手动检查类型,让检查器自动 cast 类型
https://imgur.com/j0YS8FN
nothingistrue

nothingistrue      6 小时 22 分钟前

@fpure #56
先回答你这个 “我的问题是有没有可能制造一种类型系统在实际类型匹配的情况下自动地做这个类型断言、类型转换”:
有,就是动态类型语言或者弱类型语言,原生 JavaScript 就是典型。

然后你再回头看看你到底知不知道什么是静态类型。
otakustay

otakustay      6 小时 19 分钟前

这是控制流分析的问题了,其实是能够分析出来“调用 f 的时候 x 只有可能为 10”并过去的,但这个太损性能了,你不会想要的
CodeCodeStudy

CodeCodeStudy      6 小时 16 分钟前

你连问题都没表达清楚
fpure

fpure      6 小时 16 分钟前

@nothingistrue 算了,你还是没看懂我的问题
fpure

fpure      6 小时 14 分钟前

@CodeCodeStudy 只是随感而发,抛砖引玉
hsfzxjy

hsfzxjy      6 小时 12 分钟前 via Android

自动断言可以做,但这不是类型系统的责任
hxtheone

hxtheone      5 小时 51 分钟前 via iPhone

虽然 LZ 的问题我没看懂, 但是楼上 TS 的实现真惊为天人, 类型系统还能这样玩儿的
laqow

laqow      5 小时 47 分钟前

感觉 10 在:后面只是个符号,和它在阿拉伯地区的意义无关,没要求写成:"10"已经算 javascript 引擎很人性化了。用来赋值的时候应该是被隐式转换为 number ,同样没要求写成 number("10")也很人性化了。
jjwjiang

jjwjiang      5 小时 42 分钟前

你加个 if(x==10)不就行了吗? TS 是这方面做的最接近你的想象的语言了

TS 各种类型推断都是这么做的,到了你这个例子你怎么忽然就想不明白了?
ecnelises

ecnelises      5 小时 33 分钟前 via iPhone

楼主把 10 作为类型的意思更像是 Number<10>,即一个值只能为 10 的 Number ,有点 Dependent Type 那意思了。

@Kawa
TS 和 ES 类型标注提案都要求类型只当作静态注释,不影响引擎执行。至于说为什么,应该是避免影响动态类型的基本运行方式..
fpure

fpure      5 小时 29 分钟前

@imKiva 之前一直想学 agda🤣
lin07hui

lin07hui      5 小时 21 分钟前

取值自动收窄类型不利于代码维护和阅读
mizuhashi

mizuhashi      5 小时 17 分钟前 via iPhone

agda 的话可以,做法参考 42 楼,你需要构造一个 isTen 类型,然后穿参的时候提供一个这个类型的证明,如果你用 literal 来调用这个证明可以自动产生,但是别的运行时量证明需要你自己写
karloku

karloku      5 小时 6 分钟前

作为其他语言用户确实困扰了
但是按 10 是 number 的一个子类大概理解一下觉得这个才直觉. 宽引用转换到窄必须显式转换并且最好有相应的异常处理. 不然谁能保证 x: number 一定是符合 10 的
libook

libook      5 小时 4 分钟前

个人认为,核心问题在于类型和值通常是两种概念,且大多静态类型系统都预期开发者在声明类型的时候填的是类型,而不是值,比如严格来讲,x 的值是 10 ,但类型是 number ,TS 不认为类型“10”等价于值为 10 的 number 类型,就好比 10 平米面积不等价于底面积为 10 平米的体积。

如果非要这种特性的话,就得允许开发者不止在声明类型的地方写类型名称,而是可以写值,甚至表达式来算值,然后编译器负责按照值推算成对应的类型+值,再限制对应的类型,并额外增加限制对应的值。
这样会有个问题,类型系统就不止做类型校验的工作了,还杂糅了值校验的工作,就看语言的设计者和使用者是否接受这种设计了。

个人认为作为类型系统来说,做到类型校验就足够了,值校验本身就不是类型系统的份内事,真搞出来就应该不算“类型系统”了,而是另一种类型与值的复合系统。
xz410236056

xz410236056      4 小时 53 分钟前

“我的问题是有没有可能制造一种类型系统在实际类型匹配的情况下自动地做这个类型断言、类型转换”

你以为你写个类型 10 就是 数字 10 了?谁告诉你他俩实际上一样的,你写的是代码啊,不是实际的上的数啊。所以你想要一个,你写 10 ,计算机也知道他是个"数字"匹配上 number ?你这是人类思维。
MonoLogueChi

MonoLogueChi      4 小时 49 分钟前

我先按照我的理解,重新写一下这段代码

```js
let x: number;
x = 10;
function f(arg: 10){}
f(x) //报错
```
首先 x 的类型是 number ,值是 10 ,而 arg 的类型是 10 ,10 是 number 的子集,也可以按照其他语言,理解为 10 是继承 number 的一个子类,是两种不同的类型,我们再来重新写一下

```js
let x:10 = 10;
function f(arg: 10){}
f(x)
```
geelaw

geelaw      4 小时 42 分钟前

>我的问题是有没有可能制造一种类型系统在实际类型匹配的情况下自动地做这个类型断言

不能,因为判定“实际”类型是否匹配是不可计算问题(确切来说,否认“实际”类型匹配是不可识别问题)。如果只考虑有限定义域(因为实际的电脑是有限大小的内存之类的),确认“实际”类型匹配处于多项式层级的第二层并且是 Sigma_2 完备问题。
mxT52CRuqR6o5

mxT52CRuqR6o5      4 小时 37 分钟前

按照你 rust 的举例
typescript 也可以
if(x===10{f(x)}
这样就不报错了
iamzuoxinyu

iamzuoxinyu      4 小时 35 分钟前

Haskell 貌似有个 Refinement 扩展,可以参考下。我记得需要运行时支持。
MonoLogueChi

MonoLogueChi      4 小时 33 分钟前

再补充一下,ts 不太熟,以另一种强类型语言 C# 为例说一下。10 应该算是 ts 定义好的一种类型,在 C# 内,你说的这种 “在实际类型匹配的情况下自动地做这个类型断言”,应该被称为隐式转换,举个例子,比如说 byte 类型可以隐式转换为 int ,int 可以隐式转换为 long 。C# 中可以使用 implicit 关键字定义隐式转换,例子就不举了。再回到 ts ,同样有一个很著名的隐式转换 any ,我们再看一下上的例子

```
let x: number;
x = 10;
function f(arg: any){}
f(x)
```

x 类型从 number 隐式转换为 any ,肯定不会报错,这不就是你说的 “在实际类型匹配的情况下自动地做这个类型断言”
Ritr

Ritr      4 小时 16 分钟前

这种其实是类似于枚举的操作,一个 number 类型当然不能赋值给一个枚举类型
jjwjiang

jjwjiang      4 小时 10 分钟前

@MonoLogueChi ts 比你想象的做的多,楼主的例子是完全能行的,就是加一个 if(x==10)就行了。

而 ts 做不到楼主想要的连 if 都不要的推断,原因很简单,加了 if 能在编译前就能够正确推断,而不加 if 的话在编译前的推断不一定准确且有可能有代码是根本没法推断出值的。

我是不明白 rust 的例子楼主很明白是咋回事,却对 ts 同样的特性视而不见
exonuclease

exonuclease      4 小时 7 分钟前

x=10 是一个运行时的赋值 你也可以写 x=Console.Read() 那编译时怎么办 你想要的功能需要支持编译时常量 然后应该就可以推断出 x 的类型是 10 比如 c++的 constexpr
exonuclease

exonuclease      4 小时 4 分钟前

或者你可以加个判断 这种情况下 x 是能收窄到 10 的
let x: number
x = 10
function f(x: 10) { }
if (x == 10) {
f(x)
}
Alander

Alander      3 小时 50 分钟前

我认为这个问题真的也是挺有意思的,是否可以考虑成解析成本的原因?
如果 const i = 10; 静态解析后 i 不可能变成其他 number 所以不会报错,let 就可能被重新赋值而不符合字面量类型。
从这个结论来说是不是可以认为 ts 只做到了 let/const 的区分,而没有在静态词法分析上更近一步去分析代码运行到这一行 i 到底是不是 10 。
DianQK

DianQK      2 小时 53 分钟前 via Android

按照 rust 的这个例子来看,这个是静态分析的工作,例子中的检查应该已经做到了
DianQK

DianQK      2 小时 50 分钟前 via Android

@Alander 这个分析工作会在 IR 上进行,这一层相比词法、语法分析上能额外获得控制流等信息,进而判断变量是否有可能不在 10 的这个范围呢。
DianQK

DianQK      2 小时 44 分钟前 via Android

btw 如果 op 对这些感兴趣刚好可以看下 [南京大学《软件分析》课程 01 ( Introduction )-哔哩哔哩] https://b23.tv/yNGs4E8
周一我刚看完全部课程,非常棒的教学资源
unco020511

unco020511      1 小时 37 分钟前

这个其实不叫类型收窄,应该叫『类型智能转换』,但不是你这样的用法,智能转换的前提你先调用类似 if(x is 10)这样的判断,或者 assert(x !is 10)这样的断言,这样你下面就可以直接调用 f(x),无需手动调用 x as 10;如果按照你的说法,那编译器在编译期要做的检查可太多了,因为从定义变量到使用变量之间,可能还有 n 多赋值操作,不可能每次复制都记录下来的.得不偿失
unco020511

unco020511      1 小时 24 分钟前 via Android

@unco020511 其实也不是不能做到自动判断,但也会限制在很小的部分场景。不能有多重赋值,因为可能有很长的一个赋值链条,最终真实的值甚至 io http 之类的,编译器在编译期该如何追踪真实值类型呢?所以,回到原点,限制 const 之类的静态值才能适用于自动判断。
opengg

opengg      1 小时 18 分钟前

你想要的是在编译期基于数学集合( set theory )去推导类型吧。
这叫做 set theoretic programming 。
在我非常浅薄的认知范围内,确实没有这样的编程语言。
littlewing

littlewing      1 小时 12 分钟前

用 C ,所有参数用 void*
Dragonphy

Dragonphy      30 分钟前

OP 应该是想 f(x=10){} 这样声明吧,还是故意这么做?

About Joyk


Aggregate valuable and interesting links.
Joyk means Joy of geeK