HaskellでTypeInferを作る
型を定義する
実装のASTよりはだいぶシンプルになる
hsdata Type
= TInt
| TBool
| TVar Int -- 型変数：識別番号
| TLambda Type Type
deriving (Show, Eq) TVar は、「未知の型を一時的に入れておくための型」包含はするが「
AST.Var の型」という意味ではない型推論しないなら不要
型変数の型
TVar ここ はユニークなidを振っている未確定な型を識別する
TLambda Type Type は高階関数の許容を表現している TLambda A B の場合は A -> B という型を表している (A -> B)-> C などの入れ子も表現できるように Constriant を取って再帰になっている今はまだないが型を引数にとって型を作る型コンストラクタも出てくる
これとか参考になりそう
Array型とか
型検査を行う
「型推論」より簡単な、単なる「型検査」について
型環境を持つ
コード内に出てくる「変数」が「何の型」を持つかを記憶する
なので、変数を使っていないコードの場合は不要
(変数名, 型) のリストex.
hoge = "Hoge" みたいな変数があれば ("hoge", String) hstype TEnv = Map String Type型検査器単体では推論はしない
Add A B が来たときに「 A , B 両方が Int であるかどうか」などを判断する If B then T else E なら「
B は Bool で、かつ T と E は同じ型かどうか」など型推論はせず、型検査のみの実装にするためには、
コード内ですべての変数に型宣言を強制するsyntaxにする必要がある
つまり
TVar という型が存在しない型推論をする
型検査のときと同様に型環境を持ち回る
(変数名, 型) のリストhstype TEnv = Map String Type AST.Var "x" の推論をする型環境に変数名
x の型が登録されているか確認あれば、その型に紐付ける
なければエラー
このEnvの中の型変数
TVar 1 の具体的な型がわかったらどう更新する？推論結果が2つ以上に当てはまる場合は、それらの結果を表す代表となる型にする
type inferの型
hstype TEnv = Map String Type
type TVarInfo = (Int, Map Int Type)
data TypeState = TypeState {
tenv_ :: TEnv,
tvarInfo_ :: TVarInfo
}
newtype TI a = TI (StateT TypeState Identity a)型環境
TEnv type TEnv = Map String Type (変数名, 型) のリストASTの変数がそれぞれ何の型なのかをリストにする
中身の例
("x", TInt) 変数
x は TInt 型である ("hoge", TVar 2) 変数
hoge の具体型はまだ定まっておらずとりあえず型変数 TVar 2 型である型変数情報
tvarInfo_ type TVarInfo = (Int, Map Int Type) (Int, Map Int Type) Int の方は、次の TVar の id を表す TVar は TVar 1 、 TVar 2 のように、ユニークな型変数を表すので、次に TVar を作成するときの id を保持している Map Int Type の方は型変数
TVar がそれぞれ何の型なのかのリストするex.
[(TVar 1, TInt), (TVar 2, TBool), (TVar 3, TBool)] id をここで持つの微妙では？Varを見るときに新しい型変数が必要になるが
このときはEnvしか更新しないのにも関わらず
idを知る必要があるためtypeListを参照する必要がある
そうなのであればidを個別でstateで持ったほうが良いのでは
関数適用を推論する
App String Exp hs-- ノリ。後で修正
doInfer (AST.App f x) = do
tf <- doInfer f -- tf :: TLambda TInt TBool
tx <- doInfer x -- tx :: TInt
tr <- -- result
unify (TLambda tx tr) tf
return tr最初に
f を推論すると関数型 t1 -> t2 が判明する t1 , t2 は TInt など具体的な型次の
x の型 tx は、 t1 == tx となっていないといけない doInfer (AST.App f x) が返す型は、 x を f に適用した f x の型であるこれを
tr とする t2 == tr になっているはずであるなので、
tf: t1 -> t2 は、 tx -> tr と全く等しいことが求められるよって単一化で、
unify (TLambda tx tr) tf を求める問と回答
| 入力 | 環境 | 出力 | 備考 |
| Nat 2 | TInt | ||
| Bool True | TBool | ||
| Var "x" | ("x", TBool) | TBool | |
| Lambda "x" (Add (Var "x") (Nat 1)) | ("x", TInt) | TLambda TInt TInt | |
| Lambda "x" (Nat 1) | TLambda (TVar 0) TInt | aは任意 |
型剣先と型推論器は別個に作るものなのかまとめて作るものなのか
referってなに
参考
詳しい。一番わかりやすい。最初に読めばよかった
重すぎない
型推論器を俯瞰する。理論にはほぼ触れなく、実装ベース
Haskellで簡単な推論機を実装する
理論も軽く触れる
Haskell力がつよい..!
めっちゃ参考にできそう
OCamlのtype checkerの開発者による解説
Haskellの型システムの実装
haskellで実装していく記事
taplのruby実装
TaPL 22章
CoPL 10章