Qiita Teams that are logged in
You are not logged in to any team

Log in to Qiita Team
Community
OrganizationAdvent CalendarQiitadon (β)
Service
Qiita JobsQiita ZineQiita Blog
0
Help us understand the problem. What is going on with this article?
@h_sakurai

型推論器を作る(3) 単相の型推論②出現チェック

More than 5 years have passed since last update.

前回のunifyでは、型のコピーを取りました。その型のコピーがもしも、自分自身の型だったら、型が循環して場合に寄ってはコンパイラが止まらなくなってしまうかもしれません。
そこで、型をコピーする前に型が自分の中に含まれていないかをチェックします。
それが、occurs checkです。

  let rec occurs (tvr: tv ref) (t:t):unit =
    match t with
    | TVar tvr' when tvr == tvr' -> failwith "occurs check"
    | TVar({contents = Link t}) -> occurs tvr t
    | TArrow(t1,t2) -> occurs tvr t1; occurs tvr t2
    | _ -> () 

実装は上記のように簡単です。型tの中身が型変数でかつ自分自身なら例外を投げます。
Linkならその中身をチェックし直します。
関数の型なら再帰的にチェックします。

この作成した出現チェック関数をunifyに組み込めば、出現チェックがうまく動作するようになります。

    | (TVar({contents=Unbound _} as tv), t)
    | (t, TVar({contents=Unbound _} as tv)) ->
      occurs tv t';
      tv := Link t
0
Help us understand the problem. What is going on with this article?
Why not register and get more from Qiita?
  1. We will deliver articles that match you
    By following users and tags, you can catch up information on technical fields that you are interested in as a whole
  2. you can read useful information later efficiently
    By "stocking" the articles you like, you can search right away

Comments

No comments
Sign up for free and join this conversation.
Sign Up
If you already have a Qiita account Login
0
Help us understand the problem. What is going on with this article?