双方向型検査パズル

 (haskellforall.com)
1 ポイント 投稿者 GN⁺ 1 시간 전 | 1件のコメント | WhatsAppで共有
  • Grace の 双方向型検査 実装では、リスト先頭要素の型をリスト全体の要素型のように扱っていたため、port: 8080 フィールドが削除され、誤った評価結果になっていた
  • 問題の例は、{ domain: "google.com" } と { domain: "localhost", port: 8080 } のリストを走査し、デフォルトポート 443 を使うコードで、期待値 [ "google.com:443", "localhost:8080" ] の代わりに [ "google.com:443", "localhost:443" ] を返していた
  • 既存のリスト推論は最初の要素から List { domain: Text } を推論し、その後ほかの要素をその型に合わせて検査していたため、エラボレーション(elaboration) の過程で上位型にない port フィールドが削除されていた
  • 修正後の実装では、各要素の型をすべて推論してから 最も具体的な上位型 を計算し、各要素をその型に合わせて再検査して、欠けている Optional 値を null または some で埋める
  • 修正後、元のリストは List { domain: Text, port: Optional Natural } と推論され、最初のレコードの port は null、2 番目の port: 8080 は some 8080 として保持され、期待どおりの結果を返す

Grace のリスト型推論バグ

  • Grace は Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism に基づく 双方向型検査 システムを使っており、このアプローチの限界を回避する実装が積み重なった結果、奇妙なバグにつながっていた
  • 問題となったプログラムは、authorities リストを走査しながら各レコードの domain と port を束縛し、port がなければ 443 をデフォルト値として使うリスト内包表記だった
let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for { domain, port = 443 } of authorities

in  "${domain}:${show port}"
  • 期待される結果は [ "google.com:443", "localhost:8080" ] だったが、バグのあるバージョンは [ "google.com:443", "localhost:443" ] を返し、2 番目のレコードの port: 8080 フィールドを完全に無視していた
  • 問題は評価器ではなく 型検査器 で発生しており、リスト型推論と型検査中に行われるエラボレーションが組み合わさって影響していた

双方向型検査と従来のリスト推論方式の限界

  • Grace が authorities リストに対して期待していた型は次のとおりだった
List { domain: Text, port: Optional Natural }
  • この型は、各レコードが必須の domain: Text フィールドを持ち、port: Optional Natural フィールドはあってもなくてもよいことを意味する
  • 実際の従来実装は、次のようにもっと狭い型を推論していた
>>> :type [ { "domain": "google.com" }, { "domain": "localhost", "port": 8080 } ]
List { domain: Text }
  • 双方向型検査 は基本的に次の 2 つの作業に分かれる
    • 式の型を推論する
    • 式が期待される型に合っているかを検査する
  • この 2 つの作業だけでは、リスト内の複数要素の型を組み合わせて、リスト全体の要素の上位型を容易に作ることができない
  • 従来の Grace 実装では、リスト型を次の方法で推論していた
    • リスト最初の要素の型を推論する
    • 残りのすべての要素が、最初の要素から推論した型に合っているかを検査する
  • 最初の要素 { domain: "google.com" } の型が { domain: Text } なので、リスト全体の要素型も { domain: Text } になっていた
  • 別の型を望むなら明示的な型注釈を追加する必要があったが、Grace が扱おうとしている現実の JSON はスキーマが大きく複雑になり得るため、巨大な型注釈としてスキーマ全体を書かせたくはなかった

エラボレーションが評価結果まで変えてしまった理由

  • Grace の型検査器は型エラーを見つけるだけでなく、型検査の過程で式を調整する エラボレーション(elaboration) も行う
  • 下位型を上位型に合わせて検査するとき、両者の型が違えば、型検査器は明示的な強制変換(coercion)を挿入する
  • Grace の評価器は内部的に、すべての Optional 値を null または some x というタグ付きの値として表現する
  • Optional が期待される位置にタグなしの値を置くと、Grace は自動的に some タグを挿入する
>>> [ some 1, 2 ]  # This would be a type mismatch without elaboration
[ some 1, some 2 ]
  • 最初の要素の型が Optional Natural と推論され、2 番目の要素がタグなしの Natural なら、型検査器は型不一致エラーの代わりに some タグを挿入する
  • レコードでも同じことが起き、Grace は レコード部分型 をサポートし、上位型に合うようレコードを強制変換する
>>> { x: 1, y: true }: { x: Natural }
{ "x": 1 }
  • より小さいレコード型でレコードに注釈を付けると、型検査器はそれを許可しつつ、上位型にないフィールドを削除する
  • authorities リストをそのまま評価しただけでも、従来実装では次のように port フィールドが削除されていた
