UV Study 51 Rust勉強会 型システム超入門
自己紹介
型システムとは何か
コンピュータプログラムにおける構成要素、値に対して型(type)と呼ばれる特性を付与するための形式体系 プログラムを安全かつ効率的に動作させるための基本的な仕組み
整数型、文字列型、Structなどの型が適切に使われているかをチェックする
型推論
プログラマが明示的に型を指定しなくても、コンパイラやインタプリンタが自動的に型を推論する機能。
code:rust.rs
let x: i32 = 42;
let y = x + 1 // yの型はコンパイラが自動的に推論してくれる(この場合はi32)
型推論はどうやって行われているか
型環境
型環境とは、プログラム中の変数や式に対して、それぞれの型情報を保持する構造。プログラムに登場した値は全て型環境に追加して記録する。
型環境は通常、以下のような形式で表される
ø:空の型環境。初期状態で何も含まれていない状態を示します。
Γ, x : T:既存の型環境 Γ に、新しい変数 x とその型 T を追加した型環境です。
推論規則
$ \frac{仮定A}{結論B}と書かれた場合、これは、「仮定A が正しければ 結論B も正しいと証明(推論)できる」という意味になる。
また、$ \frac{A_1 A_2}{B}と書かれた場合、これは、「A1 と A2 の両方が正しければ B も正しいと証明できる」という意味になり、条件の部分には2個以上の式を書くことができる。
型付け規則
任意の式に対して型を決定するための規則。型付け規則を用いると、式の型を、数学の証明と同じく推論規則に基づく証明によって決定することができる。
型推論を実際にやってみる
code:例題.rs
let x = 42;
let y = x + 1;
上記のような指揮の型推論のプロセスを考える。
基本的な型付け規則の定義
1. 整数リテラル:
$ (\frac{}{\Gamma \vdash n : \text{int}})(nは整数)
2. 変数:
$ (\frac{x : \tau \in \Gamma}{\Gamma \vdash x : \tau})
3. 足し算:
$ (\frac{\Gamma \vdash e_1 : \text{int} \quad \Gamma \vdash e_2 : \text{int}}{\Gamma \vdash e_1 + e_2 : \text{int}})
ここで、$ \Gammaは型環境を表し、$ (\Gamma \vdash e : \tau)は型環境$ \Gammaのもとで式eが型$ \tauを持つことを示します。
実際に推論を行う(1行目)
code:例題.rs
let x = 42;
1. まず、整数リテラル42の方を推論する
1. 規則1を適用
$ (\frac{}{\Gamma \vdash 42 : \text{int}})
2. xに42を束縛
新しい型環境$ \Gamma_1 = \Gamma \cup \lbrace x:int \rbrace
実際に推論を行う(2行目)
code:例題.rs
let y = x + 1;
1. x + 1の型を推論する
変数xの型は$ \Gamma_1から取得
規則2を適応
$ (\frac{x : int \in \Gamma_1}{\Gamma_1 \vdash x : int})
2. 整数リテラル1の方を推論
規則1を適応
$ (\frac{}{\Gamma_1 \vdash 1 : \text{int}})
3. xと1の足し算x + 1の方を推論
規則3を適応
$ (\frac{\Gamma_1 \vdash x : \text{int} \quad \Gamma_1 \vdash 1 : \text{int}}{\Gamma_1 \vdash x + 1 : \text{int}})
4. yにx + 1を束縛
新しい型環境$ \Gamma_2 = \Gamma_1 \cup \lbrace y:int \rbrace
型環境の遷移
最終的な型環境は以下のようになる
1. 初期型環境$ \Gamma = \phi
2. $ \Gamma_1 = \Gamma \cup \lbrace x:int \rbrace
3. $ \Gamma_2 = \Gamma_1 \cup \lbrace y:int \rbrace = \Gamma \cup \lbrace x:int, y:int \rbrace
このようにして、推論規則と型付け規則を適応することで、プログラム内の格式に対する型を導き出すことができる。
まとめ
Rustでよく聞く型システムの一端を説明した。
IF で同じ方を返す必要がある
ぶら下がりポインタが発生しない
参考