簡単な型システムを実装していく１０ STLC+...+Error (1)

例外を投げるようなエラー処理のための型システムを追加していく。

今までの変更に比べて圧倒的に複雑なので複数回にわけている。

何が複雑かというと、「エラーが投げられた箇所の式の型は何か？」という問題の答えが「任意の型を取り得る」というものだからだ。

例えば

let x = if some_condition
         then 1
         else failwith "condition failed!"
let y = if some_other_condition
         then "hello"
         else failwith "some other condition failed!"

のようなOCamlコードは型検査を通るが、failwith "condition failed!"はint型として、failwith "some other condition failed!"はstring型として許容されなければ型検査が失敗するはずだ（if式の第二、第三式の型は合致する必要があるため）。

このような「なんの型とでも合致する」という型を表現する方法としては、型推論で行うように新しい型変数を振っておいて任意の型と単一化できるようにしておく（型推論に関するトピックは近いうちに書く予定）、部分型を導入して「すべての型の部分型となるBottom型」を定義して使う、といったアプローチがある。このシリーズではTaPLに準拠して後者の部分型を使ったアプローチでいく。

今回はBottom型は導入するがまったく不十分な変更しか加えられていないコードを見ていく：

gist.github.com

型

型はTBottomを追加するのみ：

type ty =
...
| TBottom

式

式としては二種類：

type exp =
...
| EError
| ETry of exp * exp

例外を投げるためのEError式と、try ... except ...に相当するETry式。後者は第一式をまず評価し、何事もなく評価が終わればその結果がETry式の結果になり、評価の途中でエラーが投げられたら第二式を評価してその結果がETry式の結果になる、というもの。

例外の種類やエラーメッセージを保持するなどの機能はない（ただしTaPLではちゃんとそういう機能についても書いてある）。

typeof式

EError式のケース：

let rec typeof env = function
...
| EError -> TBottom

これはTBottom型になる。

ETry型：

| ETry(e1, e2) ->
  let t = typeof env e1 in
  if t = typeof env e2 then t
  else failwith "type mismatch between try and except clauses"

tryで評価する式の型とexcept部分の式の型が合致しているかを調べてから、その合致している型を返す。tryの部分でintを返そうとしていたのに、エラーでexceptの方に行ってリカバリとしてboolが返ってきた、というような状況では型検査は当然失敗になる。

次回

ここまでのコードは前述のとおりまったく不十分である。なぜならエラー関連の式とBottom型を導入したはいいが、Bottom型がすべての型の部分型である、つまりTNatとTBottomを比較しても「同一型」、TBoolとTBottomを比較しても「同一型」となるといった特殊性が全然実装されていないからだ。

次回からは何回かにわけて部分型を扱えるように今まで書いてきたコードの大部分を改装していく。