这是一个创建于 912 天前的主题，其中的信息可能已经有所发展或是发生改变。
以这段 typescript 代码为例，f 期待一个类型为 10 的参数，x 等于 10 ，但是因为 x 的类型为 number ，所以不匹配
第 1 条附言 · 2022-06-30 13:27:18 +08:00
无关 typescript ，这里只是用 typescript 举个例子，主要是为了了解类型系统研究中对于此类问题的一些解决方案和成果
第 2 条附言 · 2022-06-30 14:17:49 +08:00
许多人没理解我的问题，我当然知道什么是静态类型，这里需要做类型断言，我的问题是有没有可能制造一种类型系统在实际类型匹配的情况下自动地做这个类型断言
第 3 条附言 · 2022-06-30 15:59:00 +08:00
我举另外一个例子：rust为了防止未定义行为，会默认在运行时对数组访问进行边界检查，越界就panic（可关闭）。毫无疑问如果有大量的数组访问的操作发生将会影响性能。考虑下面这段代码：
let mut x: [i32; 10];
x[y]
那么如果能在编译时y的范围，即如果确定y小于10则通过检查，如果不确定则要求用户添加范围守卫
let mut x: [i32; 10];
if y < 10 {
x[y]
}
就可以取消边界检查且不产生未定义行为
106 条回复 • 2022-07-03 19:57:55 +08:00
 |
101
hst001 2022-07-01 10:47:50 +08:00
number 是一个集合，10 是 number 的一个子集，两个集合不相等，所以类型检查不通过是对的，如果能在编译期能确定下来 x 是集合 10 的元素之一就没有问题，比如修改 x 定义：
const x = 10 |
 |
102
frzh 2022-07-01 11:32:41 +08:00
1. 如果这里 x 是确定不能再赋值其它的值自动收窄当然是可以的，但是编译器要付出检查的代价，实际编码有比这更复杂的情况，但是编码的人却能简单的做个判断就能解决此问题。
2. 如果 x 是完全放飞的，那要是执行 f()的时候不是 10 怎么整。 |
 |
103
xgdgsc 2022-07-01 14:34:05 +08:00 via Android
julia multiple dispatch 用了都说好
|
 |
104
qbug 2022-07-01 17:14:30 +08:00
你需要 dependent types ，你这个需求在 idris 语言里可以被完美地满足 https://www.idris-lang.org/ 所谓类型驱动的开发。其实就是引入了形式化验证包括自动定理证明技术，在某些工业和区块链场合是挺重要的。
|
 |
105
icatme 2022-07-03 09:41:08 +08:00 via Android
楼主你要的是集合类型吧，
你用离散数学语言表述应该更多人能理解， 没现成可用就写一个呗， 现在这个类型 10 太辣眼了 |
 |
106
hackape 2022-07-03 19:57:55 +08:00 via iPhone
有可行性，但只会在有限范围内。TS 的类型收窄，就是静态分析器有限度的做了一点运行时的工作：a) 读懂 if condition; b) 收窄的有效期需要跟踪变量是否在判断后没有改变。类似的，rust 的 lifetime 检查其实也是部分在做运行时的一些 context sensitive 的工作。
所以现在的问题就是，你愿意付出多大的代价维护这个 context ？从实用角度讲，你肯定不能要求静态分析器去追求运行时等效，那性能就没法保障。 咱还拿 TS 类型收窄举例 ```ts if (x === 10) { x = 10 f(x) } ``` 加上 `x = 10` 就会报错，说明 TS 的实现逻辑就是，老子刚检查完你别动这变量啊，动了我就不保证了。那你说它读的懂 `x === 10` 能不懂 `x = 10` 吗？肯定不能啊，只是它选择不去懂。 思考一下 OP 想要的功能怎么实现，就是要求静态检查器跟踪变量的运行时赋值，除了检查 assignability 还要把 literal value 挨个记住。形如下例会付出多大代价呢： ``` x = 1 f1(x) x = 2 f2(x) x = 3 f3(x) ``` 考虑性能，backtrace 大概率不会用因为慢，那就用 cache ，赋值几次 cache 几次，就算不考虑循环，赋值这么频繁出现的操作，内存肯定要爆炸。综上，我认为是有理论可行性的，但不经济。 反观类型收窄，是进入 if block 的时候才启用，并且只 cache 一个值，干净又卫生，所以就实现了。 |
Select Language