동일한 공효과, 다른 기반: 등급 타입(Graded Types)의 두 가지 주요 접근 방식 연결

등급 타입(Graded types)은 타입 시스템에 세밀한 정보를 추가하여 부수 효과(side effects)나 문맥 의존성(context dependence) 및 자원 사용(공효과(coeffects)라고 불림)을 추적할 수 있는 방법을 제공합니다. 공효과를 위한 등급 타입은 Haskell, Idris, Granule와 같은 언어에 도입되어, 다양한 일반성 수준을 가진 공효과 분석(coeffect analysis)을 통해 자원 중심의 추론을 가능하게 했습니다. 지난 10년 동안 두 가지 별개의 등급 공효과 시스템 계보가 등장했습니다. 하나는 공효과 어노테이션(coeffect annotations)이 만연하여 함수 타입에 어노테이션이 필요한 방식(우리는 이를 graded-base라고 부름)이고, 다른 하나는 선형 타입(linear types) 위에 등급 모달 타입 연산자(graded modal type operator)를 통해 공효과를 추가하는 방식(우리는 이를 linear-base라고 부름)입니다. 후자는 자원에 집중된 프로그래밍 언어 연구의 풍부한 토양이 되어온 Girard의 선형 논리(Linear Logic)에 기원을 두고 있는 반면, graded-base 접근 방식은 2010년대 중반에 등장하여 QTT 및 Linear Haskell 등 프로그래밍 언어 이론과 실무에서 빠르게 채택되었습니다. 그러나 이 두 스타일 사이의 관계는 미해결 과제로 남아 있었습니다. 우리는 두 계보의 계산법(calculi) 쌍 사이에 타입(type), 등급(grade) 및 연산 의미론(operational-semantics)을 보존함을 증명하는 번역(translations)을 제공함으로써 이 질문에 답합니다. 우리는 동일한 문맥 의존성 개념이 두 스타일 모두에서 표현될 수 있음을 보여줌으로써, 두 계보 사이에 다리를 놓아 결과와 아이디어의 전달을 가능하게 하는 동시에 언어 설계자들이 더 정보에 입각한 선택을 할 수 있도록 돕습니다.