OCamlの 型推論 ---- OCamlとは ---- プログラミング 言語の ひとつ ---- 型推論 とは ---- 型を推論 すること ---- 例 ---- fun a b c → c(if a then b else "あ") + 5 ---- 型は書いて ないけど ---- fun a b c → c(if a then b else "あ") + 5
: bool→string→(string→int) →int
---- コンパイラが 自動で 推論 ---- 直感的に 言うと ---- (if a then ...) ということは ---- a は bool に ---- 決定 ---- (... then b else "あ") ということは ---- b と "あ" は 同じ型 ---- つまり b は ---- string ---- c(...) + 5 intの5と 足せるのは ---- int ---- c (.."あ"..) が int だった ---- よって c は ---- stringから intへの 関数 ---- そんな感じで。 ---- 詳しい アルゴリズム ---- 1:全部の 式に とりあえず ---- 適当に 型を振る ---- aはα型 bはβ型 cはγ型 ---- c(if a then b else "あ") + 5 はδ型 ---- c(if a then b else "あ") はε型 5 はζ型 ---- if a then b else "あ" はη型 "あ" はθ型 ---- これで 全部 ---- 2: それぞれの 式
だけ
から わかること ---- 「5はζ型」 ---- 5は どう見ても intです ---- ζ = int ---- 「"あ"はθ型」 ---- "あ"は どう見ても stringです ---- 本当に ありがとう ございました ---- θ = string ---- 次は 「c(if a then b else "あ") + 5 はδ型」 に着目 ---- 足し算 である ---- OCamlには オーバーロード 無し ---- + は 常に intの足し算 ---- 「c(if a then b else "あ") + 5 はδ型」 「c(if a then b else "あ") はε型」 「5はζ型」 ---- δ = int ε = int ζ = int ---- 「c(if a then b else "あ") はε型」 に 着目 ---- 「cはγ型」 「if a then b else "あ" はη型」 「c(if a then b else "あ") はε型」 ---- γにηを適用 すると εになる ---- そういう 関数 ---- γ = η→ε ---- 「if a then b else "あ" はη型」 に 着目 ---- 「if a then b else "あ" はη型」 「aはα型」 ---- if の条件は bool に 決まってる ---- α = bool ---- 「if a then b else "あ" はη型」 「bはβ型」 ---- thenの結果と if全体の結果は 同じ型 ---- β = η ---- 「if a then b else "あ" はη型」 「"あ"はθ型」 ---- 同様に ---- θ = η ---- これで 全部 ---- 3:わかった ことを 並べる ---- ζ = int θ = string δ = int ε = int ζ = int γ = η→ε α = bool β = η θ = η ---- わかったヤツらを α=bool, δ=int ε=int, ζ=int, θ=string ---- わかってないヤツらに γ = η→ε β = η θ = η ---- 代入 ---- γ = η→
int
β = η
string
= η ---- η=string が わかった ---- 代入 ---- γ =
string
→int β =
string
---- 謎は 全て解けた ---- ζ = int θ = string δ = int ε = int γ = string→int α = bool β = string η = string ---- 型推論 完了 ---- 4: 注釈 ---- 代入してる 間に ---- int = string とか出たら ----
型エラー
---- 代入しまくっても 「わかってない ヤツら」が 消えない場合は…? ---- 5: 次回予告 ---- 「型推論と 多相型」 ---- お楽し みに
戻る
進む