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

[fpure]

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

[CodeCodeStudy]

你连问题都没表达清楚

[fpure]

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

[fpure]

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

[hsfzxjy]

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

[hxtheone]

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

[laqow]

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

[jjwjiang]

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

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

[ecnelises]

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

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

[fpure]

@imKiva 之前一直想学 agda🤣

[lin07hui]

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

[mizuhashi]

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

[karloku]

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

[libook]

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

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

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

[xz410236056]

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

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

[MonoLogueChi]

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

```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]

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

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

[mxT52CRuqR6o5]

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

[iamzuoxinyu]

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

[MonoLogueChi]

再补充一下，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]

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