>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com" }, { "domain": "localhost" } ]
  • この結果は次の流れで発生する
    • 最初の要素の型が { domain: Text } と推論される
    • 2 番目の要素がその期待型に合わせて検査される
    • 2 番目の要素はその型に適合するが、追加フィールド port を持っている
    • 型検査器が期待型に合わせるため port フィールドを削除する
  • レコード強制変換そのものが根本原因ではなく、実際の原因は、リスト型推論で最初の要素の型をリスト全体の型のように扱っていた方式にあった

解決策: 最も具体的な上位型の計算

  • Grace は リスト全体の型を正しく推論するための新しい演算 を追加した
  • この新しい演算は、2 つの型の 最も具体的な上位型(most-specific supertype)、つまり最小上界(least upper bound)を計算する
  • C が A と B の上位型であるとは、C が A の上位型であり、かつ B の上位型でもあることを意味する
  • C が A と B の最も具体的な上位型であるとは、C が A と B のほかのあらゆる上位型の下位型であることを意味する
  • この新しい演算を使ったリスト型推論は、次の手順に変わった
    • リスト内の各要素の型を推論する
    • すべての要素型の最も具体的な上位型を計算する
    • 各要素がその最も具体的な上位型に合うかを検査する
    • その最も具体的な上位型を、リスト全体の要素型として返す
  • この方式により、次のリストは正しい型を推論する
>>> :type [ { x: 1 }, { y: true } ]
List { x: Optional Natural, y: Optional Bool }
  • 内部の流れは次のとおり
    • { x: 1 } は { x: Natural } 型と推論される
    • { y: true } は { y: Bool } 型と推論される
    • 2 つの型の最も具体的な上位型は { x: Optional Natural, y: Optional Bool } になる
    • 各要素がその上位型に合わせて検査される
  • 各要素をもう一度上位型に合わせて検査する理由は、欠けている some や null を補うなど、正しいエラボレーションを適用するためである
>>> [ { x: 1 }, { y: true } ]
[ { "x": some 1, "y": null }, { "y": some true, "x": null } ]

修正後の authorities の型と評価結果

  • 型検査の修正後、元の authorities リストは期待どおりの型を推論する
>>> :type [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
List { domain: Text, port: Optional Natural }
  • エラボレーション後の評価結果でも port は選択的フィールドとして保持される
>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com", "port": null }
, { "domain": "localhost", "port": some 8080 }
]
  • 最初のレコードにない port は null で埋められ、2 番目のレコードの port: 8080 は some 8080 として保持される
  • 元のリスト内包表記の例も、期待どおりの結果を返す
[ "google.com:443", "localhost:8080" ]

JSON サポートと実装複雑性の選択

  • Grace が双方向型検査を強く推し進める理由は、この方式が複雑であっても、現実の JSON 型を推論できるだけの十分に強力な型検査フレームワークだと考えているからである
  • Hindley-Milner 推論やそれに近い、より単純な型検査フレームワークでは、実際の JSON データに見られる形を扱うのが難しい
  • Grace は JSON 作業専用のエルゴノミックな言語として作られたわけではないが、JSON サポートを無視しているわけでもない
  • Dhall での経験を通じて、ユーザーが使いやすい JSON 相互運用性に敏感であることを踏まえ、Grace の構文と型システムは、実装複雑性が増しても JSON 互換性を考慮するよう設計されている

参考になる関連資料

  • Datatype unification using Monoids: Grace で最も具体的な上位型を計算するときに使うアルゴリズムと本質的に同じ、単純データ型推論アルゴリズムを扱っている
  • The appeal of bidirectional typechecking: 何らかの形で部分型を使う言語を実装しようとするなら、双方向型検査を学ぶ価値がある理由を扱っている
  • Local Type Inference: 双方向型検査の先駆的な論文の 1 つであり、最小上界や内部言語への式のエラボレーションといった技法の出典として挙げられている

付録: レコード強制変換が必要な理由

  • 次の Grace 式は、レコード強制変換が必要な理由を示す例である
let f (input: { }) = input.x

in  f { x: 1 }
  • この式が型検査される場合、f の戻り値型を何にすべきかが問題になる
  • 戻り値型は Natural であってはならない
let f (record: { }): Natural = record.x  # WRONG: type error

in  f { x: 1 }
  • f は空レコード { } 型の input を受け取るので、そのレコードから Natural 値を取り出すことはできない
  • 呼び出し時にたまたま x フィールドを持つレコードを渡したとしても、関数 f は { } 型のどんな入力に対しても動作しなければならない
  • 型検査器が、宣言された入力型に存在しないフィールドへのアクセスを拒否するのも健全な選択だが、そうすると実際の JSON データを扱うのに必要な機能を失ってしまう
  • 元の authorities の例は、次の式の構文糖と本質的に同じである
