ロジックへの変換
ここでの重要な観察は、Rust のトレイトシステムが基本的に 一種の論理であり、標準的な論理的推論規則へ対応付けられる、 という点です。そのうえで、たとえば Prolog ソルバーが動作する方法と 非常によく似た形で、それらの推論規則に対する解を探すことができます。 ただし、Prolog の規則（Horn 節とも呼ばれます）をそのまま使うことは 完全にはできず、やや表現力の高い変種が必要になることがわかっています。
Rust のトレイトと論理
最初に得られる観察の 1 つは、Rust のトレイトシステムが 基本的に一種の論理であるということです。そのため、struct、trait、 impl の宣言を論理的推論規則へ対応付けることができます。大部分において、 これらは基本的に Horn 節ですが、Rust の表現力を完全に捉えるには、 特にジェネリックプログラミングをサポートするには、標準的な Horn 節より 少し先へ進む必要があることを見ていきます。
この対応付けがどのように機能するかを見るために、例から始めましょう。 次のようにトレイトといくつかの impl を宣言するとします。
#![allow(unused)]
fn main() {
trait Clone { }
impl Clone for usize { }
impl<T> Clone for Vec<T> where T: Clone { }
}これらの宣言は、Prolog 風の記法で書かれたいくつかの Horn 節へ、 次のように対応付けることができます。
Clone(usize).
Clone(Vec<?T>) :- Clone(?T).
// `A :- B` という記法は「B が真なら A は真である」ことを意味します。
// 別の言い方をすれば、B は A を含意します。
Prolog の用語では、Clone(Foo)（ここで Foo は何らかの
Rust の型です）は、型 Foo が Clone を実装しているという考えを表す
述語である、と言えるでしょう。これらの規則はプログラム節です。
つまり、その述語を証明できる（すなわち、真とみなせる）条件を述べています。
そのため、最初の規則は単に「usize に対して Clone が実装されている」と
言っています。次の規則は「任意の型 ?T について、?T に対して clone が
実装されているなら、Vec<?T> に対して Clone が実装されている」と
言っています。したがって、たとえば Clone(Vec<Vec<usize>>) を証明したい場合、
規則を再帰的に適用することでそれを行います。
Clone(Vec<Vec<usize>>)が証明可能であるのは、次の場合です。Clone(Vec<usize>)が証明可能である場合で、それは次の場合です。Clone(usize)が証明可能である場合です。（これは証明可能なので、問題ありません。）
しかし今度は、Clone(Vec<Bar>) を証明しようとしたとしましょう。
これは失敗します（結局のところ、Bar に対する Clone の impl は
与えていません）。
Clone(Vec<Bar>)が証明可能であるのは、次の場合です。Clone(Bar)が証明可能である場合です。（しかし、適用可能な規則がないため、これは証明可能ではありません。）
上の例は、複数の入力型を持つジェネリックなトレイトを扱うように
簡単に拡張できます。そこで、Eq<T> トレイトを考えてみましょう。
これは、Self が型 T の値と等価比較可能であることを宣言します。
trait Eq<T> { ... }
impl Eq<usize> for usize { }
impl<T: Eq<U>> Eq<Vec<U>> for Vec<T> { }これは次のように対応付けることができます。
Eq(usize, usize).
Eq(Vec<?T>, Vec<?U>) :- Eq(?T, ?U).
ここまでは順調です。
通常の関数の型チェック
さて、トレイトがいつ実装されるかを表現し、関連型を扱うことができる いくつかの論理規則を定義したので、少し焦点を型チェックへ 移しましょう。型チェックが興味深いのは、証明する必要があるゴールを 与えてくれるものだからです。つまり、ここまで見てきたことはすべて、 プログラム内のトレイトと impl から、ゴールを証明するための規則を どのように導出するかに関するものでした。しかし、私たちは証明する必要がある ゴールをどのように導出するかにも関心があります。そしてそれらは 型チェックから得られます。
ここで、関数 foo() の型チェックを考えてみましょう。
fn foo() { bar::<usize>() }
fn bar<U: Eq<U>>() { }もちろん、この関数は非常に単純です。行っているのは bar::<usize>() を
呼び出すことだけです。さて、bar() の定義を見ると、
U: Eq<U> という where 節が 1 つあることがわかります。つまり、
foo() が型引数として usize を指定して bar() を呼び出せることを
示すには、usize: Eq<usize> を証明する必要がある、ということです。
望むなら、bar() を呼び出せる条件を定義する Prolog の述語を書くことも
できます。ここでは、その条件を「well-formed」であることと呼ぶことにします。
barWellFormed(?U) :- Eq(?U, ?U).
すると、bar::<usize> への参照（つまり、型 usize に適用された
bar()）が well-formed であれば、foo() は型チェックに通る、と
言うことができます。
fooTypeChecks :- barWellFormed(usize).
ゴール fooTypeChecks を証明しようとすると、成功します。
fooTypeChecksが証明可能であるのは、次の場合です。barWellFormed(usize)の場合で、これは次の場合に証明可能です。Eq(usize, usize)の場合で、これは impl があるため証明可能です。
ここまでは順調です。より複雑な関数の型チェックへ進みましょう。
ジェネリック関数の型チェック: Horn 節を超えて
前のセクションでは、標準的な Prolog の Horn 節（Rust の型等価性の概念で
拡張したもの）を使用して、いくつかの単純な Rust 関数を型チェックしました。
しかし、それが機能するのは、非ジェネリック関数を型チェックしている場合に
限られます。ジェネリック関数を型チェックしたい場合、Prolog が提供できるものより
強いゴールの概念が必要になることがわかります。私が何を言っているのかを見るために、
前の例を改造して foo をジェネリックにしてみましょう。
fn foo<T: Eq<T>>() { bar::<T>() }
fn bar<U: Eq<U>>() { }foo の本体を型チェックするには、型 T を「抽象的」に保てる必要があります。
つまり、特定の何らかの型についてだけではなく、すべての型 T に対して
foo の本体が型安全であることをチェックする必要があります。これは次のように
表現できるでしょう。
fooTypeChecks :-
// すべての型 T について...
forall<T> {
// ...Eq(T, T) が証明可能であると仮定するなら...
if (Eq(T, T)) {
// ...`barWellFormed(T)` が成り立つことを証明できる。
barWellFormed(T)
}
}.
ここで使っている記法は、私がプロトタイプ実装で使ってきた記法です。
標準的な数学の記法に似ていますが、少し Rust 風になっています。いずれにせよ、
問題は、標準的な Horn 節ではゴール内で全称量化（forall）や含意（if）を
許可しないことです（ただし、多くの Prolog エンジンは拡張としてそれらを
サポートしています）。このため、「一階 hereditary Harrop」（FOHH）節と呼ばれるものを
受け入れる必要があります。この長い名前は、基本的には「本体内に forall と if を
持つ標準的な Horn 節」という意味です。しかし、正式な名前を知っておくのはよいことです。
FOHH 節を効率的に扱う方法を説明した研究が数多くあるからです。たとえば、
Gopalan Nadathur による優れた
「A Proof Procedure for the Logic of Hereditary Harrop Formulas」 を
Chalk Book の参考文献で参照してください。
FOHH のサポートは、実際にはそれほど難しいものではないことがわかっています。
そして、それができるようになれば、foo のようなジェネリック関数の
型チェック規則を、私たちのロジックで簡単に記述できます。
出典
このページは、 Nicholas Matsakis によるブログ記事を軽く改変したものです。