Почему равенство суждения терпит неудачу при дефункционализации

Эта статья рассматривает напряжение между судящим равенством и дефункционализацией в языках с зависимыми типами. В то время как α-β и η-равенство являются стандартными во многих системах, они перестают выполняться, когда функции преобразуются в конструкторы данных. В статье предлагается компромиссное решение: присваивать глобально уникальные имена косоответствиям для сохранения равенства при преобразовании, отвергая общее η-равенство, чтобы избежать логических противоречий. Результатом является система типов, замкнутая относительно дефункционализации и рефункционализации без ущерба для корректности.