First Principles에서 의존형 OOP를 도출하기

이 논문은 종속 타입을 배경으로 표현 문제를 다루며, 함수형 프로그래밍과 객체 지향 프로그래밍이 데이터와 코데이터에 기반한 이중 패러다임임을 보여줍니다. 저자들은 종속 타입을 객체 지향 프로그래밍에 임시변통으로 확장하는 대신, 디펑셔널라이제이션(defunctionalization)과 리펑셔널라이제이션(refunctionalization)을 사용하여 종속 타입 객체 지향 미분법의 이중성을 도출합니다. 그 결과, 두 개의 의미적으로 동등한 조각(함수형과 객체 지향)을 가진 언어가 탄생하며, 이는 타입과 의미를 보존하는 변환을 통해 연결됩니다. 이는 타입이 지정된 프로그래밍 언어의 이론적 기반과 확장성을 넓혀줍니다.