개발 도구는 표현식이 어떤 타입을 가지는지 보고하지만, 왜 그런 타입을 갖는지는 알려주지 않습니다. 본 논문은 타입 슬라이싱(type slicing) 이론을 개발합니다. 프로그래머가 특정 항(term)을 선택하고 그 타입 정보의 어느 부분을 질의하면, 질의된 타입을 재현하는 데 충분한 프로그램 조각(program slice)을 받게 됩니다. 우리는 양방향 타입 시스템(bidirectional type systems)에 대한 타입 슬라이싱을 공식화하는데, 여기서 합성 슬라이스(synthesis slices)는 항이 합성하는 타입을 설명하고 분석 슬라이스(analysis slices)는 주변 컨텍스트가 기대하는 타입을 설명합니다. 이 이론은 타입과 항에 대해 하향 정적 등급성 속성(downwards static graduality property)을 갖춘 정밀도 순서(precision orders)를 갖춘 모든 양방향 시스템에 적용됩니다. 우리는 Hazelnut 및 marked lambda calculus를 기반으로 하는 구멍(holes), 곱(products), 합(sums), 명시적 다형성(explicit polymorphism)을 가진 코어 계산(core calculus) 위에서 메타이론을 개발합니다. 우리는 모든 질의가 최소 슬라이스(minimal slice)를 가지며, 질의를 정제하는 것이 그 최소 슬라이스를 단조적으로 축소시킨다는 것을 증명합니다. 그런 다음 이러한 슬라이스를 정확하게 그리고 근사적으로 계산하는 방법을 보여줍니다. 마지막으로, 타입 슬라이싱을 오류 마킹 이론(error marking theory)과 통합함으로써 이 결과를 임의의 잘못된 타입 프로그램까지 확장하여, 하나의 메커니즘이 완전하고 불완전하며 오류가 있는 코드에서 타입과 타입 오류를 모두 설명하게 합니다. 이 메타이론은 Agda로 기계화되었으며, Hazel 프로그래밍 환경을 위한 타입 슬라이싱의 선형 시간 근사치가 구현되었습니다.