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

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

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

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

那么如果能在编译时y的范围，即如果确定y小于10则通过检查，如果不确定则要求用户添加范围守卫
let mut x: [i32; 10];
if y < 10 {
x[y]
}

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

类型为 10 是什么鬼

什么叫做类型是 10…

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

const x=10 as const;

f(x) 就不会报错了

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

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

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

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

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

像是符合直觉的报错

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

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

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

类型为 10 ，活久见。。。

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

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

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

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

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

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

特定情况下 TS 是可以通过类型收窄来帮助验证代码逻辑的， www.typescriptlang.org/docs/handbook/2/narrowing.html

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

stackoverflow.com/a/71569082

"我在想这里 x 的类型可不可能随着实际取值完美收窄，然后程序通过这样的类型系统自动证明程序的正确性"
完全可以 PROGRAM = PROOF

www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/INF551/course.pdf

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

as const

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

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

10 是 number 的子集。。。

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

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

＃14 这是显然可以的，但是在 ts 里不行。可以试试用 dt 语言
比如 agda: tio.run/＃＃XY09DoJAEIX7PcUrpYCopUQLo60xXoBMEMgmyywuS4GEzsYDeACvxkFcl/[email&＃160;protected]/[email&＃160;protected]fFaCr/[email&＃160;protected]

＃42 补充一下：“但是在 ts 里不行” 除非 as const

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

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

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

什么场景会这么写

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

我了解了一下 Refinement type ，有点意思，学到了👍

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

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

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

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

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

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

噢看错了你的问题

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

// 类型关系：Child extend Base

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

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

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

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

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

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

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

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

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

正确的做法是：

1. 使用 const 且不显式声明类型
   imgur.com/fud80Cr

2. 手动检查类型，让检查器自动 cast 类型
   imgur.com/j0YS8FN

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

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

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

你连问题都没表达清楚

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

只是随感而发，抛砖引玉

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

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

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

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

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

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

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

之前一直想学 agda🤣

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

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

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

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

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

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

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

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

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

let x: number;
x = 10;
function f(arg: 10){}
f(x) //报错

首先 x 的类型是 number ，值是 10 ，而 arg 的类型是 10 ，10 是 number 的子集，也可以按照其他语言，理解为 10 是继承 number 的一个子类，是两种不同的类型，我们再来重新写一下

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

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

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

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

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

再补充一下，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 ，肯定不会报错，这不就是你说的 “在实际类型匹配的情况下自动地做这个类型断言”

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

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

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

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

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

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

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

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

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

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

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

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

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

用 C ，所有参数用 void*

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

OP 的想法大体上是理解了，先不说理论上有没有 soundness ，这个想法实用性还是有一点的（大体上就是可选运行时断言的弱化版的细化类型方案）
不过话说回来，现在编译器智能程度大概已经能消除掉很多额外的断言了）
而无法消除的，再用手工标记的方式去消除，倒也是一种可能的选择
初步实现形式可以采用细化类型标记，然后采用 sat 求解器去做静态检查，无法证明的部分则生成运行时断言，即可兼顾正确性和运行时性能
还需要补充的部分，大概就是断言失败的处理了，传统异常模型在这里恐怕不能适用，所以可能需要一些特殊控制流构造来描述

TS 已经做了呀。

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

let n: number;
n = 10;

// 这里加 if 判断就能收窄，不需要断言。
if (n === 10) func(n);

所有（静态）类型系统在遇到类型规则不符合需求时都会出现这类问题。越是如 Robert Harper 强调“静态”的正统性，遇到这个问题越会诛心。
这其实是大部分搞 PL 的都没搞清楚的实用通用语言设计中的核心问题（关键词：intrinsic and extrinsic views of typing ）。相比来说，大部分 PL 壬所谓的 soundness 、totality 之类的问题，是很次要的。
根本解决方法是在基础设计中完全放弃带有静态类型系统的静态语言，让类型系统规则自身可编程。
作为魔改现有“无类型”动态语言发家的 TS ，恰恰是所有语言中这类问题最小的一类。不过即便是这样，要绕过去也基本意味着用户需要自己实现 JS 到 TS 的转换，因为 TS 的设计没有考虑到它自身这部分足够模块化而让便于用户复用（做成 JS 或 TS 的库），以节约重新实现类型系统的开销。
顺便，所谓 gradual typing 只是一种妥协，原则上并不确保用户可修改类型系统规则。

既然都会加标记断言了，那为什么不更进一步，直接用 contract 而不是变着法子搞什么 refinement 得了(cf. Racket)？
到了这一步，这里真正麻烦到值得计较的反而是怎么确保 proper tail call 之类的更全局的性质，大部分类型论特性反而不重要了。

C++里的integral_constant就没有歧义了

这就是哪壶不开提哪壶了，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 层次的魔法这点，就气不打一处来。）

再借楼发（跑）散（题）超纲一点，我想特别显示一下在 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 。）

还是 ts 对你太宽松了让你能写出这样的代码....