Dependent Type

Dependent Type 一般指代一类类型系统中的一个特定的特性，即支持【让类型依赖于值】。

广义的 Dependent Type 就是这个定义的字面意思所描述的那样，因此 C 语言的定长的栈上数组也属于 Dependent Type。 不过一般来说，带有 Dependent Type 支持的类型系统需要一个 Elaborator 来进行 bidirectional typechecking，基于 substitution 的 C++ 以及基于 decay 的 C 则没有这种特性。