Syl: зависимые типы на этапе компиляции без проверки тотальности

Compile-Time Dependent Types

Автор языка Syl предлагает модальную систему типов, где значения помечаются как static или dynamic и как erased или unerased. Это позволяет делать вычисления на этапе компиляции зависимыми, а в рантайме — простыми: функции со static-аргументами мономорфизируются. В отличие от Lean и Agda, Syl допускает общее рекурсию и type : type, поэтому типы не доказывают утверждения, зато не нужны проверка тотальности и иерархия вселенных.