Типы? Типы... Типы! Офлайн 2021

Не секрет, что многие программисты на Python считают, что типы не нужны. Они мешают выражать свои мысли, ограничивают в возможностях, то есть просто не дают писать код. С другой стороны, разработчики на языках со статической типизацией как-то научились со всем этим справляться и вряд ли кто-то из них горит желанием избавляться от типов.

В этом докладе я продемонстрирую, как богатая строгая статическая система типов позволяет разработчикам выражать свои идеи в типах и заставляет компиляторы эти идеи проверять. Будет много примеров кода на таких языках, как Haskell и Idris (и даже на языках пострашнее!), поэтому будет сложно, но я попытаюсь объяснить эти примеры так, чтобы было понятно, как именно типы там работают. В частности, мы посмотрим на то, как вычисления на типах строго специфицируют Web API и отправляют данные на GPGPU, как зависимые типы позволяют использовать регулярные выражения для контроля значений переменных и реализовывать корректно работающие структуры данных, как линейные типы применяются для обеспечения гарантий корректности управления ресурсами, наконец, как типы высших порядков выражают целые классы систем сборки (да-да, это что-то про make!).