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

2022-06-30 11:11:01 +08:00
 fpure

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

9675 次点击
所在节点    程序员
106 条回复
jjwjiang
2022-06-30 16:30:37 +08:00
@MonoLogueChi ts 比你想象的做的多,楼主的例子是完全能行的,就是加一个 if(x==10)就行了。

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

我是不明白 rust 的例子楼主很明白是咋回事,却对 ts 同样的特性视而不见
exonuclease
2022-06-30 16:33:03 +08:00
x=10 是一个运行时的赋值 你也可以写 x=Console.Read() 那编译时怎么办 你想要的功能需要支持编译时常量 然后应该就可以推断出 x 的类型是 10 比如 c++的 constexpr
exonuclease
2022-06-30 16:36:07 +08:00
或者你可以加个判断 这种情况下 x 是能收窄到 10 的
let x: number
x = 10
function f(x: 10) { }
if (x == 10) {
f(x)
}
Alander
2022-06-30 16:50:04 +08:00
我认为这个问题真的也是挺有意思的,是否可以考虑成解析成本的原因?
如果 const i = 10; 静态解析后 i 不可能变成其他 number 所以不会报错,let 就可能被重新赋值而不符合字面量类型。
从这个结论来说是不是可以认为 ts 只做到了 let/const 的区分,而没有在静态词法分析上更近一步去分析代码运行到这一行 i 到底是不是 10 。
DianQK
2022-06-30 17:47:11 +08:00
按照 rust 的这个例子来看,这个是静态分析的工作,例子中的检查应该已经做到了
DianQK
2022-06-30 17:50:22 +08:00
@Alander 这个分析工作会在 IR 上进行,这一层相比词法、语法分析上能额外获得控制流等信息,进而判断变量是否有可能不在 10 的这个范围呢。
DianQK
2022-06-30 17:56:45 +08:00
btw 如果 op 对这些感兴趣刚好可以看下 [南京大学《软件分析》课程 01 ( Introduction )-哔哩哔哩] https://b23.tv/yNGs4E8
周一我刚看完全部课程,非常棒的教学资源
unco020511
2022-06-30 19:03:55 +08:00
这个其实不叫类型收窄,应该叫『类型智能转换』,但不是你这样的用法,智能转换的前提你先调用类似 if(x is 10)这样的判断,或者 assert(x !is 10)这样的断言,这样你下面就可以直接调用 f(x),无需手动调用 x as 10;如果按照你的说法,那编译器在编译期要做的检查可太多了,因为从定义变量到使用变量之间,可能还有 n 多赋值操作,不可能每次复制都记录下来的.得不偿失
unco020511
2022-06-30 19:16:23 +08:00
@unco020511 其实也不是不能做到自动判断,但也会限制在很小的部分场景。不能有多重赋值,因为可能有很长的一个赋值链条,最终真实的值甚至 io http 之类的,编译器在编译期该如何追踪真实值类型呢?所以,回到原点,限制 const 之类的静态值才能适用于自动判断。
opengg
2022-06-30 19:22:41 +08:00
你想要的是在编译期基于数学集合( set theory )去推导类型吧。
这叫做 set theoretic programming 。
在我非常浅薄的认知范围内,确实没有这样的编程语言。
littlewing
2022-06-30 19:28:43 +08:00
用 C ,所有参数用 void*
Dragonphy
2022-06-30 20:10:42 +08:00
OP 应该是想 f(x=10){} 这样声明吧,还是故意这么做?
codehz
2022-06-30 22:37:19 +08:00
OP 的想法大体上是理解了,先不说理论上有没有 soundness ,这个想法实用性还是有一点的(大体上就是可选运行时断言的弱化版的细化类型方案)
不过话说回来,现在编译器智能程度大概已经能消除掉很多额外的断言了)
而无法消除的,再用手工标记的方式去消除,倒也是一种可能的选择
初步实现形式可以采用细化类型标记,然后采用 sat 求解器去做静态检查,无法证明的部分则生成运行时断言,即可兼顾正确性和运行时性能
还需要补充的部分,大概就是断言失败的处理了,传统异常模型在这里恐怕不能适用,所以可能需要一些特殊控制流构造来描述
DOLLOR
2022-06-30 23:03:26 +08:00
TS 已经做了呀。

const func = (a: 10) => { }

let n: number;
n = 10;

