TL;DR

  • 양방향 타입 시스템에서 타입 질의에 충분한 프로그램 슬라이스를 제공하는 타입 슬라이싱 이론을 제시하고, 모든 질의에 최소 슬라이스가 존재하며 질의를 정밀화할수록 최소 슬라이스가 단조롭게 축소됨.
  • 표현식이 합성하는 타입을 설명하는 합성 슬라이스와 주변 문맥이 기대하는 타입을 설명하는 분석 슬라이스를 구분함.
  • 정밀도 순서와 하향 정적 점진성(downwards static graduality) 속성을 갖춘 모든 양방향 시스템에 이론을 적용함.
  • 구멍, 곱 타입, 합 타입, 명시적 다형성을 포함하는 핵심 계산법에서 메타이론을 전개하고, 정확한 계산과 근사 계산을 제시함.
  • 오류 표시 이론과 결합해 불완전하거나 잘못된 프로그램까지 설명하며, Agda로 메타이론을 기계화하고 Hazel 환경에 선형 시간 근사를 구현함.

논문 개요

  • 개발 도구는 표현식의 타입을 알려주지만, 그 타입이 왜 도출되는지는 설명하지 않는 경우가 있음.
  • 논문은 프로그래머가 항(term)을 선택하고 타입 정보의 일부를 질의하면, 질의한 타입을 재현하기에 충분한 프로그램 슬라이스를 반환하는 타입 슬라이싱 이론을 제시함.
  • 논문 제목은 *Bidirectional Type Slicing*이며, Max Carroll과 Anil Madhavapeddy(University of Cambridge), Cyrus Omar(University of Michigan)가 작성함.
  • 2026년 7월 13일 arXiv에 제출된 논문으로, 식별자는 arXiv:2607.12197임.

양방향 타입 시스템의 슬라이스

  • 합성(synthesis) 슬라이스는 항이 합성하는 타입을 설명하고, 분석(analysis) 슬라이스는 항을 둘러싼 문맥이 기대하는 타입을 설명함.
  • 타입과 항에 대한 정밀도 순서 및 하향 정적 점진성 속성을 갖춘 모든 양방향 타입 시스템에 이론을 적용함.
  • Hazelnut 및 marked lambda 계산법을 기반으로, 구멍·곱 타입·합 타입·명시적 다형성을 포함하는 핵심 계산법에서 메타이론을 전개함.

최소 슬라이스와 계산

  • 모든 질의에 최소 슬라이스가 존재함을 증명함.
  • 질의를 단조롭게 정밀화하면 최소 슬라이스가 축소됨을 증명함.
  • 슬라이스를 정확하게 계산하는 방법과 근사해 계산하는 방법을 제시함.

오류 프로그램과 구현

  • 타입 슬라이싱을 오류 표시 이론과 통합해, 임의의 타입 오류 프로그램에도 결과를 확장함.
  • 하나의 메커니즘으로 완전한 코드, 불완전한 코드, 오류가 있는 코드의 타입과 타입 오류를 모두 설명함.
  • 메타이론을 Agda로 기계화하고, Hazel 프로그래밍 환경에 타입 슬라이싱의 선형 시간 근사를 구현함.