RustBelt試行中: get_x の一般化

Rust Coq

RustBeltの examples/get_x.v をいじってみた。

From iris.proofmode Require Import tactics.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".

Section get_x.
  Context `{typeG Σ}.

  Definition get_x : val :=
    funrec: <> ["p"] :=
       let: "p'" := !"p" in
       letalloc: "r" <- "p'" +ₗ #0 in
       delete [ #1; "p"] ;; return: ["r"].

  Lemma get_x_type :
    typed_val get_x (fn(∀ α, ∅; &uniq{α} Π[int; int]) → &shr{α} int).
  Proof.
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
    inv_vec p=>p. simpl_subst.
    iApply type_deref; [solve_typing..|]. iIntros (p'); simpl_subst.
    iApply (type_letalloc_1 (&shr{α}int)); [solve_typing..|]. iIntros (r). simpl_subst.
    iApply type_delete; [solve_typing..|].
    iApply type_jump; solve_typing.
  Qed.
End get_x.

これはだいたい以下のようなプログラムを表しているようだ。

fn get_x<'a>(p: &'a mut (i32, i32)) -> &'a i32 {
    &p.0
}

ただし、現在のλRustでは整数型はひとつしかなく、無限に大きな整数を保持可能で、サイズは1である (ポインタのサイズも1)。

これを

fn fst<'a, T, U>(p: &'a mut (T, U)) -> &'a T {
    &p.0
}

に一般化してみた。試行錯誤の結果、以下のようにすると上手くいくことがわかった。

From iris.proofmode Require Import tactics.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".

Section get_x.
  Context `{typeG Σ}.

  Definition get_x T U `{!TyWf T} `{!TyWf U} : val :=
    funrec: <> ["p"] :=
       let: "p'" := !"p" in
       letalloc: "r" <- "p'" +ₗ #0 in
       delete [ #1; "p"] ;; return: ["r"].

  Lemma get_x_type T U `{!TyWf T} `{!TyWf U} :
    typed_val (get_x T U) (fn(∀ α, ∅; &uniq{α} Π[T; U]) → &shr{α} T).
  Proof.
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
    inv_vec p=>p. simpl_subst.
    iApply type_deref; [solve_typing..|]. iIntros (p'); simpl_subst.
    iApply (type_letalloc_1 (&shr{α}T)); [solve_typing..|]. iIntros (r). simpl_subst.
    iApply type_delete; [solve_typing..|].
    iApply type_jump; solve_typing.
  Qed.
End get_x.

同様に、

fn snd<'a, T, U>(p: &'a mut (T, U)) -> &'a U {
    &p.1
}

は以下のように定義できた。

From iris.proofmode Require Import tactics.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".

