В среду,
3 февраля, в Спейсе (Воронцово поле, 5/7с8, Москва)
в 20:00 Денис Буздало́в (ИСП РАН) сделает
доклад о Quantitative Type Theory и о ее применении.
Также будет трансляция, ссылка на которую появится в канале за 10мин до начала.
QTT — это расширение системы типов для языков программирования со строгой типизацией, которая позволяет в сигнатурах функций уточнять когда может использоваться тот или иной параметр, тем самым давая более точные обещания пользователю функции или сужая возможные реализации для того, кто эту функцию пишет. В частности, таким образом можно избегать определённого рода ошибок в программах.
Для людей, знакомых с линейными типами (например, знакомых с Rust), можно сказать, что QTT — это обобщение линейных типов, которое, правда, в отличие от Rust, в докладе будет рассматриваться на примере функциональных языков.
Изложение будет лежать в практической плоскости: будет рассказано не о самой теории типов QTT как таковой, а о применении этой теории типов — о том, что можно специфицировать в языках, в основе которых лежит QTT
QTT лежит в основе системы типов Idris 2, примеры в докладе будут использовать синтаксис Idris.
Основная статья по QTT:
Robert Atkey. The Syntax and Semantics of Quantitative Type Theory. 2018.
https://bentnib.org/quantitative-type-theory.pdf
