依赖类型

类型可以依赖于值，比如"长度为 n 的数组"。能把更多性质编码进类型。