HaskellでTypeInferを作る
型を定義する
実装のASTよりはだいぶシンプルになる
code:hs
data 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)
code:hs
type TEnv = Map String Type
型検査器単体では推論はしない
Add A Bが来たときに「A,B両方がIntであるかどうか」などを判断する
If B then T else Eなら
「BはBoolで、かつTとEは同じ型かどうか」など
型推論はせず、型検査のみの実装にするためには、
コード内ですべての変数に型宣言を強制するsyntaxにする必要がある
つまりTVarという型が存在しない
型推論をする
(変数名, 型)のリスト
code:hs
type TEnv = Map String Type
AST.Var "x"の推論をする
型環境に変数名xの型が登録されているか確認
あれば、その型に紐付ける
なければエラー
このEnvの中の型変数TVar 1の具体的な型がわかったらどう更新する？
推論結果が2つ以上に当てはまる場合は、それらの結果を表す代表となる型にする
type inferの型
code:hs
type 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
code: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を求める table:問と回答
入力 環境 出力 備考
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力がつよい..!
めっちゃ参考にできそうmrsekut.icon
OCamlのtype checkerの開発者による解説 Haskellの型システムの実装
haskellで実装していく記事
taplのruby実装