Доказательство законов классов типов на бесконечных типах

[_Ivana]

Здравствуйте. Давно я сюда ничего не писал, но вот недавно возникла ситуация, и я решил попросить помощи.
Фабула: есть классический функциональный тип Список:

data List a = Nil | Cons a (List a)

для него требуется доказать выполнение второго закона класса типов Функтор:

fmap f (fmap g l) = fmap (f . g) l

то есть композиция функторного преобразования равна функторному преобразованию по композиции составляющих. На одной площадке было написано простейшее индуктивное доказательство в духе Tapl и Бенджамина Пирса: доказываем для базы индукции Nil, доказываем индукционный переход. Но Пирса можно понять - у него все выкладки базируются на языке со строгой семантикой и все типы конечны, мы не встретим там бесконечных списков, значит наивная индукция работает. Но подобное доказательство было приведено относительно Хаскеля, где присутствуют бесконечные списки. Это вызвало мое подозрение, т.к. по такой же логике можно доказать утверждение "бесконечных списков не существует", что противоречит истине. Мне были даны ссылки на Википедию "Трансфинитная индукция", но детально затруднились показать, как мы вводим отношение порядка на множестве списков для удовлетворения условиям этой индукции.

Собственно, вопрос: как доказать? В процессе обсуждения были высказаны предположения, что даже само определение равенства термов, не имеющих нормальной формы, может вызвать затруднения. Но в этом вопросе у меня есть некий оптимизм - мы можем попытаться ввести понятие равенства термов не приводя их к нормальным формам, а пытаясь привести оба терма (через частичные применения альфа/бета/эта редукции) к таким термам, которые равны (не являясь нормальными формами) - этакое экстенсиальное равенство. А поскольку в реальности мы можем ограничиться только конечными термам и (возможно, не имеющими нормальной формы), то на исходном множестве конечных термов можно считать отношение равенства определенным. Вопрос про применение индукции на таких бесконечных коиндуктивных типах, ну и, возможно, определение равенства на них.

[Legioner93]

Может просто сравнить оба (бесконечных) списка поэлементно?

[iifat]

Если вы используете в запуске программы 1000 первых элементов списка, то вам, в общем-то, всё равно, сколько в нём — 1001 элемент, 10000, или бесконечность. Может, отсюда плясать?

[Xaositect]

M. P. Fiore "A Coinduction Principle for Recursive Data Types Based on Bisimulation"
Вкратце: Бисимуляция для коиндукцивных списков - это такое отношение $R$, что $R([], [])$ и $R(x, y) \Rightarrow \operatorname{head}(x) = \operatorname{head}(y) \& R(\operatorname{tail}(x), \operatorname{tail}(y))$. Из бисимуляции следует равенство, потому что коиндуктивный тип - это терминальная коалгебра.

[_Ivana]

Xaositect, спасибо, похоже это именно то, что надо. На досуге попробую детальнее разобраться.