近況 2023-01-31

 2023年1月31日 投稿 日記

今月の活動 (ミローネ言語など)

ミローネ言語

  • https://github.com/vain0x/milone-lang
  • 型検査が壊れていたのを直した
    • 複雑な状況になっていたが、結局は型パラメータのスコープを適切に処理すればよかった
  • 双方向型検査風味にした
    • レコード式の検査が自然になって、型エラーの位置が改善したというメリットがあった

双方向型検査

いままでは式の型をinferで計算して型の一致をみるべきときにunifyで単一化するという実装だった

infer: 式 -> 型
式の型を計算する

新たにcheck操作を加えた

check: 式 -> 型 -> unit
その式が渡した型を持つことを確かめる

check操作では式の型があらかじめ与えられるので、型によって意味が異なるような式の検査をやりやすい。 特にミローネ言語のレコード式 (withがないもの) はそれ自身ではどのレコードなのか分からないので困っていた。 いままでも後述するcheckと似たような方法でレコードの型を決めようとしていたが、それを検査の全体でやるようにした

規則

check操作は式の型の一部をその内部の式の型に伝播できるときに使う。 例えばペアの構築 (x, y) は次のようにcheck (式 ⇐ 型) を使う:

    x ⇐ 'X
    y ⇐ 'Y
    ------------------
    (x, y) ⇐ 'X * 'Y

この推論規則は次のような手続きを表していると読む:

  • ペアの構築 x, y の式をcheckするには以下を行う:
    • 対象の型がペアの型 _ * _ であることを確かめる:
      • ペアの型でなかったらエラーにする
      • 型を分解して 'X, 'Y を得る
    • 式 x の型を 'X にcheckする
    • 式 y の型を 'Y にcheckする

ミローネ言語にはメタ型がある。 対象の型がメタ型なときは ‘X, ‘Y にそれぞれフレッシュなメタ型を生成して、対象の型を 'X * 'T に束縛すれば型検査を進められる

式はcheckできるものとできないものに分類できる。 基本的に導入式 (特定の型コンストラクタの値を生み出すような式) はcheckできる。 一方、除去式 (特定の型コンストラクタの値を消費する式) はcheckしようとしても対象の型をうまく利用できない

例えば関数の適用は除去式である。 その検査ではinfer (式 ⇒ 型, 記事ではsynthと呼ばれる) を使う

    f ⇒ 'T -> 'U
    x ⇐ 'T
    -------------
    (f x) ⇒ 'U

手続き的にいえば:

  • 関数適用である式 f x の型をinferするには以下を行う:
    • f の型を infer する
    • それが関数型 _ -> _ であることを確認する
      • 関数型でなかったらエラーにする
      • 型を分解して 'T, 'U を得る
    • x の型が 'T であることを check する
    • もとの式の型は 'U である

関数適用の式の型は返り値の型であって、そこから関数や引数の型を取り出すことはできないので、checkはできない。 ただし推論規則に x ⇐ 'T とあるように関数の型が分かっていれば引数の式はcheckできる。 一例では関数の型から引数にあるレコードの型を決められるようになる (Point.area {X = 2; Y = 3}) (おそらく)

型検査の詳細な仕組みはドキュメントに起こすべきだと思ってはいるが書いていない……

メリット

利点の1つは前述のようにレコードの型を決める方法がその場しのぎだった問題が改善したこと。

また、型エラーの位置が改善する効果もあった。 いままでは単一化が起こるところで型エラーが報告されていたので粒度が粗かった。 checkによって複合的な型が分解されて部分式に下りていき、部分式で型エラーが起こるので粒度は細かくなった。 例えば以下は型エラーのテストコードからの抜粋で、タプルパターン全体ではなく、その一部であるリテラルパターンに対して型エラーが出るようになった:

// before
    match ((1, 2), 3) with
    | (1, "type error"), 3 -> ()
//          type error ^
//          (int * string) * int <> (int * int) * int

// after
    match ((1, 2), 3) with
    | (1, "type error"), 3 -> ()
//        ^ type error
//          string <> int

一方、unifyの回数を減らすとか、生成されるメタ型の個数を減らすといった効果も期待していたけど、それはあまり効果がなかった。 そもそもメタ型は注釈のない引数パターンから大量に発生していて型検査の途中に発生するものは多くないということに (測定していて) 気づいた

サブタイピングも導入したかったけど、極性の処理が必要なので先送りにした。 単一化によって型の一致 ('T = 'U) を確認するのではなく、'T <: 'U (‘T が ‘U のサブタイプであること) を確認すること。 例えば nativeptr<_> <: voidptr といったサブタイピングがあると嬉しい

参考

F# ツールのコードリーディング

関連記事