캡처 검사 내부
캡처 검사 내부 (Capture Checking Internals)
캡처 검사기는 타입 검사와 몇 가지 초기 변환 후 별도의 단계로 실행되는 전파 제약 해석기(propagation constraint solver)로 설계됐어요.
본문
제약 변수는 알려지지 않은 캡처 집합을 나타내요. 제약 변수는 다음과 같은 경우 도입돼요.
- 이전에 추론된 타입의 각 부분에 대해,
- 모든 메서드, 클래스, 익명 함수, by-name 인자의 접근된 참조에 대해,
- 클래스 생성자 호출에 전달된 파라미터에 대해.
명시적으로 쓰인 타입의 캡처 집합은 상수로 취급돼요(캡처 검사 전에는 그런 집합은 그냥 무시돼요).
캡처 검사기는 본질적으로 평소의 타이핑 규칙으로 프로그램을 다시 검사해요. 캡처 타입 사이의 하위 타입 요구가 검사될 때마다, 이것은 캡처 집합에 대한 하위 캡처 테스트로 번역돼요. 두 집합이 상수라면 이것은 단순한 예/아니오 질문이며, '아니오'는 오류 메시지를 만들어요.
비교 C₁ <: C₂의 아래 집합 C₁이 변수라면, 집합 C₂가 C₁의 상위 집합으로 기록돼요. 위 집합 C₂가 변수라면, C₁의 원소들이 C₂로 전파돼요. 원소 x를 집합 C로 전파한다는 것은 x가 C의 원소로 포함되고, C의 알려진 모든 상위 집합으로도 전파된다는 뜻이에요. 그런 상위 집합이 상수라면 x가 포함되는지 검사돼요. 포함되지 않는다면 원래 비교 C₁ <: C₂는 해가 없으므로 오류가 보고돼요.
타입 검사기는 또한 타입에 다양한 매핑을 수행해요. 예를 들어 의존 함수에서 형식 파라미터 타입에 실제 인자 타입을 대입하거나, 선택에서 "as-seen-from"으로 멤버 타입을 매핑할 때요. 매핑은 타입에서 위치의 변성(variance)을 추적해요. 변성은 초기에 공변(covariant)이고, 함수 파라미터 위치에서 반변(contravariant)으로 뒤집히며, 타입 인자에서는 타입 파라미터의 변성에 따라 공변, 반변, 또는 불변(nonvariant)일 수 있어요.
캡처 검사를 할 때 같은 매핑이 캡처 집합에도 수행돼요. 캡처 집합이 상수라면 그 원소들(역량)이 일반 타입으로 매핑돼요. 그런 매핑의 결과가 역량이 아니라면, 결과는 타입의 변성에 따라 근사된다. 공변 근사는 타입을 그 캡처 집합으로 바꿔요. 반변 근사는 그것을 빈 캡처 집합으로 바꿔요. 불변 근사는 감싸는 캡처 타입을, 더 바깥으로 전파되고 해결되는 가능한 타입들의 범위로 바꿔요.
캡처 집합 변수 C에 매핑 m이 수행되면, 매핑된 원소를 포함하고 C와 연결된 새 변수 Cm이 생성돼요. C가 이후에 전파로 추가 원소를 얻으면, 그것들도 m 매핑으로 변환된 뒤 Cm으로 전파돼요. Cm은 C와 같은 상위 집합들을, 다시 m으로 매핑해 얻어요.
캡처 검사기의 흥미로운 측면 중 하나는 캡처 터널링의 구현과 관련돼요. 캡처 검사의 기반이 되는 기초 이론은 소위 box와 unbox 연산을 통해 터널링을 명시적으로 만들어요. Boxing은 캡처 집합을 숨기고 unboxing은 그것을 되찾아요. 캡처 검사기는 타입 검사기가 암시적 변환을 삽입하는 것과 유사하게 실제 타입과 기대 타입을 기반으로 가상의 box와 unbox 연산을 삽입해요. 캡처 집합 변수가 처음 도입될 때, 타입 파라미터 인스턴스의 인스턴스인 캡처 타입의 어떤 캡처 집합도 "boxed"로 표시돼요. 표현식의 기대 타입이 boxed 캡처 집합 변수를 가진 캡처 타입이면 boxing 연산이 삽입돼요. 이 삽입의 효과는 boxed 표현식의 역량에 대한 참조가 잊혀진다는 것, 즉 캡처 전파가 멈춘다는 뜻이에요. 이중적으로, 표현식의 실제 타입이 캡처 집합으로 boxed 변수를 가진다면 unbox 연산이 삽입되는데, 이는 캡처 집합의 모든 원소를 환경에 더해요.
Boxing과 unboxing은 런타임 효과가 없으므로, 이 연산들의 삽입은 단지 시뮬레이션될 뿐이에요. 유일하게 보이는 효과는 현재 검사되는 표현식의 환경을 나타내는 캡처 집합에서 변수의 제거와 삽입이에요.
-Ycc-debug 옵션은 캡처 검사기의 작동에 대한 통찰을 제공해요. 켜면 boxed 집합이 명시적으로 표시되고, 캡처 집합 변수가 ID와 기원(provenance)에 대한 정보와 함께 출력돼요. 예를 들어 문자열 {f, xs}33M5V는 원소 f와 xs를 담고 있다고 알려진 캡처 집합 변수를 나타내요. 변수의 ID는 33이에요. M은 변수가 ID 5인 변수의 매핑을 통해 생성됐음을 나타내요. 후자는 V로 표시된 것처럼 일반 변수예요.
일반적으로 캡처 집합 뒤에 오는 문자열은 숫자와 문자가 번갈아 나타나는 것으로 이루어지는데, 각 숫자는 변수 ID를, 각 문자는 변수의 기원을 줘요. 가능한 문자는:
V: 일반 변수,M: 오른쪽의 문자열이 나타내는 변수의 매핑에서 나온 변수,B:M과 유사하되 매핑이 전단사(bijection)인 경우,F: 오른쪽의 문자열이 나타내는 변수의 원소를 필터링해서 나온 변수,I: 두 캡처 집합의 교집합에서 나온 변수,D: 두 캡처 집합의 차집합에서 나온 변수.R: 클래스 파라미터를 정제(refines)하는 일반 변수로, 생성자 인자의 캡처 집합이 클래스 인스턴스 타입에서 알려지도록 해요.
컴파일 실행이 끝나면 -Ycc-debug는 이전 출력에서 참조된 변수의 모든 변수 의존성을 출력해요. 예시가 있어요.
Capture set dependencies:
{}2V ::
{}3V ::
{}4V ::
{f, xs}5V :: {f, xs}31M5V, {f, xs}32M5V
{f, xs}31M5V :: {xs, f}
{f, xs}32M5V ::
이 절은 이전 진단에 나타난 모든 변수와 그 의존성을 재귀적으로 나열해요. 예를 들어 우리는 다음을 알 수 있어요.
- 변수 2, 3, 4는 비어 있고 의존성이 없어요.
- 변수
5는 두 의존성, 즉 변수31과32를 가지는데, 둘 다 변수5를 매핑한 결과예요. - 변수
31은 고정된 상수 상위 집합{xs, f}를 가져요. - 변수
32는 의존성이 없어요.