Syl：用模态类型系统实现编译期依赖类型

Syl 是一门正在开发中的编程语言，目标是在模态类型系统中编码编译期计算，实现编译期依赖类型、运行时简单类型。Syl 受 András Kovács 的两级类型理论及 OxCaml 计划启发，编译器已在 GitHub 上发布。其类型系统含 staticity 与 erasure 两条模态轴，支持静态参数单态化，但因允许一般递归和 type : type，构造某类型的表达式并不构成对应命题的证明。