3 ポイント 投稿者 GN⁺ 2024-07-23 | 1件のコメント | WhatsAppで共有
  • 型駆動設計では、入力を確認して捨てる検証よりも、確認結果をより精密な型として残すパースのほうが、その後のコードの安全性を高める
  • head :: [a] -> aのように一部の入力で失敗する関数は、戻り値の型を弱めることもできるが、呼び出し側が不要な失敗分岐を抱え続けることになる
  • NonEmpty aは空でないリストという状態を型に保持し、重複した検査や「絶対に起きないはず」のエラー処理を減らせる
  • 処理コードのあちこちに一時的な検証を混ぜるとshotgun parsingになり、一部の状態変更の後になって初めて入力エラーを発見する可能性がある
  • 実務では、関数シグネチャに望ましいデータ表現をまず載せ、Map、抽象型、スマートコンストラクタなどによって不変条件を型の境界へ押し上げるべきである

型駆動設計の出発点

  • 「Parse, don’t validate」は、型駆動設計を3語に圧縮した言い回しである
  • 静的型システムは、「この関数を書けるか」という問いをコードを書く前に表面化させてくれる
  • Haskellの例では、foo :: Integer -> VoidVoidに値が存在しないため、実際の値を作ることができない
  • head :: [a] -> aも空リスト[]が渡されうるため、すべての入力に対して定義されていない
    • GHCはパターンマッチが[]を処理していないと警告する
    • 取りうるすべての入力に対して定義されていない部分関数である

部分関数を全域関数に変える2つの方法

  • 戻り値の型を弱める

    • head :: [a] -> Maybe aに変えると、空リストではNothingを返せるため全域関数になる
    • 実装は簡単になるが、呼び出し側は常にNothingの可能性を処理しなければならない
    • CONFIG_DIRS環境変数を読み取り、リストが空でないことをすでに確認した後でも、mainheadの結果に対するNothing分岐を再び処理しなければならない例が示される
    • 重複した検査はコードを煩雑にし、複雑なケースでは性能コストとしても積み重なることがある
    • 前段の検査が削除されても、後段の「絶対に起きないはず」のエラーは型に表れない
    • 結局、型システムに穴が生じ、バグ発見をテストや手動レビューに頼ることになる
  • 引数の型を強める

    • 戻り値の型を弱めずに引数の型を強めれば、headが空リストに対して呼ばれる可能性を排除できる
    • Data.List.NonEmptyNonEmpty aは空でないリストを表す
    • 定義はdata NonEmpty a = a :| [a]
    • 先頭要素aと残りのリスト[a]を分けることで、末尾が空でも先頭要素は常に存在する
    • head :: NonEmpty a -> aは1つのパターンで実装でき、全域関数になる
    • getConfigurationDirectories :: IO (NonEmpty FilePath)のように戻り値の型を変えると、空でないという事実が型に保持される
    • nonEmpty :: [a] -> Maybe (NonEmpty a)は通常のリストをNonEmptyに変換する
    • Nothingの処理は入力境界で1回だけ行われる
    • mainではinitializeCache (head configDirs)のように、重複した分岐なしで使える
    • その後getConfigurationDirectoriesが空でないことを保証しないように変更されれば、戻り値の型も変わる必要があり、mainは型検査に失敗する

検証とパースの違い

  • validateNonEmpty :: [a] -> IO ()parseNonEmpty :: [a] -> IO (NonEmpty a)は、どちらも空リストを確認し、失敗時にはエラーを出す
  • 違いは戻り値の型にある
    • validateNonEmptyは情報を持たない()を返し、検査結果を捨ててしまう
    • parseNonEmptyNonEmpty aを返し、検査で得た知識を型システムに残す
  • パーサは、あまり構造化されていない入力を受け取り、より構造化された出力を作る関数とみなせる
  • この定義では、parseNonEmptyはリストを空でないリストへパースする単純なパーサである
  • パースは、プログラムと外部世界の境界で検査を先に終わらせ、その後に同じ検査を繰り返さないようにしてくれる

