왜 판단적 평등이 기능 상실화 하에서 실패하는가

이 글은 의존 타입 언어에서 판단적 동등성과 함수화 해제 사이의 긴장 관계를 살펴봅니다. α-β 및 η-동등성은 많은 시스템에서 표준이지만, 함수가 데이터 생성자로 변환되면 더 이상 성립하지 않습니다. 이 논문은 중간 해결책을 제안합니다. 즉, comatch에 전역적으로 고유한 이름을 할당하여 변환 하에서도 동등성을 유지하는 동시에, 논리적 불일치를 피하기 위해 일반적인 η-동등성을 거부합니다. 그 결과, 건전성을 희생하지 않으면서 함수화 해제 및 재함수화에 대해 닫힌 타입 시스템을 얻게 됩니다.