표준화

표준화는 값을 그 컨텍스트로부터 분리하는 과정이며, 추론 변수를 포함하는 목표(goal)를 전역적으로 캐싱하는 데 필요합니다.

핵심은 ?x와 ?y가 현재 제약되지 않은 서로 다른 두 추론 변수일 때, u32: Trait<?x>와 u32: Trait<?y>라는 목표가 주어지면 두 목표에 대해 같은 결과를 얻어야 한다는 것입니다. 따라서 정준 쿼리 exists<T> u32: Trait<T>를 한 번 증명하고 그 결과를 재사용할 수 있습니다.

먼저 정준 쿼리가 동작하는 방식을 살펴본 뒤, 표준화가 동작하는 방식의 세부 사항을 자세히 알아봅시다.

정준 쿼리 둘러보기

조금 더 쉽게 설명하기 위해, 관련된 impl이 impl<T> Trait<Vec<T>> for u32 하나뿐이라고 가정하고 트레이트 목표 u32: Trait<?x>를 예로 들어 봅시다.

입력 표준화하기

먼저 목표를 표준화하는 것으로 시작합니다. 이때 추론 변수는 존재 바운드 변수로, 플레이스홀더는 전칭 바운드 변수로 대체합니다. 그 결과 표준 목표 exists<T> u32: Trait<T>를 얻게 됩니다.

원래 컨텍스트에서 모든 바운드 변수가 가졌던 원래 값을 기억해 둡니다. 여기서는 T를 다시 ?x로 매핑하게 됩니다. 이 원래 값들은 나중에 쿼리 응답을 처리할 때 사용됩니다.

이제 정준 목표를 가지고 정준 쿼리를 호출합니다.

쿼리 내부에서 표준 목표 인스턴스화하기

표준 목표를 실제로 증명해 보기 위해, 먼저 바운드 변수를 다시 추론 변수와 플레이스홀더로 인스턴스화합니다.

이 과정은 쿼리 내부의 완전히 별개인 InferCtxt에서 일어납니다. 이제 쿼리 내부에는 u32: Trait<?0>라는 목표가 있습니다. 또한 표준 목표의 바운드 변수를 인스턴스화하는 데 어떤 값을 사용했는지도 기억해 두며, 이는 T를 ?0으로 매핑합니다.

이제 목표 u32: Trait<?0>를 계산하여 이 목표가 성립한다는 것을 알아내지만, 그 과정에서 ?0을 Vec<?1>로 제약했습니다. 마지막으로 이 결과를 호출자에게 유용한 형태로 변환합니다.

쿼리 응답 표준화하기

호출자에게는 목표가 성립하는지 여부와 쿼리 내부에서 생긴 추론 제약을 모두 반환해야 합니다.

추론 결과를 호출자에게 반환하기 위해, 쿼리에서 바운드 변수를 인스턴스화된 값으로 대응시키는 매핑을 표준화합니다. 즉, 쿼리 응답은 Certainty::Yes와 T에서 exists<U> Vec<U>로의 매핑이 됩니다.

쿼리 응답 인스턴스화하기

이제 호출자는 쿼리가 반환한 제약을 적용해야 합니다. 이를 위해 호출자는 먼저 표준 응답의 바운드 변수를 다시 추론 변수와 플레이스홀더로 인스턴스화하며, 따라서 응답의 매핑은 이제 T에서 Vec<?z>로의 매핑이 됩니다.

이제 T의 원래 값(?x)과 응답에 있는 T의 값(Vec<?z>)을 동일시하며, 이를 통해 ?x를 Vec<?z>로 올바르게 제약합니다.

ExternalConstraints

트레이트 목표를 계산하면 추론 변수를 제약할 뿐만 아니라 영역 의무(region obligation)가 추가될 수도 있습니다. 예를 들어 목표 (): AOutlivesB<'a, 'b>가 주어지면 'a: 'b가 성립해야 한다는 사실을 반환하고자 합니다.

이는 쿼리에서 바운드 변수를 인스턴스화된 값으로 대응시키는 매핑을 반환할 뿐만 아니라, 응답을 구성하는 동안 InferCtxt 컨텍스트에서 추가적인 ExternalConstraints를 추출하는 방식으로 이루어집니다.

표준화는 정확히 어떻게 동작합니까

TODO: PR이 병합되면 코드 링크를 추가하고 내용을 보완하십시오

• 타입과 상수: 유니버스를 고려하여 추론 변수는 존재적 바운드 변수로, 플레이스홀더는 보편적 바운드 변수로 매핑합니다.
• 입력에 있는 제네릭 매개변수는 루트 유니버스의 플레이스홀더로 취급됩니다
• 입력에 있는 모든 영역은 전부 존재적 바운드 변수로 매핑되며, 이들을 “고유화“합니다. &'a (): Trait<'a>는 exists<'0, '1> &'0 (): Trait<'1>로 표준화됩니다. 리전의 유니버스는 신경 쓰지 않으며, 단순히 모든 리전을 입력의 가장 높은 유니버스에 넣습니다.
• 출력에서는 호출자의 유니버스에 속한 모든 것이 루트 유니버스에 들어가며, 변수 값을 호출자의 원래 값과 통합할 때에야 비로소 올바른 유니버스를 갖게 됩니다
• 응답에서는 리전을 고유화하지 않으며 'static도 정규화하지 않습니다