Haskellエコシステムにおけるパース境界

  • Haskellアプリケーションは、外部世界と接する地点でさまざまな種類のパーサを使う
    • aeson: JSONデータをドメイン型にパースするParser型を提供
    • optparse-applicative: コマンドライン引数のパーサコンビネータを提供
    • persistent, postgresql-simple: 外部データストアの値をパースする仕組みを提供
    • servant: パス要素、クエリパラメータ、HTTPヘッダーなどからHaskellのデータ型をパースする
  • 外部世界は積型や和型ではなくバイト列で語るため、パースは避けられない
  • データを使う前に前段でパースしておけば、さまざまな種類のバグを避けられ、その一部はセキュリティ脆弱性につながる可能性もある
  • すべてを前でパースしようとすると、実際に使うよりもずっと早い時点で値をパースしなければならないことがある
  • 静的型システムでは、パースロジックと処理ロジックが食い違うとプログラムはコンパイルできない

検証中心アプローチの危険

  • その場しのぎの検証は、language-theoretic security分野でいうshotgun parsingにつながりうる
  • 2016年の論文 The Seven Turrets of Babel: A Taxonomy of LangSec Errors and How to Expunge Themでは、shotgun parsingはパースと入力検証のコードが処理コードに混ざって散在するアンチパターンとされる
  • 入力を最初にすべてパースしないと、プログラムは有効な一部の入力を処理した後で、別の部分のエラーを遅れて発見することがある
    • この場合、すでに実行した状態変更を巻き戻さなければならない
    • RDBMSトランザクションのようにロールバック可能な場合もあるが、一般には常に可能とは限らない
  • 検証ベースのアプローチは、すべての検証が本当に前段で終わっているかを確認することを難しく、あるいは不可能にしてしまう
  • パースはプログラムをパース段階実行段階に分け、不正な入力による失敗を最初の段階に限定する

実務で適用する方法

  • 関数が望むデータ表現をまず型シグネチャに書き、現在与えられている表現との差を埋める形で設計する
  • 重複キーを許してはいけない[(k, v)]リストを受け取る関数なら、別途checkNoDuplicateKeys :: ... => [(k, v)] -> m ()のような検査は簡単に抜け落ちる
  • よりよい方法は、重複キーを構造的に許さないMapを関数引数に取ることである
    • 呼び出し箇所は型検査に失敗する可能性がある
    • 呼び出しチェーンに沿って、リストをMapへ変換する作業を上流へ押し上げていく
    • 値が生成される場所、または重複が実際に許容されるべき場所に到達したら、[(k, v)] -> m (Map k v)という形の検査を入れる
  • このとき、検査の結果は後続の実行に必要なので、検査を省略することはできない
  • 2つの原則が繰り返し現れる
    • 不可能な状態を表現できないようにするデータ構造を使う
    • 証明の負担はできる限り上流へ押し上げるが、必要な地点よりさらに遠くへ無理に押しやらない

追加の設計指針と限界

  • データ型にコードを導かせ、現在書いている関数のためだけにレコードへ安易にBoolを入れたくなる誘惑を避ける
  • m ()を返す関数は疑って見る必要がある
    • 命令的な効果だけを行い、意味のある結果がないときには必要な場合もある
    • 主目的がエラーを投げることなら、よりよい方法がある可能性が高い
  • データを複数回に分けてパースすることを恐れる必要はない
    • shotgun parsingを避けるとは、完全にパースし終える前に入力データに基づいて行動してはいけない、という意味である
    • 一部の入力を使って、別の入力をどうパースするかを決めることは可能である
  • 非正規化されたデータ表現は、とくに変更可能な場合には避けるべきである
    • 同じデータを複数箇所に複製すると、相互に食い違った状態が容易に表現されてしまう
    • 非正規化がどうしても必要なら、抽象化境界の背後に隠し、小さな信頼できるモジュールだけが同期の責任を持つようにするべきである
  • Haskellの道具だけではある不変条件を本当に表現しにくい場合、抽象newtypeとスマートコンストラクタを使ってバリデータをパーサのようにできる
  • すべてのerror "impossible"をなくすためにsingletonsを導入し、アプリケーション全体をリファクタリングする必要はないが、そのようなケースでは不変条件をコメントとして残すなど、慎重に扱うべきである

さらに読むための資料と現実的な注意点

  • Haskellの型システムをうまく活用するのに、PhDや最新のGHC言語拡張が必須というわけではない
  • 出発点は「全域関数を書け」という単純な原則に近いが、実際のコードへ適用する過程は簡単ではないこともある
  • Haskellコミュニティは小さいため、設計パターンや技法が文書よりも口伝の知識として残っていることがある
  • 関連資料として、Matt ParsonのType Safety Back and Forthがある
  • より高度な話題として、Matt Noonanの2018年論文 Ghosts of Departed Proofs は、より複雑な不変条件を型システムに載せる技法を扱っている
  • 実際のプログラムでは、特定の不変条件を型システムに載せるのが難しいこともあり、これらの原則は厳密な要件というより目指すべき理想に近い

