Rust의 HKT 에뮬레이션, 컴파일러를 멈추다!

저자는 Rust에서 HKT를 직접 지원하지 않아, GATs(Generic Associated Types)를 활용하여 에뮬레이션을 시도했다. 하지만, `Wrap` 트레이트(Trait)와 `PartialEq` 트레이트를 함께 사용하면서 컴파일러가 무한 루프(Infinite Loop)에 빠지는 버그를 발견했다. 이는 Rust의 트레이트 해결사(Trait Solver)가 공귀납법(Coinduction)을 제대로 처리하지 못하기 때문에 발생한 문제로, GATs를 이용한 HKT 에뮬레이션의 한계를 보여준다.

문제의 핵심은 Rust의 트레이트 해결사가 공귀납법(Coinduction)을 제대로 지원하지 않는다는 점이다. PartialEq 트레이트와 같이, 공귀납법이 필요한 트레이트를 처리할 때, 컴파일러는 무한한 증명 트리(Infinite Proof Tree)를 생성하여 해결할 수 없는 상황에 직면한다. 저자는 이 문제를 해결하기 위해 차세대 트레이트 해결사(Next-Gen Solver)의 개선 필요성을 강조하며, 현재 진행 중인 사이클 의미론(Cycle Semantics) 강화 작업에 대한 기대를 나타냈다.

저자는 Rust의 문제점을 보완하기 위해 Lean 4를 사용하여 형식적 증명(Formal Proof)을 시도했다. Curry-Howard 동형성(Isomorphism)을 바탕으로, 논리적 증명을 프로그래밍 코드로 표현하는 방법을 탐구했다. 특히, `S` 타입(Type)의 속성을 증명하기 위해 귀납법(Induction)을 활용하는 과정을 상세히 설명하며, Lean 4를 이용한 형식적 증명의 가능성을 보여주었다. 또한, `Threeven`과 같은 명제를 정의하고 증명하는 과정을 통해, 프로그래밍과 논리의 연관성을 강조했다.

저자는 Rust의 트레이트 해결사가 귀납적(Inductive) 방식으로 작동하며, 무한 루프(Infinite Loop)를 방지하기 위해 사이클이 없는 증명 트리를 구성해야 한다고 설명한다. `Vec: Debug`와 같은 간단한 경우를 예시로 들어, 증명 트리의 구성 과정을 보여준다. 반면, `List: Send`와 같은 재귀적 타입(Recursive Type)의 경우, 무한한 증명 트리가 생성되어 문제를 발생시킬 수 있음을 지적하며, 공귀납법의 필요성을 강조한다.