양방향 타입 슬라이싱 — 타입 정보가 나온 이유를 프로그램 조각으로 설명하기

AI 요약

타입 검사기는 표현식의 타입이나 예상 타입과 실제 타입의 불일치를 알려주지만, 그 정보가 프로그램 어디에서 비롯했는지는 설명하지 않습니다. 이 논문은 사용자가 특정 표현식의 타입 일부를 질의하면, 해당 정보를 재현하는 데 필요한 프로그램 조각을 돌려주는 타입 슬라이싱(type slicing) 이론을 제시합니다. 관련 없는 하위 표현식은 구멍(hole)으로 접어 표시하므로, 긴 코드에서 질의와 무관한 부분을 걷어낼 수 있습니다.

합성과 분석을 나눠 타입의 출처를 설명합니다

논문은 타입 합성(type synthesis)과 타입 분석(type analysis)을 구분하는 양방향 타입 시스템(bidirectional type system)을 대상으로 삼습니다. 합성 슬라이스(synthesis slice)는 표현식 내부의 어떤 코드가 그 표현식의 타입을 만들었는지 보여줍니다. 분석 슬라이스(analysis slice)는 주변 문맥의 어떤 코드가 표현식에 특정 타입을 요구했는지 보여줍니다. 예를 들어 함수의 인자 타입을 질의하면, 함수 본문이 아니라 그 인자에 타입을 요구하는 문맥을 추려낼 수 있습니다.

질의는 전체 타입뿐 아니라 타입의 일부만 대상으로 삼을 수 있습니다. 함수 타입에서 반환 타입을 접고 인자 타입만 남기면, 그 타입 조각을 설명하는 코드만 남도록 슬라이스를 더 줄입니다. 논문은 질의를 더 구체화할수록 최소 슬라이스가 이전 슬라이스보다 커지지 않는 단조성(monotonicity)을 증명합니다. 따라서 사용자가 관심 범위를 좁혀도 설명에 새 코드가 불쑥 추가되지 않습니다.

정적 점진성으로 최소 슬라이스를 보장합니다

이론의 기반은 타입과 표현식의 정밀도(precision) 순서입니다. 구멍을 늘려 프로그램을 덜 정밀하게 만들면 타입 정보도 같거나 덜 정밀해져야 한다는 하향 정적 점진성(downwards static graduality)을 요구합니다. 이 조건을 만족하면 모든 질의에 최소 슬라이스가 존재하며, 타입 시스템에 캐스트 실행 의미론(cast dynamics)을 요구하지 않습니다.

저자들은 구멍, 곱·합 타입, 명시적 다형성(explicit polymorphism)을 포함한 핵심 계산법(core calculus)을 정의하고, Hazelnut과 marked lambda calculi를 바탕으로 메타이론을 전개합니다. 문맥 타이핑(context typing)은 포커스가 된 하위 표현식의 타입과 그 바깥 문맥을 분리해 기록합니다. 이 구성으로 분석 슬라이스를 정의하고, 문맥과 포커스를 다시 결합했을 때 타입이 보존되는 성질도 증명합니다. 메타이론은 Agda로 형식화했습니다.

타입 오류도 양쪽에서 추적합니다

오류 표시(error marking) 이론과 슬라이싱을 결합해, 잘못된 프로그램에서도 같은 방법으로 설명을 만들도록 확장합니다. 타입 불일치가 나면 표현식 쪽의 실제 타입을 만든 코드와 문맥 쪽의 예상 타입을 만든 코드를 따로 보여줍니다. 주석이 틀렸을 가능성을 미리 배제하지 않으므로 한쪽만 오류 원인으로 지목하지 않습니다. 사용자가 주석을 기준으로 삼고 싶다면 합성 슬라이스만 확인하는 식으로 선택할 수 있습니다. 함수 자리에 함수가 아닌 타입이 온 형태 오류(shape error)나, 타입을 합성할 수 없는 람다에 주변 문맥이 타입을 요구하는 경우도 다룹니다. 변수 범위 오류는 타입 정보에 관한 오류가 아니므로 이 방식의 대상에서 제외합니다.

정확한 최소화와 실행 비용

모든 최소 슬라이스를 찾는 최소 크기 슬라이싱 문제는 NP-hard입니다. 논문은 구조를 따라 계산하는 방법과 근사 알고리즘을 제시합니다. 특히 case 분기에서는 두 분기의 타입이 합쳐질 때 한 분기가 다른 분기의 타입 정보를 중복 제공하는 문제가 생겨, 정확한 계산이 까다롭습니다. Hazel 구현은 타입 질의를 분기별로 나눠 선형 시간 근사를 사용하며, 이 방식은 항상 정확한 최소 슬라이스를 보장하지는 않습니다. 저자들은 프로토타입을 초기 구현으로 제시하고 사용성에 관한 주장은 하지 않습니다.

원문: Lobsters / 번역·요약: Trawling

Lobsters 반응

• @cpurdy — 이 작업은 인상적입니다. 지금 형태가 도구로서 얼마나 유용할지는 잘 모르겠지만, 그 바탕이 된 사고방식은 양방향 타입 시스템을 연구하는 사람들에게 매우 유용할 수 있습니다.
• @crowdhailer — 이걸 EYG에서 작동하게 만들 방법을 꼭 살펴봐야겠네요.
• @rtfeldman — Cyrus Omar의 Hazel 작업에서 이런 결과가 나올 줄은 몰랐지만, 생각해보니 무척 자연스럽습니다. 오류 보고에 활용할 수 있을지 궁금했는데, 7절에서 다루고 있어서 반가웠습니다. 이 계산법으로 타입이 잘 맞는 프로그램의 타입뿐 아니라, 타입 오류가 있는 프로그램의 오류도 설명할 수 있음을 보여줍니다. 정말 흥미롭습니다.