1件のコメント

 
GN⁺ 2024-07-23
Hacker News の意見
  • とても良い助言で、優れた記事。このサイトで時々再掲されるのには理由がある。
    静的型付けの関数型言語を使っていない人にとっても、このアイデアはパラダイムを超えている。80〜90年代のオブジェクト指向の文献、たとえば契約による設計(Design by Contract)でも非常によく似た概念が見られるし、さらにさかのぼった論文・議論・仕様も見つかるはず。
    TypeScript も実行時に型を絞り込んでいく形でよく書かれていると思う。契約による設計は、動的言語である Clojure の spec にも影響を与えたのではないか。
    根本的には仮定と保証の問題。ある仮定を確認して保証を作れるなら、プログラムの別の部分が同じ仮定を再確認する必要はなくなる。
    コードを読んでいて、すでに保証された性質を別の場所でまた検査しているのを見るのが一番混乱する。推論や改善が難しくなる。

    • その「すでに保証された性質」は、ある時点で消えうる。より正確には、その保証を実装して実行する手続きが、何らかの理由でもはや役割を果たさなくなることがある。
      統計的にはそういうことはいずれ起こり、そのとき「本来の」検証手続きに依存していた別のプロセス・スクリプト・コードは非常に困ることになる。
    • 強い型システムを持つ言語では、プログラムが大きく複雑になるほど、これは最終的に自由を与えてくれる実用上の利点の一つになる。
      ただし実際に使わなければならない。たとえば UncheckedEmailValidEmailVerifiedEmail クラスを用意し、ある段階から次の段階へ移るには必ずメール検証プロセスを通るようにする、といった具合。
      そうすれば、メールアドレスが未確認なのか、形式上有効なのか、検証済みなのかを推測する必要がなく、更新や確認を忘れうる is_email_verified のようなブール値も不要になる。間違った場所に間違った値を使えば型チェッカーが警告してくれ、人間は重要なことに集中できる。
    • 以前の記事のコメントをざっと見てみると、この記事の最大の問題の一つはタイトルのように思える。タイトルが錨のように作用して、本文にはなく、タイトルだけが文脈なしに示唆している内容に反論する人が多くなる。
      そのため、著者が検証をまったくせずパースだけをしようと言っているように受け取るケースがあるが、実際の記事はデータをどこで検証し、その結果として何をするかについてのもの。すべての検証をなくそうという記事ではない。
  • 2019年の記事だが、今でもかなり良い助言。このパターンは現代の C# にもとてもよく合い、明示的な変数宣言を省けるのでスペースも節約できる。
    if(!Whatever.TryParse(input, out var output)) output = some-sane-default;
    または
    if(!Whatever.TryParse(input, out var output)) throw new ApplicationException($"Not a valid Thingy: {input}");
    プロのコツ:後者はカーネルモードドライバーではやらないこと。

    • プロのコツ:どちらもやらないこと。特に1つ目は絶対にやらないこと。
      正しいと思っていた値が間違っていたときに代わりに使われる暗黙のデフォルト値より、明示的な処理のほうが常に良い。
      やるべきことは、初期段階で手を挙げてパース失敗として扱い、そのうえで読み込めないファイルを扱う手順とプロトコルを非常に明確に定義すること。そうすれば、上の2つの選択肢では扱っていない難しい問いを自分たちに投げかけることになる。
      最近の CrowdStrike のカーネルモードドライバーが何らかの def/config ファイルのパースに失敗した本当の問題は、開発者・プロダクト責任者・ビジネスアナリストが「無効なファイルを読み込もうとしたらどうなるのか?」と問わなかったことにある。
    • 「かなり良い」程度である理由は何か? そして記事が公開された年とどう関係するのか? 2019年よりもっと早く公開されていたら、この記事の助言にはより権威があったという意味なのか?
    • 1つ目の方式はやめてほしい。悪いケースを処理すべきだ。「妥当なデフォルト値」に戻す処理はごくまれであるべき。
      明示的な処理 > 暗黙的な処理
    • if(!Whatever.TryParse(input, out var output)) output = some-sane-default;
      この方式は本当に嫌い。無効な入力エラーはパース関数の外で処理すべきだと思う。F# ではそれが簡単。
      type Whatever =
      static member create input =
      match input with
      | ValidWhatever x -> Some x
      | _ -> None
      match Whatever.create input with
      | Some x -> // パースされたデータを処理
      | None -> // 正しくパースされなかった場合を処理
      あるいは Option.map/Option.bind で連鎖処理を扱うパイプラインをより楽に作ることもできる。
      こうすれば、入力をパースする create メソッドを通してだけインスタンスを作れる。
      ただ実際には option より result を使いたくなる可能性が高いが、それは本筋ではない。
    • if(!Whatever.TryParse(input, out var output)) output = some-sane-default; のようなコードを見たい状況はほとんど、たぶんまったく思い浮かばない。
      入力がそもそも提供されていない場合、つまりパラメータが任意なら、妥当なデフォルト値を使うのは筋が通る。
      しかし間違った入力が提供されたのに、何の問題もないふりはしないでほしい。
      誰かが花屋に入ってきてコーヒーを頼んだとき、正しい答えはバラを渡すことではない。その人がそれを飲もうとしたら、口がずたずたに裂けてしまうだろう。
      その入力集合に対して、メソッド・モジュール・プログラムは定義された出力を持っていない。黙って間違ったことや不明確なことをしてプログラムをあっという間に推論不能にするより、その事実をはっきり示すべきだ。数か月後に異常動作のバグとして捕まるままにせず、問題を明確に発生させ、問題箇所へ直結するスタックトレースを残すほうが自分のためにもなる。
  • 強い型システムを活用して、エラー状態を表現不可能にするべきだという助言。ソフトウェア全体でバグを減らすのに非常に有効
    問題をより深く考え、このような設計をするには時間が余計にかかるが、多くの場合その時間には十分な価値がある

    • 代数的データ型をサポートする言語なら、このやり方は時間が余計にかからないとあえて言いたい。単に自然とそうなる
      もちろん C++、Java、C#、Python、Go、JavaScript のように、データをモデル化するのに意識的な手順が多く必要な言語なら時間は余計にかかる
  • 「これで、型駆動設計が自分にとって何を意味するのかを表す短く強い標語ができた。さらに良いのは、それがたった3語だという点だ: Parse, don’t validate。」
    私の標語はむしろ、常に単一のコンストラクタでだけ検証せよに近い。コンストラクタ関数でも構わない
    そうすれば無効なオブジェクトはそもそも存在できず、常に単一の真実の供給源ができる。オブジェクトを変更したいなら、同じコンストラクタを再度呼び出して新しい状態を作る方式で実装すればよい

    • 同じ話ではない
      核心は、検証するだけではその情報が後で消えてしまうことにある
      例えば、ある int が正の数かどうかを検証するだけでは利点は限られる。その値を正の整数としてパースしなければ、その後の型レベルにはその情報が残らないからだ。空でない配列・リストについても同様で、後続の利用側がそのリストが本当に空でないかを再確認しなければならない場合がある
      この種の情報が常にオブジェクトやコンストラクタにエンコードできるとは限らない
  • 関連資料: Richard Feldman の Making Impossible States Impossible
    https://www.youtube.com/watch?v=IcgmSRJHu_8

  • 以前にも良い議論があった
    https://news.ycombinator.com/item?id=35053118
    https://news.ycombinator.com/item?id=21476261

  • この話題が出るたびに、https://cr.yp.to/qmail/guarantee.html の第5節を思い出す。そこには「パースするな」や「コンピューティングの世界におけるコマンドインターフェイスには2種類ある。良いインターフェイスとユーザーインターフェイスだ」といった文がある
    小規模でも大規模でもなく、中規模のプログラミングを教える授業をするなら、学生にこれらの提案を比較・対照するエッセイを課題として出したい。それぞれ学ぶ点があり、最初に見えるほど矛盾していない可能性もある

  • 2000年代半ばの XML ブームの頃に見たコメントを思い出す。多くの組織が設定言語を含むドメイン特化言語を XML で実装した理由は、おそらく XML がパーサを提供してくれ、ほとんどの組織は自前のパーサを書きたがらなかったからだ、という内容だった
    人々がなぜパーサを書きたがらなかったのかは分からない。パーサを書くのはそれほど難しくなく、かなり楽しい

  • キャリアの中で読んだ記事の中でも特に好きなものの一つ。人々がタイトルだけを読んで、パースと検証が somehow 相互排他的だと仮定することが多いのを見てきたが、実際にはそうではない。パースはしばしば検証を含む
    この内容は記事の “Use abstract datatypes to make validators ‘look like’ parsers” の部分で扱われている
    プリミティブ型への執着を避けようという話と同じ領域にある