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

Доклад принят в программу конференции
Виталий Брагилевский
JetBrains

Разработчик ПО и преподаватель, член комитета по стандартизации языка программирования Haskell и наблюдательного комитета по разработке компилятора GHC языка Haskell, автор книги «Haskell in Depth» (Manning Publications).

Тезисы

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

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

Другие доклады секции Офлайн 2021

Sufficiently Advanced Testing
Zac Hatfield-Dodds
Australian National University