Автор экспериментального языка Syl предлагает перенести зависимые типы в systems programming через modal type system. Проект вдохновлён two-level type theory Андраша Ковача и планами OxCaml. В отличие от ограниченных constexpr, const generics и comptime, Syl делает compile-time computation частью единой системы типов.
У каждого значения есть тип и режимы по двум осям. Staticity различает static, известное компилятору, и dynamic. Erasure различает unerased, доступное во время выполнения, и erased. Литерал обычно static unerased, но система позволяет ослабить режим до dynamic или erased; обратное «усиление» без доказательства запрещено. Ветвление по dynamic-значению делает результат dynamic, а функция, возвращающая erased, сама становится erased и не может вызываться в runtime.
Static-параметры дают мономорфизацию: при вызове компилятор выбирает специализацию функции для конкретного значения. Erased-параметр дополнительно исчезает из runtime, а if erased гарантированно вычисляется при компиляции. Это позволяет типу результата зависеть от аргумента: одна функция может вернуть int для true и bool для false. Типы сами являются erased-значениями типа type, поэтому отдельной грамматики типов нет, а полиморфизм записывается обычными функциями.
В итоге Syl dependently typed во время компиляции и simply typed во время выполнения. Типы и erased-ветви стираются, runtime не инспектирует их, а специализированные функции напоминают результат C++ template specialization.
Язык допускает general recursion в type-level computation и type : type. Поэтому наличие выражения некоторого типа не доказывает соответствующую proposition: функция может обещать значение любого типа и никогда не завершиться. Syl не претендует на роль theorem prover вроде Lean, Rocq или Agda. Typechecking становится неразрешимым в общем случае, а приложения, создающие proofs, необходимо вычислить перед использованием. Зато не нужны totality checker и universe machinery; для остановки зацикливания есть fuel limits.
Explicit partiality позволяет статически требовать ненулевой делитель: safe_div имеет рабочую ветвь для d != 0 и unreachable для нуля, выдающего понятную ошибку при инстанцировании. Примеры включают типизированный interpreter и length-indexed vector, где тип append показывает сумму длин аргументов.
Потенциальные расширения — higher-kinded types, ML-подобные modules и functors через dependent records, typed imports, reflection и пользовательские runtime-layouts. Проект далёк от завершения: нужны mode polymorphism, lifetimes, linearity, implicit parameters, proofs, incremental compilation, полезные traces и LLVM backend.