Section snd.
  Context `{typeG Σ}.

  Definition snd T U `{!TyWf T} `{!TyWf U} : val :=
    funrec: <> ["p"] :=
       let: "p'" := !"p" in
       letalloc: "r" <- "p'" +ₗ #(T.(ty_size)) in
       delete [ #1; "p"] ;; return: ["r"].

  Lemma snd_type T U `{!TyWf T} `{!TyWf U} :
    typed_val (snd T U) (fn(∀ α, ∅; &uniq{α} Π[T; U]) → &shr{α} U).
  Proof.
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
    inv_vec p=>p. simpl_subst.
    iApply type_deref; [solve_typing..|]. iIntros (p'); simpl_subst.
    iApply (type_letalloc_1 (&shr{α}U)); [solve_typing..|]. iIntros (r). simpl_subst.
    iApply type_delete; [solve_typing..|].
    iApply type_jump; solve_typing.
  Qed.
End snd.

わかったこと

  • lrust.typing.typing をインポートするとよくて、 lrust.typing.lib.* に Cell 等のライブラリがある
  • lrust.typing.examples に例がある
  • `{typeG Σ} は共通のコンテキストとして出てくる
  • まずMIRもどきを Definition で与え、あとから Lemma で型をつける。
  • ライフタイムの多相性はλRustで扱われているが、型多相性はメタレベルで表現する。
  • funrec は関数定義。
  • ! はメモリを読む。
  • delete はサイズと先頭番地を引数に取りヒープまたはスタックを解放する。 (ヒープとスタックは同等に扱われる)
  • #x は定数リテラル。
  • +ₗ はポインタと整数の足し算。
  • 型は type で、これは @type _ H (H は冒頭の Context で宣言されているやつ)
  • 不正な再帰型を避けるために、各型がwell-formedであることの保証を持ち回す必要がある。これは `{!TyWf T} で実現できる。
  • ∀α, ∅; T は生存期間に関する量化で、 ∅ は多分境界がないことを意味している。
  • &uniq{α} T と &shr{α} T は &'a mut T と &'a T 。
  • Π[A; B; C] は (A, B, C)
  • std::mem::size_of::<T>() が欲しいときは #(T.(ty_size)) と書く
  • unsized typeのサポートは今のところなくて、 type は全部 Sized な型を表す

RustのRFC一覧 (～0900)

Rust

概要: RustのRFCの一覧を作ろうとしたが、あまりに多いのでとりあえず0900までで公開することにした。なお、単に全てのRFCを列挙したいならばここを見ればよい。

このRFCはRustのコミュニティーが管理しているものであり、 “RFC” の元祖であるIETF RFCとは関係ない。いずれもrequest-for-commentの略である。

メタ

  • RFC 0002 Rust RFCの提出プロセスの説明
  • RFC 0531 Rust RFCが関与する範囲を Rust/Cargo/Crates.io/このRFCプロセス自身 の4つに限定

スタイル/慣習

  • RFC 0199 似たような動作で、所有権/借用の種別だけが異なるようなメソッドの命名規則を定める
  • RFC 0236 panic!/Result の使い分けの慣習を定義する、関連するメソッドの命名規則を定める
  • RFC 0240 unsafe の慣習の整理: unsafe 関数をメソッドにする条件の定義、論理的な不変条件を壊すが未定義動作を引き起こさない関数は unsafe ではなく *_unchecked と命名することを定義、その他 unsafe 関数の命名規則の定義
  • RFC 0344 関数/メソッド名が型名に言及する際の命名規則 (Prelude* はRFC 0445により廃止され、Rust PR #23104により完全に不要になった)
  • RFC 0430 命名規則のケーシング(snake_case, CamelCase, etc.) と、 unwrap/into_* の命名規則を定義
  • RFC 0445 拡張トレイトパターンに使うトレイトの名前を *Ext とする命名規則
  • RFC 0505 doc-commentの慣習の確立: /// を優先的に使う。Markdownを使う

ソースファイル処理と字句

  • RFC 0063 二重インクルードによる混乱を防ぐため、 mod foo; による外部ファイルの読み込みに制限をつける
  • RFC 0069 バイトリテラル b'x' とバイト列リテラル b"Foo" の導入
  • RFC 0090/0021 字句解析器をより単純にする
  • RFC 0326 文字/文字列リテラルにおいて \x00-\x7F に限定し \x80-\xFF を禁止
  • RFC 0342 abstract, final, override をキーワードとして予約する
  • RFC 0446 文字/文字列リテラルの \uXXXX/\UXXXXXXXX を廃止し、 \u{XXXXXX} を導入
  • RFC 0463 将来の互換性のために、リテラル直後の識別子の字句規則を変更
  • RFC 0593 Self をキーワードにする
  • RFC 0601 将来の末尾再帰のための予約キーワード be を廃止し、新たに become を予約
  • RFC 0879 2進/8進リテラル直後の数字を禁止する (0b012 を 0b01 2 に分割せずにエラーにする)

構文

  • RFC 0016 属性を let 文、ブロック、式にも使えるようにする (#![feature(stmt_expr_attributes)])
  • RFC 0049 マッチ腕に属性を使えるようにする
  • RFC 0059 ~T 型と ~x 式を削除し、 Box/box で置き換える
  • RFC 0068 *T 型を *const T にリネーム
  • RFC 0071 const/static 内でも、一定条件下でブロックを使えるようにする
  • RFC 0087 トレイトオブジェクトの追加の境界を &(Foo : Send + Sync) ではなく &(Foo + Send + Sync) のように指定するようにする
  • RFC 0092 if や for などのブロックと紛らわしい場面では構造体の {} を禁止する
  • RFC 0132 UFCS (<T as Trait>::sth / <T>::sth) の導入
  • RFC 0135 where 節の導入 (一部未実装)
  • RFC 0160 if let 構文
  • RFC 0164 スライスパターンをfeature gateにする
  • RFC 0168 {mod, ..} によりモジュール自体とその中身を同時にインポートする (RFC 0532により廃止)
  • RFC 0169 use baz = foo::bar; 構文を廃止し use foo::bar as baz; で置き換える
  • RFC 0179 &p パターンを &p と &mut p パターンに分割し、参照のミュータビリティーに応じて使い分けるようにする
  • RFC 0184 foo.0 のように、タプル/タプル構造体のフィールドに整数でアクセスできるようにする
  • RFC 0194 #[cfg(...)] の構文の整理
  • RFC 0198 foo[]/foo[n..m]/foo[n..]/foo[..n] のためのトレイト Slice/SliceMut を導入 (RFC 0439とRFC 0702により廃止: foo[] は foo[..] になり、 .. は [] と独立な構文になった)
  • RFC 0202 [x, ..ys] パターンを [x, ys..] に変更 (#![feature(slice_patterns)]/#![feature(advanced_slice_patterns)] に注意)
  • RFC 0214 while let 構文
  • RFC 0218 空のレコード構造体 struct A {} を許可
  • RFC 0243 e? と (do) catch {} 構文によるエラー処理 (RFC 1859も参照。catch構文は#![feature(catch_expr)])
  • RFC 0339 バイト列リテラルの型を &'static [u8] から &'static [u8; N] に変更
  • RFC 0418 enum のバリアントをレコード形式 (enum Foo { Bar {}}) で宣言する機能を安定化
  • RFC 0438 型における & と + の優先順位を変更し、 &(Foo + Bar) のように書くようにする
  • RFC 0450 RFC 0184 (foo.0), RFC 0160 (if let), RFC 0214 (while let) の安定化, TupleN トレイトの廃止
  • RFC 0469 box p パターンをfeature gateにし、安定化するまで使用を禁止
  • RFC 0490 Sized? T 記法を T: ?Sized に変更
  • RFC 0520 配列型と繰り返しリテラルの構文 [x, ..N] を [x; N] に変更
  • RFC 0522 Self を impl 内でも使えるようにする (RFC 1647も参照)
  • RFC 0532 use foo::{self, X}; によりモジュール自体とその中身を同時にインポートする。RFC 0168のキーワード置き換え
  • RFC 0534 #[deriving(Foo)] を #[derive(Foo)] にリネーム
  • RFC 0544 int/uint を isize/usize にリネーム。対応するリテラル接尾辞を is/us に変更 (リテラル接尾辞 is/us はRFC 573で廃止)
  • RFC 0558 比較演算子を非結合的にし、 a == b == c をどうしても書きたい場合は (a == b) == c のように書くようにする
  • RFC 0572 将来の後方互換性のために、未知の属性(#[foo]等) をfeature gateにする(stableでの使用を禁止する)
  • RFC 0702 RangeFull とその構文糖衣 .. の導入。 foo[] 記法を廃止して foo[..] に置き換え
  • RFC 0803 型帰属 (type ascription): e: T による型の明示 (#![feature(type_ascription)])
  • RFC 0809 box (place) expr 構文を廃止して in place { block } に置き換える。かわりに box expr 構文を導入する。 (#[feature(placement_in_syntax)], #[feature(box_syntax)], RFC 1228も参照)

マクロ

  • RFC 0085 パターンの位置でマクロを使えるようにする
  • RFC 0378 文マクロには {} または ; を必須とし、どちらも持たないマクロは式マクロとして解釈する
  • RFC 0453 マクロのエクスポート (#[macro_export]/#[macro_reexport]/#[macro_use])、 $crate メタ変数、プラグインのための #[plugin] 属性
  • RFC 0550 macro_rules! のマッチャーとして、非曖昧な(おそらくLL(1)な)マッチャーだけを許可する
  • RFC 0873 型の位置でマクロを使えるようにする

モジュール・名前解決・可視性

  • RFC 0001 構造体フィールドの可視性をデフォルトでprivateにする。
  • RFC 0003 未使用の属性のチェック方法を改善する
  • RFC 0026 enum のバリアントの可視性を常にpublicにし、 priv キーワードを廃止する。
  • RFC 0109 バージョン込みでcrateを指定できるcrate idを廃止して、ソースコードレベルではcrateの名前だけを指定するようにする
  • RFC 0116 use/let 等による同レベルシャドウイングの廃止 (現在はglob importの復活により、globのshadowingが可能)
  • RFC 0136 publicな定義の型にprivateな型を使うのを禁止する
  • RFC 0155 固有実装は該当の型と同じモジュールでのみ可能 (RFC 0735により廃止)
  • RFC 0234 enum のバリアントは常に値名前空間と型名前空間の両方に属するようにする
  • RFC 0385 モジュールシステムの整理: use/mod 順の強制を廃止、pub extern crate を許可、 extern crate のブロック内の出現を許可
  • RFC 0390 バリアントを enum の名前空間の中に移動する。つまり、 enum Foo { Bar } で Bar ではなく Foo::Bar とアクセスする
  • RFC 0459 impl とその中の fn の間での、生存期間変数と型変数のシャドウイングを禁止
  • RFC 0501 #![no_implicit_prelude] を #![no_prelude] にリネームし、動作を変更
  • RFC 0735 固有実装は該当の型と異なるモジュールに置いてもよい
  • RFC 0736 構造体の関数型レコード更新記法(FRU) S { x: 42, ..old } において、更新されないフィールドの可視性もチェックする

型システム

  • RFC 0019 既定実装 impl Send for .. {}, 否定実装 impl !Send for T {} により Send/Sync をライブラリレベルで実現する (#![feature(optin_builtin_traits)])
  • RFC 0034/0011 struct/enum の型引数に境界 T: Trait を書けるようにし、それが充足されていることを利用側で検査する。
  • RFC 0048 トレイト周りの整理: self の一般化、coherence条件の整理、トレイト選択アルゴリズムの改善など
  • RFC 0111 Index を Index/IndexMut に分割する
  • RFC 0112/0033 Box<T> から &mut T への型強制の廃止(DerefMut型強制とは別) (RFC 0139も参照)
  • RFC 0115 整数リテラル型がデフォルトで isize にフォールバックしないようにする (RFC 0212により廃止)
  • RFC 0139 Box<T> から &T への型強制の廃止 (Deref型強制とは別) (RFC 0112も参照)
  • RFC 0195 関連型・関連定数・関連生存期間 (関連生存期間は未実装)
  • RFC 0212 RFC 0115をリバートするが、整数型のデフォルトは isize ではなく i32 にする
  • RFC 0213 fn/impl でもデフォルト型引数を使えるようにする。_ を型引数のデフォルト値の意味で使えるようにする (#![feature(default_type_parameter_fallback)])
  • RFC 0241 Deref型強制: &Rc<T> を &T に自動変換等
  • RFC 0255 トレイトにobject-safetyを課すようにする
  • RFC 0341 virtual構造体と継承 virtual struct Foo {} struct Bar : Foo {} の削除
  • RFC 0401 型強制とキャストの整理: スライスへの自動参照の削除、生ポインタ型強制、サブトレイト型強制、unsizedタプル型強制、推移的型強制、ユーザー定義型のunsize型強制など (RFC 0982, RFC 1558も参照; いくつかの機能は未実装)
  • RFC 0447 未使用だったり、一意でないような impl の型引数を禁止
  • RFC 0495 スライスパターン [x, xs..] の変更: [T] にはマッチするが &[T] にはマッチしない。可変借用の分割に対応 (#![feature(slice_patterns)]/#![feature(advanced_slice_patterns)] に注意)
  • RFC 0546 トレイトをデフォルトで ?Sized にする。 Sized なトレイトをobject-safeから外す。

クロージャ

  • RFC 0114 クロージャの整理: unboxed closureのための Fn/FnMut/FnOnce トレイトの導入、 proc の削除、クロージャ型を削除して |_| -> _ を構文糖衣に変更(構文糖衣はRFC 0231により廃止)、キャプチャー方式の指定、レシーバモード |:| |&:| |&mut :| の明示(RFC 0231により廃止)
  • RFC 0151 クロージャで ref を指定しない限りムーブキャプチャーする (RFC 0231により廃止)
  • RFC 0231 キャプチャーモードの推論方式を変更、 ref || を廃止して move || を導入、 |_| -> _ 型構文を廃止、レシーバモード |:| |&:| |&mut :| を廃止
  • RFC 0587 Fn* 系トレイトの戻り値型を型引数ではなく関連型にする

生存期間/ボローチェッカー/部分型付け

  • RFC 0066 一時的な値に対する参照を間接的に取った場合も、直接取った場合と同様にそ の生存期間を延長できるようにする
  • RFC 0107 パターンマッチのガード内でムーブ束縛された変数を使う (未実装)
  • RFC 0130 ボローチェッカーにおける Box<T> の特別扱いの廃止
  • RFC 0141 生存期間の省略規則の整理
  • RFC 0192 トレイトオブジェクト型の生存期間 (RFC 0599, RFC 1156も参照)
  • RFC 0246 static を const/static に分割
  • RFC 0387 高階トレイト境界 T: for<'a> Trait の導入
  • RFC 0533 配列の特定要素からのムーブと要素ごとの初期化を廃止
  • RFC 0599 トレイトオブジェクト型の生存期間の、外側の型にもとづくデフォルト値 (RFC 1156により上書き, RFC 0192も参照)
  • RFC 0738 部分型付けにおける変性(variance)を推論するようにし、変性のためのラッパー型を削除する。未使用の型引数/生存期間引数(=双変 bivariant な引数)はエラーにする。
  • RFC 0769 ドロップチェッカーの導入により、多相型の Drop を安全に実装できるようにする。 (RFC 1238により上書き)

コード生成/ABI

  • RFC 0008 extern "rust-intrinsic" の廃止 (破棄)
  • RFC 0079 #[repr(C)] などで明示しない限り、構造体レイアウトは入れ替えられる可能性がある
  • RFC 0320 構造体等からdrop flagフィールドを削除、変数ごとのdrop flagに移行 (RFC 0533も参照)
  • RFC 0379 ランタイムリフレクションと、それを用いた {:?} の削除、 libdebug/Poly の削除 ({:?} はRFC 0504により復活)

ライブラリ

  • RFC 0040 libstd の実装を libcore, liballoc, liblibc などのライブラリに分割する。
  • RFC 0042/0007 regex crateの同梱 (現在は同梱されていない)
  • RFC 0050 デバッグモードでのみ有効化される debug_assert!() の導入
  • RFC 0060 StrBuf を String にリネーム
  • RFC 0093 println! や format! から地域化の機能を削除し、構文を整理
  • RFC 0100 PartialOrd::partial_cmp を追加
  • RFC 0123 Share を Sync にリネーム
  • RFC 0201 std::error::Error トレイトによるエラーの相互変換
  • RFC 0216 HashMap 等でfindの結果を保持する Entry 型の導入
  • RFC 0221 fail!() を panic!() にリネーム
  • RFC 0230 標準ライブラリからグリーンスレッド関係の部分を削除
  • RFC 0235 コレクション関連ライブラリの整理と慣例の確立: Cow を導入、 Deque などの抽象化用トレイトを削除し Iterator を中心にした枠組みを整備、各種関数の命名規則を統一 (RFC 0509により上書き, RFC 0580によりリネーム)
  • RFC 0256 Gc<T>/@T (Rc<T> とは異なり、循環参照も解放される) の削除
  • RFC 0356 型名にモジュール名を含めない慣習を定義し、 io::IoError を io::Error にリネーム
  • RFC 0369 std::num にあった様々な抽象的な数値型トレイトの削除 (現在は Signed も含め大部分が削除され num crateに移管済み)
  • RFC 0380 std::fmt の安定化
  • RFC 0439 std::cmp と std::ops の整理: 演算子オーバーロードトレイトの整理、ヘテロジェニアスな Eq, Slice/SliceMutを削除してRange*型を導入、IndexSetの導入 (IndexSet は実装されていない模様; RFC issue #997 も参照)
  • RFC 0458 Send: 'static を削除、 &T: Send ←→ T: Sync
  • RFC 0461 タスクローカル領域のための std::local_data を整理してスレッドローカル領域のための std::tls を導入 (現在は std::thread に統合)
  • RFC 0474 std::path の整理: 正規化の意味論を変更、UTF-8とは限らないパスのために PathBuf/OsPath 型を新たに導入
  • RFC 0486 std::ascii::Ascii 型を削除して ascii 外部crateに分離
  • RFC 0494 std::c_vec を廃止、 std::c_str を std::ffi にリネーム、 CString の所有権の扱いを変更
  • RFC 0503 std::prelude からいくつかの名前を削除し、安定化
  • RFC 0504 Show を String(現在のDisplay)とShow(現在のDebug)に分割し、新しい Show のために {:?} を割り当て (RFC 0565により現在の名前に変更)
  • RFC 0509 コレクション関連ライブラリの整備、RFC 0235の続き。いくつかのコレクションAPIの削除。コレクションAPIの安定化。 (RFC 0580によりリネーム)
  • RFC 0517 std::io と std::os の大改革。 env fs io net os os_str process への分割。アトミック性に関する意味論の整理。非utf-8文字列のサポート。ブロッキングI/Oに注力しつつ、ノンブロッキング/非同期IOのための前方互換性は確保するようにする。など
  • RFC 0526 任意のバイト列を出力できてしまう std::fmt::Formatter::write 関数を削除することで、UTF-8チェックのコストを削減
  • RFC 0528 文字列のパターン検索のための Pattern トレイトを導入
  • RFC 0529 汎用的な変換トレイト AsRef, AsMut, Into, From の導入
  • RFC 0556 from_raw* 系関数のインターフェースを変更し、誤用を防ぐためドキュメントを充実させる
  • RFC 0560 整数演算オーバーフローの意味論を変更し、条件次第でpanicしうるとする。オーバーフロー時に常に巡回させたい場合のためのメソッド wrapping_* を用意する
  • RFC 0565 std::fmt::String と std::fmt::Show を Display, Debug にリネーム
  • RFC 0574 Vec::drain, String::drain がバッファの一部だけをドレインできるようにする
  • RFC 0580 コレクション関連ライブラリのリネーム (DList→LinkedList, RingBuf→VecDequeなど)
  • RFC 0592 String/str に対して、 CString の対応物である CStr を導入する
  • RFC 0640 {:#?} によるpretty printingの導入と、 Debug の実装のためのヘルパー型の整備
  • RFC 0771 std::iter::once と std::iter::empty の追加
  • RFC 0823 std::hash の整理: Hasher トレイトと Writer トレイトの統一 write_u*/write_i* メソッドの導入、 reset メソッドの削除
  • RFC 0832 vec![e; n] 記法のための vec::from_elem 関数 (この関数は確かに追加され、現在は alloc::vec::from_elem で公開されているが、 #[doc(hidden)] で隠されている)
  • RFC 0839 どんなコレクションでも、要素が Copy なら参照イテレータから extend できるように Extend を実装する
  • RFC 0840 CString::from_slice, CString::from_vec はpanicせずに Result を返す (実際のRust PR #22482 ではさらに、これらを CString::new に統一している)
  • RFC 0888 コンパイラ用のメモリフェンス指令 std::intrinsics::atomic_singlethreadfence(_rel|_acq|_acqrel)? を追加

コンパイラ/リンカ/Cargo

RustBeltのビルド (Windows)

Rust Coq

概要: Coqと高階分離論理を用いたRustの検証プロジェクトであるRustBeltの論文とCoqの証明ファイルが公開されたので、とりあえずビルドしてみた。

RustBeltはopamを使うと簡単にビルドできるようだが、ここではWindowsでビルドしてみた。

環境

gitとmakeのインストール

$ pacman -S make git

Coqのインストール

CoqのWebサイト から coq-installer-8.6-x86_64.exe をダウンロードし、実行する。今回はデフォルトのディレクトリ C:\Coq にインストールした。

/c/Coq/bin をPATHに追加する。例えば .zshrc に

export PATH="${PATH}:/c/Coq/bin"

と書く。

ssreflect/mathcompのインストール

依存関係: Coq, make

ssreflect/mathcompのWebサイト から ssreflect-mathcomp-installer-1.6.1-win64.exe をダウンロードし、実行する。Coqのインストールディレクトリと同じディレクトリ C:\Coq を指定する。ssreflectは %COQDIR%\lib\user-contrib\mathcomp にインストールされる。

coq-std++のビルドとインストール

依存関係: Coq, git, make

$ git clone -b ee6200b4d74bfd06034f3cc36d1afdc309427e5c https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git
$ cd coq-stdpp
$ make && make install

Irisのビルドとインストール

依存関係: Coq, ssreflect/mathcomp, git, make, coq-std++

$ git clone -b 398bae9d092b6568cf8d504ca98d8810979eea33 https://gitlab.mpi-sws.org/FP/iris-coq.git
$ cd iris-coq
$ make && make install

RustBeltのビルド

依存関係: Coq, ssreflect/mathcomp, git, make, coq-std++, iris

RustBeltのWebサイトの “RustBelt: Securing the Foundations of the Rust Programming Language.” という論文のappendixをダウンロードする。 appendix.zip を解凍する。

$ cd appendix/lambdaRust
$ make && make install

以上

RustのRFC一覧 (～0500)

Rust

概要: RustのRFCの一覧を作ろうとしたが、あまりに多いのでとりあえず0500までで公開することにした。なお、単に全てのRFCを列挙したいならばここを見ればよい。

このRFCはRustのコミュニティーが管理しているものであり、 “RFC” の元祖であるIETF RFCとは関係ない。いずれもrequest-for-commentの略である。

メタ

スタイル/慣習

  • RFC 0199 似たような動作で、所有権/借用の種別だけが異なるようなメソッドの命名規則を定める
  • RFC 0236 panic!/Result の使い分けの慣習を定義する、関連するメソッドの命名規則を定める
  • RFC 0240 unsafe の慣習の整理: unsafe 関数をメソッドにする条件の定義、論理的な不変条件を壊すが未定義動作を引き起こさない関数は unsafe ではなく *_unchecked と命名することを定義、その他 unsafe 関数の命名規則の定義
  • RFC 0344 関数/メソッド名が型名に言及する際の命名規則 (Prelude* はRFC 0445により廃止され、Rust PR #23104により完全に不要になった)
  • RFC 0430 命名規則のケーシング(snake_case, CamelCase, etc.) と、 unwrap/into_* の命名規則を定義
  • RFC 0445 拡張トレイトパターンに使うトレイトの名前を *Ext とする命名規則

ソースファイル処理と字句

  • RFC 0063 二重インクルードによる混乱を防ぐため、 mod foo; による外部ファイルの読み込みに制限をつける
  • RFC 0069 バイトリテラル b'x' とバイト列リテラル b"Foo" の導入
  • RFC 0090/0021 字句解析器をより単純にする
  • RFC 0326 文字/文字列リテラルにおいて \x00-\x7F に限定し \x80-\xFF を禁止
  • RFC 0342 abstract, final, override をキーワードとして予約する
  • RFC 0446 文字/文字列リテラルの \uXXXX/\UXXXXXXXX を廃止し、 \u{XXXXXX} を導入
  • RFC 0463 将来の互換性のために、リテラル直後の識別子の字句規則を変更

構文

  • RFC 0016 属性を let 文、ブロック、式にも使えるようにする (#![feature(stmt_expr_attributes)])
  • RFC 0049 マッチ腕に属性を使えるようにする
  • RFC 0059 ~T 型と ~x 式を削除し、 Box/box で置き換える
  • RFC 0068 *T 型を *const T にリネーム
  • RFC 0071 const/static 内でも、一定条件下でブロックを使えるようにする
  • RFC 0087 トレイトオブジェクトの追加の境界を &(Foo : Send + Sync) ではなく &(Foo + Send + Sync) のように指定するようにする
  • RFC 0092 if や for などのブロックと紛らわしい場面では構造体の {} を禁止する
  • RFC 0132 UFCS (<T as Trait>::sth / <T>::sth) の導入
  • RFC 0135 where 節の導入 (一部未実装)
  • RFC 0160 if let 構文
  • RFC 0164 スライスパターンをfeature gateにする
  • RFC 0168 {mod, ..} によりモジュール自体とその中身を同時にインポートする (RFC 0532により廃止)
  • RFC 0169 use baz = foo::bar; 構文を廃止し use foo::bar as baz; で置き換える
  • RFC 0179 &p パターンを &p と &mut p パターンに分割し、参照のミュータビリティーに応じて使い分けるようにする
  • RFC 0184 foo.0 のように、タプル/タプル構造体のフィールドに整数でアクセスできるようにする
  • RFC 0194 #[cfg(...)] の構文の整理
  • RFC 0198 foo[]/foo[n..m]/foo[n..]/foo[..n] のためのトレイト Slice/SliceMut を導入 (RFC 0439により廃止: foo[] は foo[..] になり、 .. は [] と独立な構文になった)
  • RFC 0202 [x, ..ys] パターンを [x, ys..] に変更 (#![feature(slice_patterns)]/#![feature(advanced_slice_patterns)] に注意)
  • RFC 0214 while let 構文
  • RFC 0218 空のレコード構造体 struct A {} を許可
  • RFC 0243 e? と (do) catch {} 構文によるエラー処理 (RFC 1859も参照。catch構文は#![feature(catch_expr)])
  • RFC 0339 バイト列リテラルの型を &'static [u8] から &'static [u8; N] に変更
  • RFC 0418 enum のバリアントをレコード形式 (enum Foo { Bar {}}) で宣言する機能を安定化
  • RFC 0438 型における & と + の優先順位を変更し、 &(Foo + Bar) のように書くようにする
  • RFC 0450 RFC 0184 (foo.0), RFC 0160 (if let), RFC 0214 (while let) の安定化, TupleN トレイトの廃止
  • RFC 0469 box p パターンをfeature gateにし、安定化するまで使用を禁止
  • RFC 0490 Sized? T 記法を T: ?Sized に変更

マクロ

  • RFC 0085 パターンの位置でマクロを使えるようにする
  • RFC 0378 文マクロには {} または ; を必須とし、どちらも持たないマクロは式マクロとして解釈する
  • RFC 0453 マクロのエクスポート (#[macro_export]/#[macro_reexport]/#[macro_use])、 $crate メタ変数、プラグインのための #[plugin] 属性

モジュール・名前解決・可視性

  • RFC 0001 構造体フィールドの可視性をデフォルトでprivateにする。
  • RFC 0003 未使用の属性のチェック方法を改善する
  • RFC 0026 enum のバリアントの可視性を常にpublicにし、 priv キーワードを廃止する。
  • RFC 0109 バージョン込みでcrateを指定できるcrate idを廃止して、ソースコードレベルではcrateの名前だけを指定するようにする
  • RFC 0116 use/let 等による同レベルシャドウイングの廃止 (現在はglob importの復活により、globのshadowingが可能)
  • RFC 0136 publicな定義の型にprivateな型を使うのを禁止する
  • RFC 0155 固有実装は該当の型と同じモジュールでのみ可能 (RFC 0735により廃止)
  • RFC 0234 enum のバリアントは常に値名前空間と型名前空間の両方に属するようにする
  • RFC 0385 モジュールシステムの整理: use/mod 順の強制を廃止、pub extern crate を許可、 extern crate のブロック内の出現を許可
  • RFC 0390 バリアントを enum の名前空間の中に移動する。つまり、 enum Foo { Bar } で Bar ではなく Foo::Bar とアクセスする
  • RFC 0459 impl とその中の fn の間での、生存期間変数と型変数のシャドウイングを禁止

型システム

  • RFC 0019 既定実装 impl Send for .. {}, 否定実装 impl !Send for T {} により Send/Sync をライブラリレベルで実現する (#![feature(optin_builtin_traits)])
  • RFC 0034/0011 struct/enum の型引数に境界 T: Trait を書けるようにし、それが充足されていることを利用側で検査する。
  • RFC 0048 トレイト周りの整理: self の一般化、coherence条件の整理、トレイト選択アルゴリズムの改善など
  • RFC 0111 Index を Index/IndexMut に分割する
  • RFC 0112/0033 Box<T> から &mut T への型強制の廃止(DerefMut型強制とは別) (RFC 0139も参照)
  • RFC 0115 整数リテラル型がデフォルトで isize にフォールバックしないようにする (RFC 0212により廃止)
  • RFC 0139 Box<T> から &T への型強制の廃止 (Deref型強制とは別) (RFC 0112も参照)
  • RFC 0195 関連型・関連定数・関連生存期間 (関連生存期間は未実装)
  • RFC 0212 RFC 0115をリバートするが、整数型のデフォルトは isize ではなく i32 にする
  • RFC 0213 fn/impl でもデフォルト型引数を使えるようにする。_ を型引数のデフォルト値の意味で使えるようにする (#![feature(default_type_parameter_fallback)])
  • RFC 0241 Deref型強制: &Rc<T> を &T に自動変換等
  • RFC 0255 トレイトにobject-safetyを課すようにする
  • RFC 0341 virtual構造体と継承 virtual struct Foo {} struct Bar : Foo {} の削除
  • RFC 0401 型強制とキャストの整理: スライスへの自動参照の削除、生ポインタ型強制、サブトレイト型強制、unsizedタプル型強制、推移的型強制、ユーザー定義型のunsize型強制など (RFC 0982, RFC 1558も参照; いくつかの機能は未実装)
  • RFC 0447 未使用だったり、一意でないような impl の型引数を禁止
  • RFC 0495 スライスパターン [x, xs..] の変更: [T] にはマッチするが &[T] にはマッチしない。可変借用の分割に対応 (#![feature(slice_patterns)]/#![feature(advanced_slice_patterns)] に注意)

クロージャ

  • RFC 0114 クロージャの整理: unboxed closureのための Fn/FnMut/FnOnce トレイトの導入、 proc の削除、クロージャ型を削除して |_| -> _ を構文糖衣に変更(構文糖衣はRFC 0231により廃止)、キャプチャー方式の指定、レシーバモード |:| |&:| |&mut :| の明示(RFC 0231により廃止)
  • RFC 0151 クロージャで ref を指定しない限りムーブキャプチャーする (RFC 0231により廃止)
  • RFC 0231 キャプチャーモードの推論方式を変更、 ref || を廃止して move || を導入、 |_| -> _ 型構文を廃止、レシーバモード |:| |&:| |&mut :| を廃止

生存期間/ボローチェッカー

  • RFC 0066 一時的な値に対する参照を間接的に取った場合も、直接取った場合と同様にそ の生存期間を延長できるようにする
  • RFC 0107 パターンマッチのガード内でムーブ束縛された変数を使う (未実装)
  • RFC 0130 ボローチェッカーにおける Box<T> の特別扱いの廃止
  • RFC 0141 生存期間の省略規則の整理
  • RFC 0192 トレイトオブジェクト型の生存期間 (RFC 0599, RFC 1156も参照)
  • RFC 0246 static を const/static に分割
  • RFC 0387 高階トレイト境界 T: for<'a> Trait の導入

コード生成/ABI

  • RFC 0008 extern "rust-intrinsic" の廃止 (破棄)
  • RFC 0079 #[repr(C)] などで明示しない限り、構造体レイアウトは入れ替えられる可能性がある
  • RFC 0320 構造体等からdrop flagフィールドを削除、変数ごとのdrop flagに移行
  • RFC 0379 ランタイムリフレクションと、それを用いた {:?} の削除、 libdebug/Poly の削除 ({:?} はRFC 0504により復活)

ライブラリ

  • RFC 0040 libstd の実装を libcore, liballoc, liblibc などのライブラリに分割する。
  • RFC 0042/0007 regex crateの同梱 (現在は同梱されていない)
  • RFC 0050 デバッグモードでのみ有効化される debug_assert!() の導入
  • RFC 0060 StrBuf を String にリネーム
  • RFC 0093 println! や format! から地域化の機能を削除し、構文を整理
  • RFC 0100 PartialOrd::partial_cmp を追加
  • RFC 0123 Share を Sync にリネーム
  • RFC 0201 std::error::Error トレイトによるエラーの相互変換
  • RFC 0216 HashMap 等でfindの結果を保持する Entry 型の導入
  • RFC 0221 fail!() を panic!() にリネーム
  • RFC 0230 標準ライブラリからグリーンスレッド関係の部分を削除
  • RFC 0235 コレクション関連ライブラリの整理と慣例の確立: Cow を導入、 Deque などの抽象化用トレイトを削除し Iterator を中心にした枠組みを整備、各種関数の命名規則を統一
  • RFC 0256 Gc<T>/@T (Rc<T> とは異なり、循環参照も解放される) の削除
  • RFC 0356 型名にモジュール名を含めない慣習を定義し、 io::IoError を io::Error にリネーム
  • RFC 0369 std::num にあった様々な抽象的な数値型トレイトの削除 (現在は Signed も含め大部分が削除され num crateに移管済み)
  • RFC 0380 std::fmt の安定化
  • RFC 0439 std::cmp と std::ops の整理: 演算子オーバーロードトレイトの整理、ヘテロジェニアスな Eq, Slice/SliceMutを削除してRange*型を導入、IndexSetの導入 (IndexSet は実装されていない模様; RFC issue #997 も参照)
  • RFC 0458 Send: 'static を削除、 &T: Send ←→ T: Sync
  • RFC 0461 タスクローカル領域のための std::local_data を整理してスレッドローカル領域のための std::tls を導入 (現在は std::thread に統合)
  • RFC 0474 std::path の整理: 正規化の意味論を変更、UTF-8とは限らないパスのために PathBuf/OsPath 型を新たに導入
  • RFC 0486 std::ascii::Ascii 型を削除して ascii 外部crateに分離
  • RFC 0494 std::c_vec を廃止、 std::c_str を std::ffi にリネーム、 CString の所有権の扱いを変更

コンパイラ/リンカ/Cargo

RustのRFC一覧 (～0200)

Rust

この記事は古いのでこちらをご覧ください

概要: RustのRFCの一覧を作ろうとしたが、あまりに多いのでとりあえず0200までで公開することにした。なお、単に全てのRFCを列挙したいならばここを見ればよい。

このRFCはRustのコミュニティーが管理しているものであり、 “RFC” の元祖であるIETF RFCとは関係ない。いずれもrequest-for-commentの略である。

メタ

スタイル

  • RFC 0199 似たような動作で、所有権/借用の種別だけが異なるようなメソッドの命名規則を定める

構文

  • RFC 0016 属性を let 文、ブロック、式にも使えるようにする (#![feature(stmt_expr_attributes)])
  • RFC 0049 マッチ腕に属性を使えるようにする
  • RFC 0059 ~T 型と ~x 式を削除し、 Box/box で置き換える
  • RFC 0063 二重インクルードによる混乱を防ぐため、 mod foo; による外部ファイルの読み込みに制限をつける
  • RFC 0068 *T 型を *const T にリネーム
  • RFC 0069 バイトリテラル b'x' とバイト列リテラル b"Foo" の導入
  • RFC 0071 const/static 内でも、一定条件下でブロックを使えるようにする
  • RFC 0085 パターンの位置でマクロを使えるようにする
  • RFC 0087 トレイトオブジェクトの追加の境界を &(Foo : Send + Sync) ではなく &(Foo + Send + Sync) のように指定するようにする
  • RFC 0090/0021 字句解析器をより単純にする
  • RFC 0092 if や for などのブロックと紛らわしい場面では構造体の {} を禁止する
  • RFC 0132 UFCS (<T as Trait>::sth / <T>::sth) の導入
  • RFC 0135 where 節の導入 (一部未実装)
  • RFC 0160 if let 構文
  • RFC 0164 スライスパターンをfeature gateにする
  • RFC 0168 {mod, ..} によりモジュール自体とその中身を同時にインポートする (RFC 0532により廃止)
  • RFC 0169 use baz = foo::bar; 構文を廃止し use foo::bar as baz; で置き換える
  • RFC 0179 &p パターンを &p と &mut p パターンに分割し、参照のミュータビリティーに応じて使い分けるようにする
  • RFC 0184 foo.0 のように、タプル/タプル構造体のフィールドに整数でアクセスできるようにする
  • RFC 0194 #[cfg(...)] の構文の整理
  • RFC 0198 foo[]/foo[n..m]/foo[n..]/foo[..n] のためのトレイト Slice/SliceMut を導入 (RFC 0439により廃止: foo[] は foo[..] になり、 .. は [] と独立な構文になった)

意味論・型システム

  • RFC 0001 構造体フィールドの可視性をデフォルトでprivateにする。
  • RFC 0003 未使用の属性のチェック方法を改善する
  • RFC 0008 extern "rust-intrinsic" の廃止 (破棄)
  • RFC 0019 既定実装 impl Send for .. {}, 否定実装 impl !Send for T {} により Send/Sync をライブラリレベルで実現する (#![feature(optin_builtin_traits)])
  • RFC 0026 enum のバリアントの可視性を常にpublicにし、 priv キーワードを廃止する。
  • RFC 0034/0011 struct/enum の型引数に境界 T: Trait を書けるようにし、それが充足されていることを利用側で検査する。
  • RFC 0048 トレイト周りの整理: self の一般化、coherence条件の整理、トレイト選択アルゴリズムの改善など
  • RFC 0066 一時的な値に対する参照を間接的に取った場合も、直接取った場合と同様にその生存期間を延長できるようにする
  • RFC 0079 #[repr(C)] などで明示しない限り、構造体レイアウトは入れ替えられる可能性がある
  • RFC 0107 パターンマッチのガード内でムーブ束縛された変数を使う (未実装)
  • RFC 0109 バージョン込みでcrateを指定できるcrate idを廃止して、ソースコードレベルではcrateの名前だけを指定するようにする
  • RFC 0111 Index を Index/IndexMut に分割する
  • RFC 0112/0033 Box<T> から &mut T への型強制の廃止(DerefMut型強制とは別) (RFC 0139も参照)
  • RFC 0114 クロージャの整理: unboxed closureのための Fn/FnMut/FnOnce トレイトの導入、 proc の削除、クロージャ型を削除して |_| -> _ を構文糖衣に変更(構文糖衣は現在は廃止)、キャプチャー方式の指定、レシーバモードの明示(現在は廃止)
  • RFC 0115 整数リテラル型がデフォルトで i32 にフォールバックしないようにする (RFC 0212により廃止)
  • RFC 0116 use/let 等による同レベルシャドウイングの廃止 (現在はglob importの復活により、globのshadowingが可能)
  • RFC 0130 ボローチェッカーにおける Box<T> の特別扱いの廃止
  • RFC 0136 publicな定義の型にprivateな型を使うのを禁止する
  • RFC 0139 Box<T> から &T への型強制の廃止 (Deref型強制とは別) (RFC 0112も参照)
  • RFC 0141 生存期間の省略規則の整理
  • RFC 0151 クロージャで ref を指定しない限りムーブキャプチャーする (RFC 0231により廃止)
  • RFC 0155 固有実装は該当の型と同じモジュールでのみ可能 (RFC 0735により廃止)
  • RFC 0192 トレイトオブジェクト型の生存期間 (RFC 0599も参照)
  • RFC 0195 関連型・関連定数・関連生存期間 (関連生存期間は未実装)

ライブラリ

  • RFC 0040 libstd の実装を libcore, liballoc, liblibc などのライブラリに分割する。
  • RFC 0042/0007 regex crateの同梱 (現在は同梱されていない)
  • RFC 0050 デバッグモードでのみ有効化される debug_assert!() の導入
  • RFC 0060 StrBuf を String にリネーム
  • RFC 0093 println! や format! から地域化の機能を削除し、構文を整理
  • RFC 0100 PartialOrd::partial_cmp を追加
  • RFC 0123 Share を Sync にリネーム

コンパイラ

Rustのトレイト選択

Rust

概要: トレイト選択とは、トレイト制約の解決方法を検索するコンパイラの処理であり、型推論にもコード生成にも使われる重要な部品である。本記事ではトレイト選択の動作の詳細について解説する。

トレイト選択とは

トレイト選択 (selection) とは、トレイト制約 (obligation) の解決方法を検索する処理である。トレイト制約は、トレイト境界と同じく、

SomeType: SomeTrait<SomeArguments>

という形式をとる。例えば、

let z = x + y;

というコードを書いたとき、 z の型は <X as Add<Y>>::Output であるが、これをより具体的に決定するには、 X: Add<Y> の解決方法を決定する必要がある。

トレイト選択の処理はtraits/select.rsにまとまっているのでここを読むとだいたいわかる。

トレイト選択が呼ばれるタイミング

トレイト選択の本体は select関数 である。これは主に以下のような場所で呼ばれる。

  • 型推論において型を1段階以上解決する必要が生じた場合。 (今あるトレイト制約それぞれについて解決を試みるが、失敗してもよい)
  • 型推論の最後。 (全てのトレイト制約を解決する)
  • 定数式の評価中。 (関連定数・constメソッド等の解決)
  • 単相化後のコード生成。

特に、型推論中のトレイト選択では、型引数を含む上、型の判明していない型推論変数もある。そのためこの時点ではトレイト選択の結果が曖昧である可能性がある。

トレイト制約の解決方法

トレイト制約はいくつかの異なる方法で解決される。それらの分類を与えているのがSelectionCandidateである。

  • ImplCandidate … 最も標準的な解決方法。トレイト実装 (impl MyTrait for SomeType { .. }) により解決する。 (否定実装もこれに含まれる)
  • ParamCandidate … 最も標準的な解決方法。型引数等に対するトレイト境界 (fn f<T: Clone> の T: Clone など) により解決する。
  • DefaultImplCandidate … 既定実装 impl Send for .. {} により解決する。
  • ProjectionCandidate … 射影型のトレイト制約を、関連型に対するトレイト境界 (type Owned: Borrow<Self>; など) により解決する。または、匿名型 (impl Trait) のトレイト制約を、それ自身により解決する。
  • ObjectCandidate … トレイトオブジェクトのトレイト制約を、それ自身により解決する。
  • 特定のトレイトに対するビルトインの解決方法
    • BuiltinCandidate … Copy/Sized 制約を組込みの方法により解決する。
    • BuiltinUnsizeCandidate … Unsize 制約を組込みの方法により解決する。
    • BuiltinObjectCandidate … トレイトオブジェクトに追加で付与される Send/Sync 境界により解決する。
    • ClosureCandidate/FnPointerCandidate … 関数ポインタ型 fn() や |args| { .. } によるクロージャ匿名型 [closure@..] に対する Fn/FnMut/FnOnce を組込みの方法により解決する。

ImplCandidate と ParamCandidate は、この時点では全く別物であることに注意する。例えば X: Add<Y> を解決する場合でも、

fn f(x: i32, y: i32) {
    let z = x + y;
}

であれば ImplCandidate が選択されるが、

fn f<X: Add<Y>, Y>(x: X, y: Y) {
    let z = x + y;
}

であれば ParamCandidate が選択される。

トレイト選択の流れ

トレイト選択は以下の手順で行われる。

基本的には、収集・選別をして候補が2つ以上になったら曖昧、候補が0個だったり承認されなかったら失敗、それ以外の場合は成功である。また、型環境への副作用は承認の段階で発生する。

実装候補の収集と承認

実装候補の収集

実装候補の収集は以下のように行われる。

  • 該当トレイトに対する既知のトレイト実装を列挙する。
  • 各トレイト実装の型引数/生存期間変数をフレッシュな型変数/生存期間変数で置き換える。
  • トレイト実装のヘッダとトレイト制約の単一化を試みる。
  • 単一化の成否にかかわらず、型環境を直前の状態にロールバックする。
  • 単一化が成功した実装を、候補として残す。

例えば、 Vec<Box<i32>>: MyTrait<Vec<Box<i8>>> というトレイト制約に対し、

  • impl<T: Copy, U: Copy> MyTrait<Vec<T>> for Vec<U> { .. } は候補である。 (単一化に成功するため。実装に含まれるトレイト境界は満たされていないが、これは収集には関係ない。)
  • impl<T> MyTrait<Vec<T>> for Vec<T> { .. } は候補ではない。 (単一化に失敗するため)

実装候補の承認

実装候補の承認は以下のように行われる。

  • 単一化を行う。
  • where 等で指定されたトレイト境界をトレイト制約として追加する。

型引数候補の収集と承認

型引数候補の収集

型引数候補の収集は以下のように行われる。

  • where 節等のトレイト境界を列挙する。
  • 各トレイト境界を、トレイト制約と単一化し、成功したら候補に加える。
  • 単一化の成否にかかわらず、元の状態にロールバックする。

型引数候補の承認

型引数候補の承認は以下のように行われる。

  • 該当トレイト境界を、トレイト制約と単一化する。

既定実装候補の収集と承認

既定実装候補の収集

既定実装は impl Send for .. {} のように .. という記号を使って与えられる特殊な実装で、主に Send, Sync, UnwindSafe, RefUnwindSafe が用いている。

既定実装候補の収集 は条件つきで実行される。つまり、他に候補がない場合にのみ既定実装候補がチェックされる。この規則があるため、収集と選別を区別して考える必要がある。

さて、他に候補がない場合の既定実装候補の収集は以下のように行われる。

  • トレイトオブジェクト型には既定実装は使われない。 (必要なら &(Foo + Sync) のようにしたり、trait Foo : Sync のようにしたりする)
  • 型引数には既定実装は使われない。 (必要なら fn f<T: Send> のように明示する)
  • 射影型には既定実装は使われない。 (必要なら trait Foo { type X : Send; } のように明示する)
  • それ以外の型に対しては既定実装候補を残す。特に、 impl Trait 型には既定実装が適用される。
  • 型変数の場合は、上記のどちらの場合に落ちるかわからないため、曖昧となる。

既定実装候補の承認

既定実装候補の承認は以下のように行われる。なお、既定実装をもつことができるトレイトは、 Send や Sync のように引数をとらないマーカートレイトに限られる。

  • Self 型の各メンバーに、再帰的にトレイト制約を追加する。

ただし、各メンバーとは以下のことを指す:

  • 整数・浮動小数点数・bool・char・str・関数ポインタ・関数定義・!: なし
  • ポインタ・参照: 参照先の型
  • 配列・スライス: 要素型
  • PhantomData<T>: T
  • タプル・構造体・共用体・列挙型: 全てのメンバーの型
  • クロージャ: キャプチャーされた変数の型。ただし参照キャプチャーされた場合はその参照型。
  • impl Trait: 匿名化される前の型。

射影候補の収集と承認

射影候補の収集

射影候補の収集は以下のようにして行われる。

  • Self 型が射影型なら、関連型の境界を列挙する。
  • Self 型が impl Trait 型なら、 impl Trait 内の Trait を列挙する。
  • これらのそれぞれと単一化し、どれか一つでも成功したら候補として採用する。
  • 単一化の成否にかかわらず、型環境は元の状態にロールバックする。

現在の実装では、複数の候補があった場合、曖昧にはならず、最初のものが採用される。

射影候補の承認

射影候補の承認は以下のようにして行われる。

  • Self 型が射影型なら、関連型の境界を列挙する。
  • Self 型が impl Trait 型なら、 impl Trait 内の Trait を列挙する。
  • これらのそれぞれと単一化し、失敗したらロールバックする。成功したらロールバックせず終了する。

トレイトオブジェクト候補の収集と承認

トレイトオブジェクト候補の収集

トレイトオブジェクト候補の収集は以下のようにして行われる。

  • トレイト制約のトレイトがobject-safeでないなら何もしない。
  • トレイト制約の Self 型がトレイトオブジェクト型でないなら何もしない。 Self 型が型推論変数の場合は曖昧となる。
  • トレイトオブジェクト型に追加の Send/Sync 境界があり、これがトレイト制約と一致する場合は、組込みトレイトオブジェクト候補として採用し、終了する。
  • それ以外の場合は、トレイトオブジェクト型の主境界のスーパートレイト境界を(型引数込みで)推移的に求め、トレイト制約と単一化できるものを列挙する。(trait Foo: Bar<i32> + Bar<i8> のように、同じトレイトの複数のスーパートレイト境界を持つ可能性もある)
  • 残ったスーパートレイト境界がちょうど1個ならそれを候補にする。それ以外の場合は曖昧と報告する。

トレイトオブジェクト候補の承認

トレイトオブジェクト候補の承認は収集とほぼ同様だが、単一化に成功した場合はロールバックせずに型環境に対する変更をコミットする。

なお、組込みトレイトオブジェクト候補(追加の Send/Sync 境界に由来する候補) の承認は何もしない。

クロージャ候補/関数ポインタ候補の収集と承認

クロージャ候補/関数ポインタ候補の収集

クロージャ候補の収集と関数ポインタ候補の収集は以下のようにして行われる。

  • トレイト制約のトレイトが Fn/FnMut/FnOnce のいずれかを調べる。どれでもなかったら何もしない。
  • Self がクロージャ型/関数定義/関数ポインタのいずれかを調べる。どれでもなかったら何もしない。未解決の型推論変数の場合は曖昧となる。
  • クロージャ型については、キャプチャー変数の利用状況を見て、 Fn/FnMut/FnOnceが実装できるかどうかを調べる。実装できなかったら何もしない。この時点でクロージャ種別が判明していない場合は曖昧となる。
  • 関数定義/関数ポインタについては、 unsafe でないこと、 extern "Rust"である(これは何も書いていないのと同義)こと、可変長引数部分をもたないこと(extern "Rust"であることからも従う)を確認する。どれか1つでも満たされていなかったら何もしない。
  • それ以外の場合は、これを候補にする。

クロージャ候補/関数ポインタ候補の承認

クロージャ候補の承認と関数ポインタ候補の収集は以下のようにして行われる。

  • クロージャ/関数ポインタ型から、それが実装するクロージャトレイト参照を生成する。 (例: [closure@..] から Fn(u8) -> u32 / fn(&String) -> &str から FnMut(&String) -> &str)
  • 生成したクロージャトレイト参照を、トレイト制約と単一化する。
  • クロージャの場合、クロージャの種別ごとに生じる制約を追加する。

Copy/Sized の収集と承認

Copy はimpl・関連型の境界・型引数の境界のほかに、以下の組込みの規則により候補が生成されることがある。

  • 整数・浮動小数点数・bool・char・関数ポインタ・関数定義・生ポインタ・共有参照・!: 無条件で Copy である。
  • 配列: 要素型が Copy であるときに Copy である。
  • タプル: 全ての要素型が Copy であるときに Copy である。
  • トレイトオブジェクト・str・スライス・クロージャ型・可変参照: Copy ではない。他の候補の有無にかかわらず、このトレイト制約は解決されない。
  • 構造体・列挙型・共用体・射影型・型引数・impl Trait型: Copy とは限らないが、impl Copy for などの候補により Copy になるかもしれない。
  • 未解決の型推論変数の場合: 曖昧となる。

Sized にも同様の組込みの規則がある。

  • 整数・浮動小数点数・bool・char・関数ポインタ・関数定義・生ポインタ・参照・配列・クロージャ型・!: 無条件で Sized である。
  • タプル: 最後の要素型が Sized であるときに Sized である。
  • トレイトオブジェクト・str・スライス: Sized ではない。他の候補の有無にかかわらず、このトレイト制約は解決されない。
  • 構造体・列挙型・共用体: 各バリアントの末尾の型が Sized であるとき、 Sized である。
  • 射影型・型引数・impl Trait型: Sized とは限らないが、T: Sized などの候補により Sized になるかもしれない。
  • 未解決の型推論変数の場合: 曖昧となる。

これらの条件が満たされたときに、 Copy/Sizedの組込みトレイト候補が生成される。候補の生成時点では、再帰的な制約は加味しない。

Copy/Sized の組込みトレイト候補の承認のタイミングで、これらの再帰的な制約がチェックされる。

Unsize の収集と承認

T: Unsize<U> は関連型の境界・型引数の境界のほかに、以下の規則により候補が生成される。

  1. T と U がどちらも同じトレイトのトレイトオブジェクト型で、追加の Send/Sync 境界について T のほうが U より多くを実装しているときは、 T: Unsize<U> の候補が生成される。
  2. T がトレイトオブジェクト型ではなく、 U がトレイトオブジェクト型のときは、 T: Unsize<U> の候補が生成される。
  3. U がトレイトオブジェクト型ではなく、 T か U が未解決の型推論変数のときは、曖昧となる。
  4. T が配列で U がスライスのときは、 T: Unsize<U> の候補が生成される。
  5. T と U がどちらも同じ構造体を指しているときは、 T: Unsize<U> の候補が生成される。
  6. T と U が同じ長さのタプルのときは、 T: Unsize<U> の候補が生成される。

これらの候補は以下の規則により承認される。

  1. T と U の主境界は等しい。 T は U より長く生存する。
  2. U のトレイトはobject-safeである。 T は U の全てのトレイトを実装している。 T は U の生存期間以上に生存する。
  4. T と U の要素型が等しい。
  5. 構造体はフィールドを1個以上持っている。最後以外のフィールド達と、最後のフィールドは、型引数を共有していない。最後以外のフィールドは T と U で等しい。最後のフィールドを T0, U0 とおくと、 T0: Unsize<U0> である。 (これらの比較時には射影型は解決せずにそのまま扱う)
  6. タプルは1要素以上である。最後以外のフォールドは T と U で等しい。最後のフィールドを T0, U0 とおくと、 T0: Unsize<U0> である。

候補の選別

選別はさらに以下の処理に分けられる。

  • 候補がちょうど1個なら、選別処理をスキップする。
  • 各候補の承認処理をして、失敗したら候補から外す。承認の成否にかかわらず、型環境は元の状態にロールバックする。
  • それでも候補が複数残っている場合は、各候補の特殊化関係を調べ、特殊化関係にあれば負けたほうを外す。

特殊化関係はcandidate_should_be_dropped_in_favor_ofにある。これは以下の規則になっている。

  • 型引数候補は最も強い。異なる型引数候補同士は比べられない。
  • 射影候補(impl Traitを含む)とトレイトオブジェクト候補(組込みトレイトオブジェクト候補を含まない)は、その次に強い。
  • それ以外の候補は上記よりも弱く、お互いには比べられない。ただし、以下の例外がある。
    • 2つの実装候補について、実装が特殊化関係にある場合は、より特殊なほうがより強い。
    • 2つの実装候補について、 #![feature(overlapping_marker_traits)] で、両方の実装がアイテムを持たず、極性も等しい場合には、同じ強さである。

同じ強さである場合も含めて、より弱いものから順番に脱落させていく。これにより最強の候補が1つだけ残ったら選別は成功となる。

トレイト選択では未解決の型推論変数が含まれていることがあるため、コヒーレンスに関係なく、複数の候補が残る場合があり、その場合はエラーになる。逆に、トレイト選択では基本的に現在見えている実装から探索するので、「これしか該当する実装がないから」という理由により型推論が進むことがある。以下はその例である。

use std::ops::Add;
fn f<T: Add<i32>>(t: T) {
    t + Default::default(); // OK
}
fn g<T: Add<i32> + Add<i8>>(t: T) {
    t + Default::default(); // Error
}
fn main() {
    
}

より奇妙な例としては、以下のようなものも考えられる。

fn f<T>() {
    let x : (_, T); // Error
}
fn g<T: ?Sized>() where (i32, T): Sized {
    let x : (_, T); // OK
}
fn main() {
    
}

収集時には曖昧でも、選別によって曖昧性がなくなる例としては、例えば以下のようなものが考えられる。

trait Foo<Y> {
    fn y() -> Y;
}
trait Bar {}
trait Baz {}

impl<T: Bar> Foo<i32> for T {
    fn y() -> i32 { 0 }
}
impl<T: Baz> Foo<i8> for T {
    fn y() -> i8 { 0 }
}

impl Bar for i32 {}
impl Baz for i64 {}

fn f() {
    let _ = <i32 as Foo<_>>::y();
}

fn main() {
}

否定実装の処理

既定実装と異なり、否定実装は収集段階では通常の実装と同様に扱われている。否定実装の特徴は、この実装が選別された場合にはコンパイルエラーとなるという点である。

自己再帰的な制約の処理

自己再帰的なデータ構造の Send の処理などで、自己再帰的な制約が出てくることがある。これは evaluate_stackの一部分で処理されている。以下のように実装されている。

  • トレイト制約の処理中は、再帰的に処理中のトレイト制約をスタックに積む。
  • 現在のトレイト制約が、再帰的に処理中のトレイト制約と等しいときは、収集処理をせずにすぐにOKを返す。

まとめ

トレイト選択の詳細について説明した。ただし、より一般の制約のfulfillmentや、coherence checkerなどについては言及していない。

Rustにおける左辺値選好と可変性調停

Rust

概要: Rustのミュータビリティー推論に使われる左辺値選好と可変性調停について説明する。

左辺値選好

Rustの型推論では、期待型のほかに、左辺値選好 (lvalue preference) という状態もトップダウンに渡される。

LvaluePreferenceは以下のどちらかの値をとる。

  • PreferMutLvalue … 可変な左辺値を優先する。
  • NoPreference … 選好はない。不変な左辺値や、右辺値などでよい。

左辺値選好はほぼ構文的に決定される。具体的には以下のように決定・伝搬される。

  • &mut の内側の式は PreferMutLvalue
  • 代入の左辺は PreferMutLvalue
  • メソッド呼び出しとフィールド参照のレシーバーは左辺値選好を継承する。
  • x[i] の左辺は左辺値選好を継承する。
  • 参照外し演算子は左辺値選好を継承する。

左辺値選好は次の用途に用いられる。

  • x[i] は原則として Index に脱糖されるが、PreferMutLvalue ならば先に IndexMut を試す。
  • *x は原則として Deref に脱糖されるが、 PreferMutLvalue ならば先に DerefMut を試す。
    • メソッド以外の自動参照外しに対しても同じ処理が行われる。
    • メソッドのレシーバの自動参照外しは NoPreference が仮定される。 (後述)

左辺値選好が誤推論するケース

さて、この左辺値選好は多くの場合に正しく可変性を推論するが、誤った推論をするケースも考えられる。以下がこの左辺値選好の仮定である。

  • x[i] の左辺は可変性を継承する→正しい。 (Index/IndexMut の型がそうなっているので)
  • *x は可変性を継承する→正しい。 (Deref/DerefMut の型がそうなっている。また、 &T/&mut T/Box<T> の参照外しの動作も同様である。)
  • フィールド参照は可変性を継承する→正しい。
  • メソッド呼び出しは可変性を継承する→正しくない。 &mut self を受け取り &T を返したり、 &self を受け取り &mut T を返したりする可能性がある。

これにより、メソッド呼び出しのレシーバの位置に Deref や Index が来ると、可変性の推論で誤推論を起こす可能性がある。これを実験すると以下のようになる。

use std::fmt::Debug;
use std::ops::{Deref, DerefMut};


// deref/deref_mut 時にメッセージを出すラッパー
#[derive(Copy, Clone, Debug)]
pub struct Wrap<X: Debug + ?Sized>(X);

impl<X: Debug + ?Sized> Deref for Wrap<X> {
    type Target = X;
    fn deref(&self) -> &Self::Target {
        println!("deref({:?})", self);
        &self.0
    }
}

impl<X: Debug + ?Sized> DerefMut for Wrap<X> {
    fn deref_mut(&mut self) -> &mut Self::Target {
        println!("deref_mut({:?})", self);
        &mut self.0
    }
}


// 左辺値選好による推論が失敗する例
#[derive(Copy, Clone, Debug)]
pub struct A;

impl A {
    pub fn f<'a, 'b>(&'a self, p: &'b mut i32) -> &'b mut i32 {
        p
    }
    pub fn g<'a, 'b>(&'a mut self, p: &'b i32) -> &'b i32 {
        p
    }
}

fn main() {
    let mut x = Wrap(A);
    let mut y : i32 = 0;
    
    // レシーバが&Tでかまわないが、構造上&mut Tが推論される例
    &mut *(*x).f(&mut y); // deref_mut(Wrap(A));
    &mut *x.f(&mut y); // deref(Wrap(A));
    // レシーバが&mut Tを必要とするが、構造上&Tが推論される例
    &*x.g(&y); // deref_mut(Wrap(A));
}

これを見ると、一番最初の例だけ、 Deref::deref でよいはずの位置で DerefMut::deref_mut が呼ばれているが、他の例では問題なく動作している。

これは次のような理由による。

  • この例には書いていないが、&T で十分だが &mut T が推論され、しかし実際には DerefMut が実装されていない場合には、 Deref にフォールバックされるため問題ない。
  • メソッドのレシーバの自動参照外しでははじめ DerefMut ではなく Deref が仮定される。
  • メソッド解決後に発生する可変性調停のため、推論と異なり &mut T が必要な場合は、そのように修正される。

可変性調停

可変性調停 (reconciliation) はメソッドの解決後に行われる処理で、レシーバが &mut self だった場合に Deref/Index を再解決する処理である。

これは次のような手順を踏む。

  • レシーバを指定している式を調べ、影響を受ける Deref/Index 呼び出しを列挙する。 (例えば x[i][j].some_method() で some_method のレシーバが &mut self の場合、 x[i] と x[i][j] を補正する必要がある。
  • それぞれの Deref/Index を PreferMutLvalue で再推論する。これによりこの部分が DerefMut/IndexMut に昇格する。

これにより、&mut T が要求される部分で &T を誤推論したことにより発生しえたエラーを回避している。

まとめ

  • *x や x[i] などではイミュータブルな Deref/Index とミュータブルな DerefMut/IndexMut のいずれかが選択される。
  • これらは色々な仕組みによりだいたいいい感じに推論される。それには以下のような動作が関わってくる。
    • 構文的に決まる「左辺値選好」をトップダウンに伝搬する。
    • DerefMut が駄目なら Deref にフォールバックする。
    • メソッド解決でははじめイミュータブルを仮定し、 &mut self が要求されていたらミュータブルとして再推論する。