Chalk 기반 트레이트 해결

Chalk는 Rust를 위한 실험적인 트레이트 솔버로, ( 2022년 5월 기준) 타입 팀이 개발하고 있습니다. Chalk의 목표는 구현하기 어려운 여러 트레이트 시스템 기능과 버그 수정(예: GAT나 특수화)을 가능하게 하는 것입니다. 새 솔버 개발을 돕고 싶다면 rust-lang Zulip의 #t-types 채널에 들러 인사해 주십시오!

새로운 방식의 트레이트 솔버는 chalk에서 이루어진 작업을 기반으로 합니다. Chalk는 Rust의 트레이트 시스템을 논리 프로그래밍의 관점에서 명시적으로 재구성합니다. 이를 위해 Rust 코드를 일종의 논리 프로그램으로 “로워링(lowering)“하며, 이렇게 만든 프로그램에 쿼리를 실행할 수 있습니다.

여기서 핵심은 Rust 트레이트 시스템이 기본적으로 일종의 논리이며, 표준적인 논리 추론 규칙으로 옮길 수 있다는 점입니다. 그런 다음 예를 들어 Prolog 솔버가 동작하는 방식과 매우 유사한 방식으로 해당 추론 규칙의 해를 찾을 수 있습니다. 알고 보니 Prolog 규칙(혼 절이라고도 함)을 그대로 사용할 수는 없고, 그보다 표현력이 다소 더 높은 변형이 필요합니다.

chalk 자체에 대해서는 Chalk 책 섹션에서 더 자세히 읽을 수 있습니다.

진행 중인 작업

새로운 방식의 트레이트 해결 설계는 두 곳에서 이루어집니다.

chalk. chalk 저장소는 트레이트 시스템에 대한 새로운 아이디어와 설계를 실험하는 곳입니다.

rustc. 논리 규칙이 만족스러워지면 이를 rustc에 구현하는 단계로 넘어갑니다. rustc의 로워링(lowering) 모듈에서 구조체, 트레이트, impl 선언을 논리 추론 규칙으로 매핑합니다.