let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for authority of authorities

let default = fold{ some port: port, null: 443 }

in  "${authority.domain}:${show (default authority.port)}"
  • 欠けているフィールドへのアクセスを拒否すると、存在しないかもしれないフィールドを束縛したり、デフォルト値で処理したりできない
  • 現実の JSON データをうまく扱うための設計上の選択は次のとおりである
    • フィールドが存在しなければ null を返す
    • アクセスの型を forall (a: Type) . Optional a とする
  • この型は null しか取れない型である
  • この方式を採るなら、上位型にないフィールドはレコードから必ず削除しなければならない
  • 追加フィールドを削除しないと、次の例は 1 : forall (a: Type) . Optional a を返すことになってしまう
let f (input: { }) = input.x

in  f { x: 1 }
  • これは null しか持てないはずの型に 1 が入る、不正な型の式になる
  • そのような不正な式は評価器を壊す可能性もある
let f (input: { }) = input.x  # Inferred type: forall (a: Type). Optional a

let default (input: Optional Text) = fold{ some text: text, "" }

in  "${default (f { x: 1 })}!"  # Runtime error if `f` returns `1`
  • 実際の JSON データを扱う Grace では、レコードを上位型に合わせて明示的に強制変換するのは合理的な挙動であり、実際のバグは強制変換ではなく、List 型推論のための従来の暫定的な回避策にあった

関連記事

1件のコメント

 
GN⁺ 1 시간 전
Lobste.rs の意見

  • Complete And Easy 論文を実際に動作する形にしたのは称賛に値する。双方向型検査の貪欲な性質が微妙な問題を生みうることの良い例でもある。
    非難ではなく、推論には常に問題があり、結局はどの問題を受け入れるかを選ぶことに近い。なので個人的には、サブタイピングと型強制変換はたいていアンチパターンに近いと考えている。
    データを型の真実の供給源にすると、そのデータが間違っているかどうかを検査しにくくなり、例のように有用なエラーの代わりに誤った型を得ることになる。ただ、Dhall の作者ならこのあたりは私よりはるかによく分かっているはず。複数のデータを受け取ってスキーマを生成するという発想自体は研究の価値があるが、型はふつう記述的というより規範的だと見なされる点を考えると、これを「型検査」と呼ぶかどうかはよく分からない。

  • なぜ単に f を拒否しないのか、いまひとつ理解できない。そのフィールドを絶対に持ちえない型のレコードでフィールドにアクセスしているのだから、ほぼ確実にプログラムのバグであり、型検査器が知らせるべき状況に見える。
    authority の例との違いは、port の型が欠けているのではなく Optional だという点にある。欠けたフィールドを拒否するからといって、選択フィールドまで拒否しなければならないわけではない。すでに型に基づいて値を強制変換しているのなら、{ domain: "google.com" } も { domain: "google.com", port: null } という値に強制変換できる。

    • 短く言えば、f をあえて拒否する必要はなく、それは不要な制限だ。誤ったフィールドアクセスが null : forall (a : Type) . Optional a を返す方が、誤ったフィールドアクセスを拒否する方より厳密に優れていると思う。
      より多くの有効なプログラムを許容でき、型付けが誤ったプログラムは依然として失敗する。たとえば、アクセスした値を null 処理なしで使おうとするプログラムには、そのまま型エラーが残る。

  • 真っ先に思い浮かぶのは、行型(row types) がこれを解決するのではないかということ。すでに検討済みだとは思う。ここでは行型がサブタイピングと相互作用して破綻するのだろうか?

    • Grace には行型と行多相がある。Grace では行を "fields" と呼んでいるが、それ以外はまったく同じだ。
      実際、最も具体的な上位型アルゴリズムも行型を考慮している。
      たとえば次のように書くと: 
      \\record0 record1 ->

let _ = record0.x

let _ = record1.y

in  [ record0, record1 ]
      Grace はこの式に対して次の型を推論する: 
      forall (a : Type) .  
forall (b : Type) .  
forall (c : Fields) .  
  { x: b, y: a, c } -> { y: a, x: b, c } -> List { x: b, y: a, c }

  • これは Bidirectional Typing 論文の 5.1.1 節で述べられている貪欲なインスタンス化問題の例ではないか?
    「元の設定では、この貪欲な方法が引数順序に弱いという点はかなり不運だった。しかし、他の形のサブタイピングがない述語的高ランク多相の設定では、うまく機能しうる。『tabby-first problem』は起こりえない。型が厳密により小さくなる唯一の方法は、厳密により多相的になることだけであり、最初の引数が多相的なら 𝛼 を多相型でインスタンス化しなければならず、それは述語性に違反するからだ」