Исследовательская группа
Лаборатория языковых инструментов
Использование параметричности для получения бесплатных теорем
December 4
Поскольку параметрически-полиморфные функции должны обрабатывать значения разных типов идентичным образом, их возможности использования информации о поступающих значениях существенно ограничены. Эти ограничения могут быть использованы для доказательства некоторых полезных свойств полиморфных функций. Филип Уодлер предложил метод генерации теорем такого рода (известных теперь как "бесплатные теоремы» — free theorems) для любого полиморфного типа. В докладе мы разберем данный метод, а также рассмотрим конкретные примеры бесплатных теорем и их возможные применения.
Материалы к докладу:
Philip Wadler. Theorems for free!
Докладчик: Дмитрий Розплохас