Если аккуратно вертеть этой теоремой, можно автоматически вывести очень много интересных свойств полиморфных функций

Через параметрисити доказывается закон композиции для большинства конкретных функторов.
Я так понял, что тебе не известен конкретный функтор, но известно, что айдентити в нём сохраняется и нужно через параметрисити теорему доказать сохранение композиции

@yordwynn так лучше?

Пойдёт.

Драсте

Щас антон лучше объяснит

Давайте ещё докинем к отличному контенту от Одомонтоиса)

Кака Олег сказал, можно автоматом свойства выводить. А также эти свойства можно автоматически доказывать, что уменьшает работу для пруверов.
Например, меньше свойств про перестановки для списков нужно явно руками доказывать (полиморфные функции могут кратность и порядок элементов менять, но не сами элементы).

А ещё такие вещи хочется интернализовать в теорию типов, чтоб с этим нормально работать, а не аксиоматически. Например, type theory in color (https://dl.acm.org/doi/abs/10.1145/2544174.2500577)

это нихуя не читаемо

зачем улучшать лучшее)

Бот не согласен.

ему лучше знать, да

@arsenbot согласись, пожалуйста

Охрана bot )

суету наводит

суета сует

волшебные логические реляции

куда их только не суют :)

ниблагадари https://home.ttic.edu/~dreyer/course/papers/wadler.pdf

аголовок номер 2