回答編集履歴

2

サブタイピングの型推論について追記。

2018/07/15 02:05

投稿

qnighy
qnighy

スコア210

test CHANGED
@@ -110,6 +110,88 @@
110
110
 
111
111
 
112
112
 
113
+ ## 追記: サブタイプの型推論について
114
+
115
+
116
+
117
+ 「実引数が仮引数のサブタイプであるという制約を追加する。」についてより詳しく説明します。結論からいうと、これをした時点で `T` が `&mut i32` の形であること、そして**そのライフタイムがもとのライフタイムより同じか小さい**ことが確定します。
118
+
119
+
120
+
121
+ まず、Rustの型推論は単相Hindley-Milnerに基づいているので、軽く復習しておきます。[Niko Matsakis氏のブログ](http://smallcultfollowing.com/babysteps/blog/2017/03/25/unification-in-chalk-part-1/)でも使われている(比較的一般的と思われる)記法として、型変数を `?T` と表記することにします。
122
+
123
+
124
+
125
+ Hindley-Milnerでは、 `type1 == type2` という制約が追加されるごとに、現時点でわかっている最も一般的な解(most general unifier; mgu)を求めていきます。
126
+
127
+
128
+
129
+ たとえば、`?T`, `?U`, `?V` が未解決の型変数として、 `(Vec<?T>, Option<?U>) == (?U, Option<?V>)` という制約が追加されると、
130
+
131
+
132
+
133
+ - `(Vec<?T>, Option<?U>) == (?U, Option<?V>)` ⇔ `Vec<?T> == ?U` かつ `Option<?U> == Option<?V>` なのでこれらを再帰的に解く
134
+
135
+ - `Vec<?T> == ?U` なので `?U` に `Vec<?T>` を代入する
136
+
137
+ - `Option<?U> == Option<?V>` ⇔ `Option<Vec<?T>> == Option<?V>` ⇔ `Vec<?T> == ?V` なので `?V` に `Vec<?T>` を代入する
138
+
139
+
140
+
141
+ というようにして、「`?U` に `Vec<?T>` を代入し、 `?V` に `Vec<?T>` を代入する」のが最も一般的な解であることがわかります。 (`?T` の中身は依然不明なので、その後追加される制約で解決されることが期待されます。)
142
+
143
+
144
+
145
+ 最も基本的なHindley-Milnerでは以上のようにして等号を再帰的に解きます。では**Rustのサブタイピング**が入った場合のHindley-Milnerを考えてみます。
146
+
147
+
148
+
149
+ この場合、 `type1 == type2` の形の制約に加えて、 `subtype <: supertype` の形の制約を考える必要があります。しかしやることは同じで、一般性を失わないように制約を分解していけばいいことになります。
150
+
151
+
152
+
153
+ では `&'a mut i32 <: ?T` という制約の場合はどうでしょうか。まず、`&mut`は組み込みの構文が与えられていますが、型システムという観点からは `RefMut<'a, T>` のような型とみなせます。 (標準ライブラリの同名の型とは別です) つまり、 `RefMut<'a, i32> <: ?T` という制約を解くことになります。
154
+
155
+
156
+
157
+ この制約から確実にわかることはなんでしょうか。Rustのサブタイピングでは生存期間以外の構造が変わることはありません。したがって `?T` が `RefMut` であることはこの時点でわかっています。つまり、新しい生存期間変数 `'b` と型変数 `?U` を導入して
158
+
159
+
160
+
161
+ `RefMut<'a, i32> <: RefMut<'b, ?U>` かつ `RefMut<'b, ?U> == ?T`
162
+
163
+
164
+
165
+ と書けることになります。あとは `RefMut` 同士のサブタイプ制約を分解するだけです。 `RefMut<'a, T>` は `'a` に対して共変で `T` に対して非変ですから、
166
+
167
+
168
+
169
+ `RefMut<'a, i32> <: RefMut<'b, ?U>` ⇔ `'a <: 'b` かつ `i32 == ?U`
170
+
171
+
172
+
173
+ となります。 `'a <: 'b` (期間の包含でいうと `'b <= 'a`) は型推論にとってはもう分解できない制約なので(そのままborrow checkerに渡される)、これで終わりです。結局、
174
+
175
+
176
+
177
+ - 新しい変数 `'b`, `?U` を導入する
178
+
179
+ - `?T == RefMut<'a, ?U>`
180
+
181
+ - `?U == i32`
182
+
183
+ - `'a <: 'b`
184
+
185
+
186
+
187
+ とするのが、この時点で最も一般的な解ということになります。
188
+
189
+
190
+
191
+ これが、前の節の「実引数が仮引数のサブタイプであるという制約を追加する。」の中で起こっていることです。
192
+
193
+
194
+
113
195
  ## おまけ
114
196
 
115
197
 

1

驚くべきことに、リストのネストができないので苦し紛れをした

2018/07/15 02:05

投稿

qnighy
qnighy

スコア210

test CHANGED
@@ -94,9 +94,9 @@
94
94
 
95
95
  - まず、仮引数と実引数の型を比べて、条件次第で型強制を挿入する。
96
96
 
97
- - ちなみにコンパイラ内部では再借用は型強制の一種として処理されています。
97
+ - ちなみにコンパイラ内部では再借用は型強制の一種として処理されています。
98
98
 
99
- - [型強制のコード](https://github.com/rust-lang/rust/blob/1.27.1/src/librustc_typeck/check/coercion.rs#L208-L222)を見るとわかりますが、強制先の型が参照と判明しているときだけ再借用が検討されます。これが、ジェネリックパラメーターでは再借用されないとされる所以です。
99
+ - [型強制のコード](https://github.com/rust-lang/rust/blob/1.27.1/src/librustc_typeck/check/coercion.rs#L208-L222)を見るとわかりますが、強制先の型が参照と判明しているときだけ再借用が検討されます。これが、ジェネリックパラメーターでは再借用されないとされる所以です。
100
100
 
101
101
  - ↑の成否にかかわらず、実引数が仮引数の**サブタイプ**であるという制約を追加する。
102
102