Лаборатория языковых инструментов

Поскольку параметрически-полиморфные функции должны обрабатывать значения разных типов идентичным образом, их возможности использования информации о поступающих значениях существенно ограничены. Эти ограничения могут быть использованы для доказательства некоторых полезных свойств полиморфных функций. Филип Уодлер предложил метод генерации теорем такого рода (известных теперь как "бесплатные теоремы» — free theorems) для любого полиморфного типа. В докладе мы разберем данный метод, а также рассмотрим конкретные примеры бесплатных теорем и их возможные применения.

Материалы к докладу:

Philip Wadler. Theorems for free!

Докладчик: Дмитрий Розплохас