// 这里加 if 判断就能收窄,不需要断言。
if (n === 10) func(n);
FrankHB
2022-07-01 03:44:58 +08:00
所有(静态)类型系统在遇到类型规则不符合需求时都会出现这类问题。越是如 Robert Harper 强调“静态”的正统性,遇到这个问题越会诛心。
这其实是大部分搞 PL 的都没搞清楚的实用通用语言设计中的核心问题(关键词:intrinsic and extrinsic views of typing )。相比来说,大部分 PL 壬所谓的 soundness 、totality 之类的问题,是很次要的。
根本解决方法是在基础设计中完全放弃带有静态类型系统的静态语言,让类型系统规则自身可编程。
作为魔改现有“无类型”动态语言发家的 TS ,恰恰是所有语言中这类问题最小的一类。不过即便是这样,要绕过去也基本意味着用户需要自己实现 JS 到 TS 的转换,因为 TS 的设计没有考虑到它自身这部分足够模块化而让便于用户复用(做成 JS 或 TS 的库),以节约重新实现类型系统的开销。
顺便,所谓 gradual typing 只是一种妥协,原则上并不确保用户可修改类型系统规则。
FrankHB
2022-07-01 03:48:23 +08:00
@codehz 既然都会加标记断言了,那为什么不更进一步,直接用 contract 而不是变着法子搞什么 refinement 得了(cf. Racket)?
到了这一步,这里真正麻烦到值得计较的反而是怎么确保 proper tail call 之类的更全局的性质,大部分类型论特性反而不重要了。
dangyuluo
2022-07-01 03:51:36 +08:00
C++里的`integral_constant`就没有歧义了
FrankHB
2022-07-01 04:20:10 +08:00
@dangyuluo 这就是哪壶不开提哪壶了,C++的那种强 phase (of translation)隔离的做法反而是最让我火大的糟心解。
虽然表面没 OP 的问题,实际上更恶心了:用户完全被剥夺了跨 phase 表达同一实体的抽象能力。
比如就想要精确表达 10 这个抽象的数,用 C++源码是做不到的。传统的 C/C++中,用户被迫在 pp-number 10 、integer-constant 10 作出抉择,而 C++加了一种介于两者之间的、光是语法上就明显更欠扁的 integral_constant<int, 10>,更加混乱(考虑到 template-template parameter 的无能,metafunction 不方便 partial application ,integral_constant 第一模板参数还特别不方便参数化地使用,更显得 int 这种“强类型”就是在没事找抽刷存在感)。
结果就算不考虑被静态类型污染的问题,真要通用,就得向上游迁移——及早确定然后顺下来给各个 phase 用(还照样省不掉显式“转换”),实际就意味逻辑就尽量塞预处理器了。这也就是一个整数,如果塞不进预处理器呢?
(想到 endianness 没法尽量只靠可移植的 template metaprogramming 实现最后还是得 std::endian 加 pp phase 层次的魔法这点,就气不打一处来。)
FrankHB
2022-07-01 05:09:58 +08:00
再借楼发(跑)散(题)超纲一点,我想特别显示一下在 lang spec 里钦定 phase 这个做法的实际历史性后果,以说明它是如何比 PL 壬沉溺(钦定设计的) type system 和相关研究更优先值得黑的。

钦定 phase 的一个显著后果单方面由语言设计者决定了何为“静态”,而没有用户议价的空间,导致不切实际的无效工作。
一旦不满足用户需要,要维持可编程性,就需要 ad-hoc (致敬 ad-hoc polymorphism ,表示“不一定就是坏的”,但实际大家都懂的)的 reflection 机制来变通。
这种机制基本也只可能由 spec 钦定,于是设计语言时就凭空多出来本不必要的一大坨的 API 设计(经常还没法避免主观性,特别是甄选什么 feature subset 配被 reflect )的工作:工作量大体 O(n^t),其中 t 是 phase 数,常量和其它特性正相关。(虽然大 O 是渐进上界,但常数可不小,一般要可用也够受的了。)
大部分语言中 t=2 ,被隐含钦定的 phase 是 phase of translation 和 phase of execution 两个,这也是一般所谓语言是否可被视为“静态”的分野。光是这个就制造出了反射这种原本就是同一个直接语义直接元编程的就能“免费”实现(源语言语法满足 homoiconicity 时)的工作。而 C/C++这种直接钦定一大坨 phase 的做法更加突出了所谓 compilation-time reflection 的更欠抽的“高阶”无谓设计和实现工作量。(当然,C 一直装死摆烂,这里可以算了。)(还好,除了 C++主流语言里还有谁那么乱的么……)
第二个后果是简单粗暴的 phase 蕴含了粗放式分层架构,即便实际的需求中,各个 phase 的问题域具有局域性,而并不要求语言规则具有明确的分层结构。
这是 reflection 这样的机制难以被其它形式的元编程替代的另一个原因。
这里有个类型系统外过于“静态”的例子:hygienic macro 再强,就算 host lang 再 homoiconic ,基本也得多一个 template sublanguage (而增加无谓设计和用户学习的工作量)——很大程度是多了个 expansion-time phase 的锅。
作为对比,bind-time analysis 中多出来的就是 local stage ,不添加类似的缺陷。
第三个后果是对实现结构的影响(不过其实 C 这种传统设计其实算是直接泄漏了实现的设计),尤其是造成片面拔高 AOT 编译的能力的偏见,工程上力大砖飞,搞不好就加人,全然不管项目规模扩大的代价,特别是路径依赖。
(幸甚,multi-staged ML/reflective Lisp 之流从来不成气候,所以毒害的主要也就局限在传统“静态”语言实现了……)
当年编译器理论界对 nanopass 的普遍怀疑也说明这不仅仅是工业界见识短的问题,“理论界”也整体就跑偏了。
近年来 PyPy 和 Graal+Truffle 这样更正统(指 variants of Futamura projection )的计科传统艺能(指无情地自动化加抽象)重新上线,让一些实现者认识到现有方法论的欠缺(你人再多能打得过自动化翻译解释器成量产优化编译器么),算是自底向上地打了脸。
遗憾的是,这个问题在工业界距离彻底纠正差得远了:可预见的未来内要指望主流工业界开窍避免依赖 GCC 和 LLVM 这样的力大砖飞式历史包袱是十分不现实的。

其它理论碎碎念:github.com/FrankHB/pl-docs/blob/master/en-US/calling-for-language-features.md#phases-and-stages (关于这些问题如何破坏语言的通用性,Ctrl+F smoothness 。)
pkoukk
2022-07-01 10:44:47 +08:00
还是 ts 对你太宽松了让你能写出这样的代码....

这是一个专为移动设备优化的页面(即为了让你能够在 Google 搜索结果里秒开这个页面),如果你希望参与 V2EX 社区的讨论,你可以继续到 V2EX 上打开本讨论主题的完整版本。

https://tanronggui.xyz/t/863142

V2EX 是创意工作者们的社区,是一个分享自己正在做的有趣事物、交流想法,可以遇见新朋友甚至新机会的地方。

V2EX is a community of developers, designers and creative people.

© 2021 V2EX