Про свободные теоремы

Свободная теорема - это содержательное тождество, которое следует из типа любой параметрически полиморфной функции в полиморфно типизированном лямбда-исчислении. В "простых" полиморфных системах (вроде System F) свободные теоремы выполняются безусловно. В более богатых системах, например, в Хаскелле, имеются некоторые ограничения, возникающие из-за наличия в языке примитивов неограниченной рекурсии fix и строго вычисления seq, подробности см. [Johann06].

( Read more... )

PS. Ну и чтобы всё было в одном месте - автоматический генератор свободных теорем.