공귀납
트레이트 솔버는 목표를 증명할 때 공귀납을 사용할 수 있습니다. 공귀납은 꽤 미묘한 개념이므로 별도의 장에서 다룹니다.
공귀납과 귀납
귀납에서는 유한한 증명 트리가 만들어질 때까지 증명을 재귀적으로 적용합니다. 다음과 같은 트리를 만들어 내는 Vec<Vec<Vec<u32>>>: Debug의 예를 살펴보십시오.
Vec<Vec<Vec<u32>>>: DebugVec<Vec<u32>>: DebugVec<u32>: Debugu32: Debug
이 트리는 유한합니다. 그러나 성립하기를 바라는 모든 목표가 유한한 증명 트리를 갖는 것은 아닙니다. 다음 예를 살펴보십시오.
#![allow(unused)]
fn main() {
struct List<T> {
value: T,
next: Option<Box<List<T>>>,
}
}List<T>: Send가 성립하려면 그 모든 필드도 재귀적으로 Send를 구현해야 합니다. 그러면 다음과 같은 증명 트리가 만들어집니다.
List<T>: SendT: SendOption<Box<List<T>>>: SendBox<List<T>>: SendList<T>: SendT: SendOption<Box<List<T>>>: SendBox<List<T>>: Send- …
이 트리는 무한히 커지며, 바로 이것이 공귀납이 다루는 대상입니다.
목표를 귀납적으로 증명하려면 그 목표에 대한 유한한 증명 트리를 제시해야 합니다. 목표를 공귀납적으로 증명할 때는 제시하는 증명 트리가 무한해도 됩니다.
공귀납이 올바른 이유
어떤 트레이트 목표가 성립하는지 검사할 때, 우리는 “이 바운드를 만족하는 impl이 존재하는가“를 묻는 것입니다. 중첩된 목표가 무한히 이어지더라도, 사용해야 할 impl은 여전히 하나로 정해집니다.
공귀납을 구현하는 방법
무한한 트리를 구성하려면 무한한 자원이 필요하므로 우리 구현은 그런 방식으로 공귀납을 검사할 수 없지만, 그래도 이러한 관점에서 공귀납을 생각하는 것은 의미가 있습니다.
무한 트리를 검사할 수는 없으므로, 대신 무한 증명 트리를 만들어 낸다고 알려진 패턴을 찾습니다. 현재 감지하는 패턴은 (정규화된) 순환입니다. T: Send가 T: Send에 의존한다면, 이것이 끝없이 계속되리라는 것은 매우 분명합니다.
순환이 있을 때는 캐싱에 주의해야 합니다. 영역과 추론 변수의 표준화 때문에, 순환을 만났다고 해서 무한한 증명 트리가 생기는 것은 아닙니다. 다음 예제를 살펴보십시오.
#![allow(unused)]
fn main() {
trait Foo {}
struct Wrapper<T>(T);
impl<T> Foo for Wrapper<Wrapper<T>>
where
Wrapper<T>: Foo
{}
}Wrapper<?0>: Foo를 증명할 때는 impl<T> Foo for Wrapper<Wrapper<T>> impl을 사용하는데, 이 impl은 ?0를 Wrapper<?1>로 제약한 다음 Wrapper<?1>: Foo를 요구합니다. 표준화 때문에 이것은 순환으로 감지됩니다.
해결 방안은 순환을 감지할 때마다 잠정 결과를 반환하고, 잠정 결과가 해당 목표의 최종 결과와 같아질 때까지 목표를 반복해서 다시 시도하는 것입니다. 처음에는 제약이 없는 Yes를 결과로 사용하고, 다시 실행해야 할 때마다 이를 이전 반복의 결과로 갱신합니다.
TODO: 여기에 자세한 설명을 추가해야 합니다. 공귀납적 순환에 대해서는 chalk와 같은 접근 방식을 사용합니다. 귀납적 순환은 현재 단순히 Overflow를 반환한다는 점에서 처리 방식이 다르다는 것에 유의하십시오. chalk 책의 관련 장을 참고하십시오.
향후 작업
현재는 자동 트레이트, Sized, WF 목표만 공귀납적인 것으로 간주합니다. 앞으로는 사실상 모든 목표를 공귀납적으로 만들 계획입니다. 먼저 더 많은 공귀납적 증명을 허용하는 것이 애초에 왜 바람직한지 자세히 설명하겠습니다.
재귀 데이터 타입은 이미 공귀납에 의존하고 있습니다…
…트레이트 솔버에서는 그것들을 피하는 경향이 있을 뿐입니다.
#![allow(unused)]
fn main() {
enum List<T> {
Nil,
Succ(T, Box<List<T>>),
}
impl<T: Clone> Clone for List<T> {
fn clone(&self) -> Self {
match self {
List::Nil => List::Nil,
List::Succ(head, tail) => List::Succ(head.clone(), tail.clone()),
}
}
}
}이 impl에서는 tail.clone()을 사용하고 있습니다. 이를 위해 Box<List<T>>: Clone을 증명해야 하며, 이는 List<T>: Clone을 요구합니다. 그런데 이는 현재 검사 중인 바로 그 impl에 의존합니다. perfect derive에서 하듯이 그 요구 사항을 impl의 where 절에 추가하면, 그 순환이 트레이트 솔버 안으로 옮겨지고 오류가 발생합니다.
재귀 데이터 타입
프로젝션을 포함하는 재귀 타입을 추론하는 데에도 공귀납이 필요합니다. 예를 들어 다음 코드는 유효해야 함에도 현재 컴파일에 실패합니다.
#![allow(unused)]
fn main() {
use std::borrow::Cow;
pub struct Foo<'a>(Cow<'a, [Foo<'a>]>);
}이 문제는 적어도 2015년부터 알려져 있었으며, 더 알고 싶다면 #23714를 참고하십시오.
명시적으로 검사되는 암시적 바운드
impl을 검사할 때, 우리는 impl 헤더에 있는 타입이 적격이라고 가정합니다. 이는 impl을 인스턴스화하여 사용할 때 실제로 그러한지 증명해야 한다는 뜻입니다. #100051은 실제로는 그렇지 않다는 것을 보여 줍니다. 이를 고치려면 impl 헤더에 있는 타입들에 대해 WF 술어를 추가해야 합니다. 모든 트레이트에 대한 공귀납이 없으면 이것은 core마저 망가뜨립니다.
#![allow(unused)]
fn main() {
trait FromResidual<R> {}
trait Try: FromResidual<<Self as Try>::Residual> {
type Residual;
}
struct Ready<T>(T);
impl<T> Try for Ready<T> {
type Residual = Ready<()>;
}
impl<T> FromResidual<<Ready<T> as Try>::Residual> for Ready<T> {}
}FromResidual의 impl이 올바른 형식(well-formed)인지 검사할 때 다음과 같은 순환이 발생합니다:
이 impl은 <Ready<T> as Try>::Residual과 Ready<T>가 올바른 형식이면 올바른 형식입니다.
wf(<Ready<T> as Try>::Residual)는 다음을 요구합니다Ready<T>: Try이며, 이는 슈퍼 트레이트 때문에 다음을 요구합니다Ready<T>: FromResidual<Ready<T> as Try>::Residual>, impl에 대한 암시적 바운드 때문에wf(<Ready<T> as Try>::Residual):tada: 순환
공귀납을 더 많은 목표로 확장할 때의 문제점
공귀납을 확장할 때 염두에 두어야 할 몇 가지 추가적인 문제가 있습니다. 여기서 다루는 문제는 현재 솔버와는 관련이 없습니다.
암시적 슈퍼 트레이트 바운드
현재 우리의 트레이트 시스템은 슈퍼 트레이트(예: trait Trait: SuperTrait)를 1) Trait를 구현하는 모든 타입에 대해 SuperTrait가 성립해야 한다고 요구하고, 2) Trait가 성립하면 SuperTrait도 성립한다고 가정하는 방식으로 다룹니다.
1)을 증명하는 동안 2)에 의존하는 것은 건전하지 않습니다. 이는 공귀납적 순환이 있는 경우에만 관찰될 수 있습니다. 순환이 없다면, 2)에 의존할 때마다 사용된 Trait의 impl에 대해 2)에 의존하지 않고 1)도 이미 증명했어야 합니다.
#![allow(unused)]
fn main() {
trait Trait: SuperTrait {}
impl<T: Trait> Trait for T {}
// Keeping the current setup for coinduction
// would allow this compile. Uff :<
fn sup<T: SuperTrait>() {}
fn requires_trait<T: Trait>() { sup::<T>() }
fn generic<T>() { requires_trait::<T>() }
}이는 공귀납 자체의 근본적인 문제라기보다는, 기존에 있던 속성이 공귀납 때문에 건전하지 않게 된 것입니다.
가능한 해결책
이를 해결하는 가장 쉬운 방법은 2)를 완전히 제거하고, 트레이트 솔버 외부에서 T: Trait를 항상 T: Trait와 T: SuperTrait로 확장(elaborate)하는 것입니다. 이렇게 하면 1)도 제거할 수 있지만, 트레이트에 대한 일반적인 where 바운드는 여전히 증명해야 하므로 이는 추가 작업일 뿐입니다.
1)을 검사할 때 2)의 순환적 사용을 비활성화하는 방법을 생각해 볼 수는 있지만, 적어도 저(@lcnr)의 아이디어는 모두 합리적이라고 하기에는 지나치게 복잡합니다.
normalizes_to 목표와 진전
normalizes_to 목표는 <T as Trait>::Assoc가 어떤 U로 정규화된다는 요구 사항을 나타냅니다. 이는 사실상 먼저 <T as Trait>::Assoc를 정규화한 다음, 그 결과 타입을 U와 동일시하는 방식으로 이루어집니다. 각 프로젝션은 정확히 하나의 타입으로 정규화되어야 하므로 이는 사상(mapping)이어야 합니다. 단순히 무한한 증명 트리를 허용하면 다음과 같은 동작이 발생합니다:
#![allow(unused)]
fn main() {
trait Trait {
type Assoc;
}
impl Trait for () {
type Assoc = <() as Trait>::Assoc;
}
}이제 normalizes_to(<() as Trait>::Assoc, Vec<u32>)를 계산하면, impl을 해석하여 연관 타입 <() as Trait>::Assoc를 얻게 됩니다. 그런 다음 이를 기대 타입과 동일시하므로 normalizes_to(<() as Trait>::Assoc, Vec<u32>)를 다시 검사하게 됩니다. 이 과정은 끝없이 계속되어 무한한 증명 트리가 만들어집니다.
이는 <() as Trait>::Assoc가 다른 어떤 타입과도 같아진다는 뜻이며, 이는 건전하지 않습니다.
해결 방법
경고: 이 내용은 미묘하며 틀렸을 수 있습니다
트레이트 목표와 달리 normalizes_to는 생산적(productive)1이어야 합니다. normalizes_to 목표는 프로젝션이 강체(rigid) 타입 생성자로 정규화되면 생산적이므로, <() as Trait>::Assoc가 Vec<<() as Trait>::Assoc>로 정규화되는 것은 생산적입니다.
normalizes_to 목표에는 두 종류의 중첩된 목표가 있습니다. 하나는 프로젝션을 실제로 정규화하는 데 필요한 중첩 요구 사항이고, 다른 하나는 정규화된 프로젝션과 기대 타입 사이의 동등성입니다. 생산적이어야 하는 것은 동등성뿐입니다. 증명 트리의 분기는 유한하거나, 별칭이 강체(rigid) 타입 생성자로 해소되는 normalizes_to를 적어도 하나 포함하면 생산적입니다.
또는 normalizes_to의 동등화 분기를 항상 귀납적으로 취급할 수도 있습니다. 모든 순환은 무한 타입을 낳을 것입니다. 무한 타입은 어차피 지원되지 않으며, 코드 생성을 위해 깊이 정규화할 때 오버플로만 일으킬 것입니다.
실험과 예시: https://hackmd.io/-8p0AHnzSq2VAE6HE_wX-w?view
요약을 한 번 더 시도해 봅니다.
- 프로젝션 동등성에서는 rhs를 제약하는 쪽으로 반드시 진전을 이루어야 합니다.
- 순환은 동등화하는 동안 정규화 후 lhs에 강체 타입이 적어도 한 번 나타나는 경우에만 괜찮습니다.
normalizes_to의 재귀적인eq호출 바깥의 순환은 항상 괜찮습니다.