前書き
Pythonプログラマの皆様へ
- 用語について
目的別の読み方 ── 皆様のご関心の所在に応じて
- 篩型の概念だけを把握したい方。
TL;DR ── この記事が明らかにすること
想定読者
この記事を読む価値
全体地図
この地図の読み方
- 補足 ── F* の位置付けについて
- 本記事は、「Python を捨てて関数型言語に移行せよ」と主張するものではありません。
第１部 ── 篩型とは、そもそも何か
- まず最初にPythonの型ヒントを、思い出してください
- 篩型は、この「値の条件」を、型そのものに書き込む仕組みです
- 篩型の一般形
- なぜ「型に条件を書ける」ことが嬉しいのか
本節の主要参考文献
第２部 ── 篩型を実装した主要な言語
- LiquidHaskell ── Haskell に後付けされた篩型
  - LiquidHaskell の主要参考文献。
- F* ── Microsoft Research 発の、篩型・依存型・エフェクト・抽出を統合した検証志向言語
  - F* の主要参考文献。
- Typed Racket における refinement / dependent の考え方 ── Lisp/Scheme 系での取り組み
  - Typed Racket の refinement 機能の主要参考文献。
第３部 ── LiquidHaskell のコード例と読み方
- - コード例について
- 例１ ── ゼロ除算を型で防ぐ
- 例２ ── 空でないリストの先頭要素を取り出す
- 例３ ── 自然数を返すことを"「型」で保証"する
- 例４ ── リストの長さを"「型」のレベルで追跡"する
- 例５── 整列済みリストの性質を"「型」に書き込む"
第４部 ── F* のコード例と読み方
- 例１ ── 篩型の基本構文
- 例２ ── ゼロ除算を防ぐ
- 例３ ── リストの長さを、依存型で追跡する
- 例４ ── Hoare論理風の事前条件・事後条件
  - 注記
  - （補足）
- 例５ ── 実世界での応用 ── HTTPS/TLS の暗号ライブラリ
  - HACL* はどう動いているのか？
  - HACL* の産業利用について
  - Python エンジニアへの含意。
第５部 ── Typed Racket の refinement 機能のコード例と読み方
- 例１ ── 篩型の基本構文
- 例２ ── 42 だけを含む型
- 例３ ── ベクトルの安全なアクセス
- 例４ ── 前提条件を使った別の書き方
- 例５ ── 戻り値の性質
第６部 ── 依存型言語 Idris 2 との使い分け
- 依存型と篩型の共通点：「値を型に持ち込む」発想は同じ
- （相違点１）表現の仕方
  - 依存型の書き方（Idris 2）
  - 篩型の書き方（LiquidHaskell）
- （相違点２）検査の仕組み
  - 依存型の検査。
- （相違点３）表現力
- Agentic codeで人間が担うべき部分はAI Agentに委ねられるか？
- これら３つの事例に共通する教訓
使い分けの実践的な指針
- 篩型を選ぶべき場合
- 依存型を選ぶべき場合
- F* のようにハイブリッドを選ぶべき場合。
第７部 ── 篩型が輝く実務の場面
- 場面１ ── 金融計算での符号の保証
- 場面２ ── 配列の範囲外アクセスの防止
- 場面３ ── ゼロ除算の防止
- 場面４ ── REST API の入力バリデーション
- 場面５ ── SQL クエリの安全性
- 場面６ ── 暗号ライブラリ
- 場面７ ── AI エージェントの規則の検証（将来の応用可能性）
第7.5部 ── 同じ問題を３つの世界で解いてみる ── 表現力と検証の広さ・深さの比較
- 問題１ ── 「長さ n のベクトルと長さ m のベクトルを連結すると、長さ n+m のベクトルになる」
３つの世界の対比
- 問題２ ── 「ソートされたリストに要素を挿入すると、結果もソートされている」
３つの世界の対比
- 問題３ ── 「銀行口座の残高は、いかなる時点でも負にならない」
３つの世界の対比
- この対比から学べること。
３つの世界の使い分けの結論
- - 篩型言語（LiquidHaskell、F、Typed Racket の refinement 機能）*
  - 依存型言語（Idris 2、Agda、Lean 4、Rocq）
結論
本節のコード例と参考文献
第8部 ── Python の型ヒントとの関係
- 比較表 ── Python の実行時バリデーションと、篩型言語の refinement types
Curry-Howard 対応との関係
- Python の typing.Annotatedの発想は篩型に近い
- Pydantic の PositiveInt、EmailStr、conint
- 実務の指針 ── Python エンジニアが、今日から取り組めること
第９部 ── Python における篩型ライブラリの現状
- 現状１ ── Python 標準の typing.Annotated(PEP-593)が、篩型の入口
- 現状２ ── annotated-types ライブラリ（共通の制約メタデータ標準）
- 現状３ ── beartype の beartype.vale.Is ── ラムダでその場に述語を書ける
- 現状４ ── Pydantic の Field(...) と AfterValidator
- 現状５ ── FLAT-PY（2025年、学術研究段階）── Python 用の「本格的な」篩型テストフレームワーク
- 現状６ ── typing.TypeIs(PEP 742、Python 3.13)── 篩型そのものではないが、関連する「型絞り込み」の仕組み
- 現状７ ── mypy Issue #560 ── 本格的な篩型の Python 導入は、まだ議論段階
  - なぜ実装されないのか。
- 現状８ ── Python.org Discussion「篩型の仕様の明確化」(2024年)
- 現状の総合評価 ── Python プログラマは得たもの、まだ得ていないもの
  - Python プログラマが、いま既に得ているもの。
  - Python プログラマが、まだ得ていないもの。
- それゆえに、Racket や Idris 2、Lean 4、F* を学ぶ価値がある
**第９部の主要参考文献。
第１０部 ── 学び始めるための最短経路
- 経路A ── LiquidHaskell から入る（Haskell の経験がある皆様）
- 経路B ── F* から入る（篩型と依存型を両方見たい皆様）
- 経路C ── Typed Racket の refinement 機能から入る（Lisp/Scheme の経験がある皆様）
- 経路D ── まず Python の Pydantic で「篩型的な発想」に慣れる
第１１部 ── よくある疑問
- 疑問１ ── SMT ソルバーが自動で全部やってくれるなら、なぜ皆使わないのか
- 疑問２ ── 篩型を書くのに、どのくらいの学習コストがかかるか
- 疑問３ ── Python に篩型を導入する動きはないのか
- 疑問４ ── 篩型と依存型、初学者はどちらから始めるべきか
第12部 ── エピローグ研究の最前線 ── 篩型で「バグの実在」を保証する新しい方向
京都大学五十嵐研究室の研究 ── 到達可能性を検証する篩型システム
- 背景と意義。
６つの技術の一覧比較
この表の読み方
- 皆様がどの水準の保証を必要とするかは、業務の性質次第です。
おわりに ── 篩は、値をふるいにかけ、正しさを残す
参考 ── ブックマークにお勧めの主要ハブ
- LiquidHaskellのハブ
- F* のハブ
- Typed Racket の refinement機能のハブ
- 篩型の主要学術文献 ── 本記事執筆にあたって参照した論文
- Python 篩型ライブラリの公式ドキュメント
先行記事および今後の関連記事
出典についての注記。