1
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

@etale_cohomology(Etale Cohomology)

Pythonの型ヒントの限界を超える「篩型」入門 ―― "x > 0" を型に書くと何が起きるのか （LiquidHaskell・F*・Typed Racket・Idris 2 への誘い）

1
Last updated at Posted at 2026-07-26

thumbnail_picture.jpg

前書き

本記事は、Python しか触ったことのないプログラマの皆様に、篩型（ふるいがた、refinement types） という型システムの考え方を、コード例とその読み方の解説つきで紹介するものです。

「篩（ふるい）型ってなに？」

「Python の型ヒントとは、なにが違うの？」

「依存型（dependent types）というのも、最近よく聞くけれど、いったいなにが違うの？」

「そもそも、Python にも篩型のライブラリはあるの？」

こうした疑問に、Pythonの型ヒントの延長線として、平易にお答えしていきます。

pic_1.jpg

専門家の皆様から誤りをご指摘いただかない水準の正確さは維持しつつ、関数型プログラミングの経験がまったくない皆様にも、噛み砕いた説明を心がけました。
 

Pythonプログラマの皆様へ

Python にも、篩型の発想を導入する主要ライブラリ(annotated-types、beartype、Pydantic の Field + AfterValidator、Python 3.13 の TypeIs)が、既に実用段階で存在します。

これらを業務コードに導入すると、次のような問題が構造的に軽減されます。

  • 「関数の引数に、想定外の値（負の数、空リスト、0）が入ってきて、実行時に落ちる」
     
  • 「Pydantic の入力バリデーションは書いたが、その後の処理では『検証済み』の情報が型で追跡されず、下流でまた if x > 0: を書き続ける」
     
  • 「型ヒントは書いているのに、テストで初めて気付くバグが多い」
     
  • 「配列の範囲外アクセス、ゼロ除算、空リストの先頭要素アクセスが、開発中に見つからない」

Python でも、値の制約を型注釈に近い形で表現し、関数呼び出し時に自動検証させることは、実務レベルで可能です。
 
しかし、それでも Python では原理的に届かない領域があります。

静的検証時の SMT ソルバーによる自動証明、依存型による値の完全追跡、形式検証されたコードの他言語への抽出 ── これらは、Python の実行時篩型ではどうしても実現できません。

金融・暗号・医療・航空といった「実行して初めてバグが分かることが許されない分野」、
AI エージェントの規則の完全検証、数学の定理の機械証明、OS カーネルやコンパイラのような基盤層

こうした場面では以下の関数型言語を学ぶ価値があります。

  • Racket（Typed Racket） の refinement 機能
  • Idris 2
  • Lean 4
  • F*
  • LiquidHaskell

Python で実用上の制約検証を行い、より強い保証が必要な部分だけを形式検証の対象にする
── これが皆様が採り得る現実的なアプローチです。

pic_2.jpg

本記事の第９部では、公式資料の内容を踏まえた 「Python における篩型ライブラリの現状」 をお伝えいたします。
 
なお、本記事に登場する各言語（LiquidHaskell、F*、Typed Racket、Idris 2）の詳細な入門記事は、今後、それぞれ別途執筆する予定です。

本記事は、篩型という考え方の紹介と、各言語のコード例を一望することに徹します。
 

用語について

本記事では「Python の篩型」という言葉を、LiquidHaskell や F* のような完全な静的篩型システムという厳密な意味ではなく、Python の型注釈に値の制約を付加し、静的解析または実行時検証に利用する仕組みを広く指して用います。

これは、Python の annotated-types、beartype、Pydantic、TypeIs などの仕組みが、篩型言語の意味論そのものを Python に持ち込んだものではないためです。

詳しくは、第8部と第9部で明確に整理します。

pic_3.jpg

目的別の読み方 ── 皆様のご関心の所在に応じて

本記事は、篩型の入門から関数型言語の実務応用、最新研究までを網羅した比較的長い記事です。
皆様のご関心に応じて、次のような読み方をお勧めします。

篩型の概念だけを把握したい方。

第１部（篩型とは何か）と、第７．５部（３つの世界で同じ問題を解く）だけをお読みください。
それで篩型の本質と、Python・篩型言語・依存型言語の力の違いは、腹落ちしていただけます。

Pythonで今日から使える篩型的なライブラリを知りたい方。

TL;DR と、第８部・第9部を中心にお読みください。

annotated-types、beartype、Pydantic、TypeIs の実務導入で何が解決するかが、コード例つきで分かります。

関数型言語（LiquidHaskell、F*、Typed Racket）のコード例を見たい方。

第３部から第5部までを、順にお読みください。
各言語のサンプルコードと、Pythonエンジニアの直感で読める解説を用意しています。

依存型言語 Idris 2 との使い分けを知りたい方。

第６部と、第７．５部の問題２「ソート済みリスト」の3世界比較をお読みください。

実務応用と研究の最前線までお知りになりたい方。

第７部（実務の７場面）、第１２部エピローグ（篩型で「バグの実在」を保証する京都大学の研究）まで通してお読みください。

なお、参考文献は本記事の末尾および各節の末尾に、著者・タイトル・URL 付きで明記しました。

TL;DR ── この記事が明らかにすること

第１に、篩型とは「値が満たすべき条件」を型そのものに書き込む型システムです。

Python の型ヒント x: int は「x は整数である」としか言えず、「x は正の整数である(x > 0)」を型として表現できません。

皆様が def divide(x: int, y: int) と書いても、y に 0 が入ることは型では防げず、実行時に ZeroDivisionError が飛ぶことになります。

その一方で、篩型言語では、 x: {v: int | v > 0} と書くことができます。

この記法は「整数 v で、かつ v > 0 を満たすもの全体」という型を意味します。

型そのものに、値の条件を書き込めるのです。

pic_4.jpg

第２に、篩型は、既存の関数型プログラミング言語に「後付け」できるのが強みです。

LiquidHaskell は Haskell に、Typed Racket の refinement 機能は Racket に、それぞれ後付けされています。

pic_5.jpg

第３に、篩型の検査はSMT ソルバー（Z3 など）が自動で行ってくれます。

皆様がコードを書けば、静的検証時に自動で「この関数はゼロ除算を起こさない」といったことを機械が証明してくれます。

pic_6.jpg

第４に、依存型言語 Idris 2 との違いは次のとおりです。

依存型は、「値が型に組み込まれる（長さ5のリスト、という型がある）」仕組みです。

それに対して、篩型は、「型に述語（条件）をつける」仕組みです。

一般的には、依存型のほうが広い種類の依存関係を表現できますが、篩型のほうが既存言語に導入しやすく、SMT ソルバーによる自動検査が効きやすいです。

ただし、両者の境界は言語設計によって異なり、F* のように両者を統合した言語もあります。

pic_7.jpg

詳しくは第６部で扱います。

第５に、実務で篩型が輝くのは次のような場面です。

  • 配列の範囲外アクセスの防止
  • ゼロ除算の防止
  • 金融計算での符号の保証
  • 暗号ライブラリの安全性
  • REST API の入力バリデーション
  • SQL クエリの安全性

いずれも、「値の条件を型に埋め込みたい」場面です。

pic_8.jpg

第６ Python にも篩型のライブラリは既に実用段階で存在します。

annotated-types(共通の制約メタデータ標準)、
beartype(ラムダで述語を書ける実行時型チェック)、
Pydantic の Field + AfterValidator、
Python 3.13 の TypeIs

これらを組み合わせれば、篩型言語の述語による制約表現の相当部分は、Pythonでも書くことができます。

pic_9.jpg

第７ Python プログラマがこれらのライブラリを導入すると、次のような問題が構造的に軽減されます。

「関数の引数に想定外の値が入って落ちる」
「Pydantic でバリデーションしたのに下流でまた if x > 0: を書き続ける」
「テストで初めて気付くバグが多い」
「配列の範囲外アクセス、ゼロ除算、空リストへのアクセス」

これらの悩ましい事象は、コードを修正するだけで、実行時の関数呼び出し段階で自動的に検出されるようになります。

pic_10.jpg

第８ それでも Python では原理的に届かない領域があります。

静的検証時の SMTソルバーによる自動証明、
依存型による値の完全追跡、
形式検証されたコードの他言語への抽出

これらは、金融・暗号・医療・航空・AI エージェントの規則検証・OS カーネル・コンパイラといった領域で必要になります。

そこでは、Racket（Typed Racket の refinement 機能）、Idris 2、Lean 4、F*、LiquidHaskell を学ぶ価値があります。

Python で実用上の制約検証を行い、より強い保証が必要な部分だけを形式検証の対象にする
── これが皆様の採り得る現実的なアプローチです。

pic_11.png

第９ 記事の最後では、篩型の新しい研究方向をご紹介します。

従来の篩型が**「安全性(バグがない)」を保証する**のに対し、
「到達可能性（バグが実在する）」を保証する新しい篩型システムが、佐藤聡太先生ら(京都大学 五十嵐研究室)で研究されています（PPL 2026 発表）。

「到達可能性」とは、少し馴染みのない用語ですので、平易にご説明します。

プログラム解析の用語で「到達可能性（reachability）」とは、「あるプログラムの実行の途中で、特定の状態に本当に到達しうるか」 を問う考え方です。

たとえば、皆様が業務コードを書いていて、こうお思いになる場面があるのではないでしょうか。

  • 「この if 文の中の異常処理、本当に実行されることがあるのだろうか」
  • 「このエラー返却の枝は、そもそも到達不能なのではないだろうか」

こうした場面で皆様が頭の中でお考えになられていることが、「到達可能性」 です。

従来の篩型が保証してきたのは、その裏返しでした。

  • 「この関数は、ゼロ除算が起こる状態には決して到達しない」
  • 「この配列アクセスは、範囲外の状態には決して到達しない」

つまり、「悪い状態への到達不可能性」を保証することで、プログラムの安全性を担保するという発想です。

京都大学の新しい研究は、この発想を裏返しにしました。

  • 「このプログラムは、この悪い状態に到達しうる」
  • 「この入力を与えると、この不正な出力が必ず生じる」

こうした**「バグや悪い状態への到達可能性」を、型で証明する**ことで、バグの実在そのものを形式的に保証する という新しい方向性の研究です。

なぜこれが重要なのでしょうか。

従来の篩型は、「バグがないことの証明」を得意とします。

しかし、実際のセキュリティ研究や品質保証の現場では、「バグがあることの証明」も必要とされます。

  • セキュリティ研究者
    ── 「このシステムには、この入力を与えると、確実に情報漏洩が発生する」ことを形式的に示したい
     
  • 品質保証の担当者
    ── 「このテストケースを与えれば、確実にバグが再現される」ことを機械的に判定したい
     
  • バグ発見のためのツール開発者
    ── ファジング（不規則な入力を与えてバグを発見する手法）やシンボリック実行（記号的にプログラムを実行してバグを探る手法）といった技術と、篩型システムを橋渡ししたい

京都大学の研究は、これらの実務的な需要に、篩型という形式的な理論基盤を与える試みなのです。

「型検査に成功すること」が、「バグが実在すること」を保証する。

これまでとは逆の発想の型システム、とご理解いただけます。

エピローグとして、本記事の最終部でお伝えします。

pic_12.jpg

想定読者

本記事は、次のような方々に向けて書いています。

  • Python でウェブ、機械学習、データ処理の仕事をしている
     
  • Python の型ヒント（typing、mypy、Pydantic）を日常的に使用している
     
  • しかし、関数型プログラミング（Haskell、OCaml、Lisp、Scala、F# など）はまだ触ったことがない
     
  • 「篩型」「依存型」「Curry-Howard 対応」といった用語は、聞いたことはあるが、学んだことがない
     
  • 「型で不正な値を弾く」「コンパイル時にバグを見つける」ことに、なんとなく興味がある

関数型プログラミングの前提知識は要りません。

コード例には、Python エンジニアの皆様に馴染みのある発想を橋渡しする丁寧な解説を添えます。

pic_13.jpg

この記事を読む価値

本記事は、皆様が以下の状態を脱却するお手伝いをすることが目的です。

  • 「型ヒントを書いても、実行時に想定外の値が入ってくるバグに悩まされる」
     
  • 「Pydantic で値を検証しているけれど、もっと根本的に、型で弾く方法はないのか」
     
  • 「Idris 2 の依存型に興味はあるけれど、既存の Python コードにどう活かせるのか、いまいち見えない」

具体的には、次の疑問に順にお答えします。

  • 篩型とは、そもそも何か
     
  • Python の型ヒントとは、どう違うのか
     
  • 篩型を実装した主要な言語は何か
     
  • コードで実際に何が書けるのか、どう読むのか
     
  • 依存型言語（Idris 2）とは、どう使い分けるのか
     
  • 実務のどんな場面で役に立つのか
     
  • Python にも、篩型に相当するライブラリはあるのか。それで何が解決するのか
     
  • Pythonの実行時検証、篩型言語、依存型言語はそれぞれ、表現力と保証の広さ・深さがどう違うのか
     
  • 篩型と依存型のどちらを選ぶべきなのか

すべての参考文献と公式サイトの URL は、記事本文の各解説段落の中に、その場で参照できる形で全て掲載しました。

全体地図

本題に入る前に、これから皆様が歩む道の全体像を地図としてお示しします。

Python の型ヒントから出発し、値の制約を型に付加する発想がどこまで広がっているのか、そしてそれが依存型と定理証明の世界にどう接続していくのか。

これを、１枚の地図としてご覧いただきます。

 

この地図の読み方

  • 一番上に、皆様が日常で書かれている Python の型ヒント があります
     
  • そこからannotated-types、beartype、Pydantic といった Python の実行時検証ライブラリ が、値の制約を型に付加する発想を実務に持ち込んでいます
     
  • その延長線に静的な篩型システム(Refinement Types) があります。LiquidHaskell、F*、Typed Racket の3言語です
     
  • その上により一般的な依存型言語 の世界があります。Idris 2、Agda、Lean 4、Rocq が並びます
     
  • 最上部にCurry-Howard 対応 を経て、定理証明・形式検証の世界 が広がっています
     

補足 ── F* の位置付けについて

この地図では、学習経路の分かりやすさのために、
$「篩型システム → より一般的な依存型言語」$
という段階的な流れを示していますが、F* は篩型と依存型の両方を最初から統合した言語です。

したがって、「F* を学んでから依存型言語へ」というより、「F* の中に篩型も依存型も含まれている」とご理解いただくのが概念的には正確です。

地図の矢印は、皆様の学習進度を示す便宜的な経路であり、言語間の含有関係を厳密に示すものではありません。

 

本記事は、「Python を捨てて関数型言語に移行せよ」と主張するものではありません。

Python の型ヒントを出発点として、値の制約を型に付加するという発想のもと、どこまで保証の度合いを強化できるかを、１つの地図として示すことが本記事の目的です。

Python でできることは Python で、
より強い保証が必要な部分だけを篩型言語や依存型言語で
── これが、本記事を通じて皆様にご覧いただく道筋の風景です。

第１部 ── 篩型とは、そもそも何か

まず最初にPythonの型ヒントを、思い出してください

Python の型ヒントは、こう書きます。

def divide(x: int, y: int) -> float:
    return x / y

この関数、皆様なら、すぐお気づきになるはずです。

y が 0 だったら、実行時に ZeroDivisionError が飛びます。

型ヒントは、x と y が int であることを言うだけで、「y は 0 ではない」という値の条件を、型に書き込むことがはできません。

Pydantic を使えば、こういう書き方もできます。

from pydantic import BaseModel, PositiveInt

class DivideInput(BaseModel):
    x: int
    y: PositiveInt  # 正の整数(0や負の数を弾く)

これで、y に 0 が入ると、実行時に ValidationError が飛びます。

「実行時に弾く」ことはできます。

しかし、「実行前の静的検証で弾く」ことは、Python の型ヒントだけではできません。

篩型は、この「値の条件」を、型そのものに書き込む仕組みです

篩型を持つ言語では、次のようにコードを書くことができます（F* のコード例）。

let divide (x: int) (y: int{y <> 0}) : int = x / y

y: int{y <> 0} の部分に注目してください。

これは「y は整数で、かつ 0 ではない」という型です。

中括弧 { } の中に、y が満たすべき条件を、そのまま書き込めるのです。

そして、この関数を呼び出そうとしたときに、コンパイラは次のことを自動でチェックします。

「呼び出し側で渡している y は、本当に 0 ではないと保証されているのか？」

もし呼び出し側が divide 10 0 と書けば、F* の型検査で拒否されます。
（SMT ソルバー Z3 が y <> 0 を証明できないため）

もし呼び出し側で y が別の場所から来ていて、その y が 0 でないと保証できなければ、やはり F* の型検査で拒否されます。

篩型の一般形

篩型は、一般に次の形で書かれます。

{ v : T | P(v) }

これは、「型 T の値 v のうち、述語 P(v) が成り立つもの全体の型」 を意味します。

Python の型ヒントに例えるなら、次のような疑似コードでイメージいただけます。

# 疑似コード。 実際の Python にはこの記法はありません
y: {v: int | v != 0}
xs: {v: list[int] | len(v) > 0}
n: {v: int | 0 <= v <= 100}

「型に、値が満たすべき条件をつける」── これが篩型の本質です。

「篩（ふるい）」という名前は、「値のうち、条件を満たすものだけを、ふるいにかけて残す」という発想から来ています。

なぜ「型に条件を書ける」ことが嬉しいのか

理由は３つあります。

（理由１） 実行前に値の条件違反を検出できる。

Pydantic の実行時バリデーションと違い、コードを書いてコンパイルした時点で、条件違反が検出されます。

リリース前に、ゼロ除算、範囲外アクセス、空リストへのアクセスといったバグを、機械的に見つけることができるようになるのです。

（理由２） 仕様を「型」としてコードに落とし込むことができる。

y: {v: int | v <> 0} という型そのものが、「この関数は、非ゼロの整数を受け取る」という仕様の記述になっています。

ドキュメントを別途書かなくても、「型」が仕様を雄弁に物語ってくれるのです。

pic_14.jpg

（理由３） SMTソルバーが自動的に証明してくれる。

篩型言語の内部では、Z3などの SMT ソルバー(satisfiability modulo theories、モジュロ理論の充足可能性ソルバー）が自動稼働しています。

皆様がすべきことは、条件の内容を「型」に書き込むことだけです。

「その条件が本当に成り立つか」の証明は、機械（Z3などのSMTソルバー）が引き受けてくれます。

本節の主要参考文献

  • Tim Freeman, Frank Pfenning, Refinement Types for ML （ACM SIGPLAN Notices, Volume 26, Issue 6, PLDI '91, 1991年）

篩型の理論的原論文。ML 言語における refinement types の最初の体系的な提案。

https://dl.acm.org/doi/10.1145/113445.113468
 

  • Ranjit Jhala, Niki Vazou, Refinement Types: A Tutorial arXiv preprint arXiv:2010.07763, （2020年）

篩型のチュートリアル論文。LiquidHaskell を素材に、篩型の基礎から実用まで解
説。本記事の第１部・第３部の基礎となる文献。

https://arxiv.org/abs/2010.07763
 

  • Leonardo de Moura, Nikolaj Bjørner, Z3: An Efficient SMT Solver (TACAS 2008、Springer LNCS 4963)

Microsoft Research による SMT ソルバー Z3 の原論文。本記事で言及する自動証明の基盤技術。

第２部 ── 篩型を実装した主要な言語

篩型を実装した主要な言語を、３つご紹介します。
第２部で取り上げるのは、次の言語です。

  • LiquidHaskell
  • F*
  • Typed Racket の refinement機能

繰り返しますが、本記事は紹介にとどめます。
各言語の詳細な入門記事は、今後、別途執筆する予定です。

pic_15.jpg

LiquidHaskell ── Haskell に後付けされた篩型

LiquidHaskell 公式サイト

  • 公式サイト

  • 公式チュートリアル（Programming with Refinement Types）

  • Niki Vazou 氏の講義資料

位置付け。

Niki Vazou 氏（現在の所属は、IMDEA Software Institute）、Ranjit Jhala 氏（UC San Diego）らが開発した、Haskell に篩型を後付けする GHC プラグインです。

Haskell の既存のコードを書き換えることなく、注釈だけで篩型を導入ですることができます。

評価・評判

「containers、hscolour、bytestring、text、vector-algorithms、xmonad など、Haskell の実世界のライブラリ 10,000 行以上に篩型を導入し、様々な性質を検証した」(Vazou ら、Haskell Symposium 2014)。

さらに、「LiquidHaskell は、TEXT ライブラリの Unicode 処理に潜んでいた微妙なバグを実際に発見し、修正した」（同論文）という実績があります。

「既存の Haskell 資産に、後から強力な型を追加できる」ことが、この言語の大きな強みです。

LiquidHaskell の主要参考文献。

  • Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, Simon Peyton Jones, Refinement Types for Haskell (ACM SIGPLAN International Conference on Functional Programming, ICFP 2014)

LiquidHaskell の中核となる論文

Haskell における篩型の実装、GHC プラグインとしての設計、実世界のライブラリでの検証実績を報告。

  • Niki Vazou, Liquid Haskell: Haskell as a Theorem Prover （博士論文、UC San Diego、2016年）

LiquidHaskell の設計と実装の詳細を体系的にまとめた学位論文。

F* ── Microsoft Research 発の、篩型・依存型・エフェクト・抽出を統合した検証志向言語

F* 公式サイト

  • 公式サイト

  • 公式チュートリアル（Proof-Oriented Programming in F*）

 

位置付け

Microsoft Research と INRIA が開発している、検証志向の関数型言語です。>

篩型と依存型の両方に加え、エフェクト(Effect)システム、Hoare 論理風の事前条件・事後条件、終端性(termination)の検証、OCaml/F#/C への実行コード抽出を統合しています。

構文は OCaml、F# に近く、SMT ソルバー Z3 を統合しています。

単なる「篩型と依存型のハイブリッド」を超えて、**「証明指向プログラミング(Proof-Oriented Programming)」**という、より広い枠組みを提供する言語です。

評価・評判

Project Everest（Microsoft、INRIA、CMU、MIT らが共同で進める、HTTPS スタック全体の形式検証プロジェクト）で、TLS 1.3、暗号ライブラリ HACL、QUIC プロトコルスタックの形式検証*に使われています。

実世界の暗号通信インフラの一部を形式検証し、その検証済みコードを他言語（C、OCaml）に抽出して産業実装に組み込む実績を持つ、代表的な検証志向言語の１つです。

F* の主要参考文献。

  • Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, Santiago Zanella-Béguelin, Dependent Types and Multi-Monadic Effects in F* （POPL 2016）

F* の中核論文。篩型、依存型、モナディックエフェクトの統合設計を提示。

  • Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, HACL*: A Verified Modern Cryptographic Library （ACM CCS 2017）

HACL* の中核論文。F* での暗号ライブラリの形式検証の設計と実装。

Typed Racket における refinement / dependent の考え方 ── Lisp/Scheme 系での取り組み

Typed Racket 公式ドキュメント

  • 公式サイト

  • 篩型導入の公式ブログ（Andrew Kent 氏、2017年11月）

位置付け。

ここでは、Racket の型システム（Typed Racket）に導入された、refinement types（篩型）および dependent function types（依存関数型）の機能を 「既存の型に述語を付加する」観点からご紹介します。

Typed Racket は、Sam Tobin-Hochstadt 氏（Indiana University）が2007年から開発している、Racket用の静的型システムです。

これに、Andrew Kent 氏らが2017年にrefinement/dependent typing の機能を追加しました。

この機能は Racket 6.11（2017年10月）のリリースブログで紹介され、その後の Typed Racket のドキュメントに反映されています。

Racket コミュニティでは、この機能を指して非公式に "Refined Racket" と呼ばれることもありますが、独立した言語処理系というより、Typed Racket の型システムを拡張する一機能、と理解いただくのが正確です。

現在の実装状況の細部については、Typed Racket 公式ドキュメントの最新版をご参照ください。

Sam Tobin-Hochstadt 氏は InfoQ の取材に対し、「Typed Racket に依存型を持たせることで、他の大部分の言語では表現できないようなプログラムのプロパティのチェックが可能になる」と述べています（InfoQ、2018年）。

Lisp/Scheme 系の言語における、篩型/依存関数型の学術的・実装的な取り組みの、代表例の1つです。

Typed Racket の refinement 機能の主要参考文献。

  • Andrew M. Kent, David Kempe, Sam Tobin-Hochstadt, Occurrence Typing Modulo Theories （ACM SIGPLAN Notices, Volume 51, PLDI 2016）

Typed Racket に refinement/dependent typing を導入する理論的基礎を提示した論文。
SMT ソルバー統合の設計を含んでいます。

  • Andrew Kent, Adding Refinement Types to Typed Racket （Racket Blog、2017年11月）
    Typed Racket に refinement types が導入された際の公式ブログ記事。
    Racket 6.11 での機能安定化を報告。

  • 川崎有亮 訳「Racket 6.11 のリリースで依存型と篩型が安定機能に(Racket 6.11 released, refinement types now stable)」(InfoQ 日本語版、2018年1月)

Sam Tobin-Hochstadt 氏へのインタビューを含む。

第３部 ── LiquidHaskell のコード例と読み方

ここから、LiquidHaskell の実際のコード例 をご覧いただきます。

構文は Haskell ですが、篩型の注釈は {-@ ... @-} というコメント風の記法で書かれます。

まだHaskellは未学習であっても、Pythonエンジニアの直感でお読めいただけるように丁寧に解説します。

コード例について

以下のコード例は、LiquidHaskell の公式チュートリアル と Vazou 氏らの入門資料 に基づく 概念説明用のスニペット です。

実際に動作させる際は、LiquidHaskell の環境構築とバージョンに応じた微修正が必要になる場合があります。
詳細は公式チュートリアルをご確認ください。

例１ ── ゼロ除算を型で防ぐ

【概念説明用のスニペット】
LiquidHaskell 公式チュートリアルを参考にした概念説明用コードです。
実処理系での動作には環境構築とバージョンに応じた修正が必要な場合があります。

{-@ divide :: Int -> {v:Int | v /= 0} -> Int @-}
divide :: Int -> Int -> Int
divide x y = x `div` y

Python エンジニアのための解説。

divide :: Int -> Int -> Int の部分は、Python でいえば def divide(x: int, y: int) -> int: に対応します。

その上にある {-@ divide :: Int -> {v:Int | v /= 0} -> Int @-} が LiquidHaskell の篩型注釈 です。

第２引数の型が {v:Int | v /= 0} になっており、「v は整数で、かつ v ≠ 0」を意味します。

つまり、この関数を呼び出す側は、y が 0 でないことを LiquidHaskell の静的検証時に保証しなければならない、という意味です。

もし呼び出し側が divide 10 0 と書いたら、LiquidHaskell の検証段階で拒否されます(Haskell 本体のコンパイルは通っても、LH プラグインの静的検証を通過できません)。

Python の Pydantic の PositiveInt は「呼び出したとき実行時にチェック」ですが、LiquidHaskell は「Haskell のコンパイル後に、LH プラグインが SMT ソルバーの支援を受けて静的に検証する」という違いがあります。

例２ ── 空でないリストの先頭要素を取り出す

【概念説明用のスニペット】

{-@ head :: {xs:[a] | len xs > 0} -> a @-}
head :: [a] -> a
head (x:_) = x

Python エンジニアのための解説。

[a] は Haskell のリスト型(Python の list に相当)、len はリストの長さです。

篩型注釈 {xs:[a] | len xs > 0} は、「リスト xs で、その長さが 0 より大きいもの」を意味します。

つまり、空リストを渡すコードは、LiquidHaskell の検証を通過できません。

Python でいえば、xs[0] を呼ぶ前に if xs: チェックを書く、というパターンを、型で強制する発想です。

「空リストへのアクセスで実行時エラー」という、Python でよくあるバグの一種を、根本的に消せます。

例３ ── 自然数を返すことを"「型」で保証"する

【概念説明用のスニペット】

{-@ absoluteValue :: Int -> {v:Int | v >= 0} @-}
absoluteValue :: Int -> Int
absoluteValue x
  | x >= 0    = x
  | otherwise = -x

Python エンジニアのための解説。

{v:Int | v >= 0} は、「値 v が 0 以上の整数」を意味します。

absoluteValue の戻り値の型がこれになっているので、「この関数は必ず非負の整数を返す」ことが LiquidHaskell の静的検証時に検証されます。

もし実装を間違えて負の値を返す枝を書いてしまうと、LiquidHaskell の検証で拒否されます。

戻り値の性質を型に埋め込むことで、Pythonの assert result >= 0 を書かなくても、機械が代わりに保証してくれます。

例４ ── リストの長さを"「型」のレベルで追跡"する

【概念説明用のスニペット】

{-@ append :: xs:[a] -> ys:[a] 
             -> {v:[a] | len v = len xs + len ys} @-}
append :: [a] -> [a] -> [a]
append []     ys = ys
append (x:xs) ys = x : append xs ys

Python エンジニアのための解説。

append はリスト2つを連結する関数(Python の xs + ys)です。

篩型注釈の戻り値の型 {v:[a] | len v = len xs + len ys} が言っているのは、「連結後のリスト v の長さは、xs の長さと ys の長さの和である」ということです。

もし実装を間違えて、例えば要素を1つ落としてしまうと、長さの等式が成り立たなくなり、LiquidHaskell の検証を通過できません。

これは、依存型言語 Idris 2 の Vect の連結と、まさに同じことを、篩型で表現している例です。

例５── 整列済みリストの性質を"「型」に書き込む"

【概念説明用のスニペット】

{-@ measure isSorted :: [Int] -> Bool
    isSorted []       = True
    isSorted [x]      = True
    isSorted (x:y:xs) = x <= y && isSorted (y:xs)
  @-}

{-@ insert :: x:Int -> {xs:[Int] | isSorted xs} 
            -> {v:[Int] | isSorted v} @-}
insert :: Int -> [Int] -> [Int]
insert x [] = [x]
insert x (y:ys)
  | x <= y    = x : y : ys
  | otherwise = y : insert x ys

Python エンジニアのための解説。

measure isSorted は、「リストが整列しているか」を判定する述語を、篩型の世界の中で定義しています。

insert 関数の型は、**「整列済みのリスト xs に要素 x を挿入すると、結果もまた整列済みである」**という不変条件を保証しています。

もし実装を間違えて、整列を崩す挿入をしてしまうと、LiquidHaskell の検証を通過できません。

Python で assert is_sorted(result) を実行時に書いても、テストケースを網羅できなければバグは残ります。

LiquidHaskell では、静的検証時に、すべての入力について整列が保たれることが SMT ソルバーの支援を受けて機械的に証明されます。

第４部 ── F* のコード例と読み方

F* は、篩型・依存型・エフェクト・termination checking・コード抽出を統合した検証志向の言語です。

Python エンジニアの皆様が「篩型の実際の使い方」をもっとも見やすい構文をしています。

コード例について。
以下のコード例は、F* 公式チュートリアル(Proof-Oriented Programming in F*)に基づく概念説明用のスニペットです。

実際に動作させる際は、F* の環境構築と、SMT ソルバー Z3の統合が必要です。
詳細は公式チュートリアルをご確認ください。

例１ ── 篩型の基本構文

【概念説明用のスニペット】
F* 公式チュートリアルを参考にした概念説明用コードです。実処理系での動作には環境構築と Z3 の統合が必要です。

type nat = x:int{x >= 0}
type non_zero = y:int{y <> 0}

Python エンジニアのための解説。

type は、Python の TypeAlias に近い、型に別名をつける宣言です。

nat = x:int{x >= 0} は、「整数 x で、x >= 0 を満たすもの」全体に、nat という名前をつけた、と読めます。

同様に、non_zero は「0 でない整数」です。

Python エンジニアの直感でいえば、Pydantic の PositiveInt や NonNegativeInt を、自分で自由に定義できる感覚です。

例２ ── ゼロ除算を防ぐ

【概念説明用のスニペット】

let divide (x: int) (y: non_zero) : int = x / y

Python エンジニアのための解説。

第2引数の型が non_zero(先ほど定義した「0でない整数」)なので、この関数は 0 を渡されることがない、とコンパイラが保証します。

呼び出し側で divide 10 0 と書けば、F* の型検査で拒否されます(SMT ソルバー Z3 が y <> 0 を証明できないため)。

LiquidHaskell と同じ発想ですが、F のほうが構文がすっきりしています。*

例３ ── リストの長さを、依存型で追跡する

【概念説明用のスニペット】

val append : l1:list 'a -> l2:list 'a 
             -> res:list 'a{length res = length l1 + length l2}

Python エンジニアのための解説。

戻り値の型が res:list 'a{length res = length l1 + length l2} になっており、「結果のリスト res は、l1 と l2 の長さの和と等しい長さを持つ」と宣言しています。

F では、篩型の中で length l1 + length l2 のような他の値を参照できます。*

これは「依存型」の性質(戻り値の型が引数の値に依存する)を、篩型の記法で書いた例です。

F は、篩型と依存型がシームレスにつながっている*のが特徴です。

例４ ── Hoare論理風の事前条件・事後条件

【概念説明用のスニペット、簡略化した例】

val factorial : n:nat -> Tot (m:nat{m >= 1})
let rec factorial n =
  if n = 0 then 1
  else n * factorial (n - 1)

注記

これは F* の仕様記述能力を直感的にお示しするための簡略化した例です。

実際の F* では、型注釈だけでなく、終端性（termination）や事前条件・事後条件の検証条件も、SMT ソルバーZ3の支援を受けて確認されます。

上記の文には、Pythonエンジニアの皆様には馴染みの薄い用語がいくつか含まれていますので、簡潔に補足いたします。
 

  • 終端性（termination） ── プログラムが有限時間で必ず停止することを指す性質です。

Python で書かれた while True: や、再帰の停止条件を書き忘れた関数は、終端性が保証されていないプログラムの例です。

F* の終端性検査は、再帰関数について、「再帰の各ステップで、何らかの尺度（通常は自然数）が確実に減少する」ことを検査することで、無限に呼び出しが続かないことを保証します。

  • 事前条件（precondition）・事後条件（postcondition） ── 関数を呼び出す前に成立していなければならない条件を**「事前条件」、関数の実行後に必ず成立していることが保証される条件を「事後条件」**といいます。

Python で例えるならば、次のような発想です。

def divide(x: int, y: int) -> float:
    assert y != 0        # 事前条件
    result = x / y
    assert result * y == x  # 事後条件
    return result

Pythonでは、 assert で実行時にチェックするしかありませんが、F* では、事前条件・事後条件を型の一部として書くことで、静的検証時にSMTソルバーの支援を受けて機械的に確認することができます。
 

  • SMT ソルバー Z3 ── SMTとは、"Satisfiability Modulo Theories"（モジュロ理論の充足可能性）"を意味しています。「与えられた論理式が本当に成り立つか」を機械的に判定するプログラム です。

Z3 は Microsoft Research が開発した、この分野で最も広く使われる SMTソルバーです。

整数の線形演算、比較、論理演算、配列やビット列の性質など、幅広い数学的性質を自動で判定できます。

F* の型検査は、「この型のこの条件が本当に成り立つか」を Z3 に問い合わせ、Z3 が『成り立つ』と答えたときに、初めて検証成功と判定します。

皆様が『条件を型に書く』だけで、Z3 が背後で自動的に証明を構築してくれる
── これが、F* をはじめとする篩型言語の中核的な体験です。

詳細は、F* 公式チュートリアルをご確認ください。

Python エンジニアのための解説。

n:nat は、「n は自然数(0以上の整数)」という事前条件です。

Tot (m:nat{m >= 1}) は、「この関数は、純粋な全域計算(Total)というエフェクトを持ち、戻り値 m は自然数で、かつ m >= 1」という宣言です。

（補足）

Tot は F* のエフェクト表記の１つで、純粋な全域計算（副作用がなく、任意の入力について値を返す）を表します。

しかし、「Tot と書いたコードは必ず停止する」のではありません。
再帰関数が実際に停止することは、F* の**終端性検査(termination checking)**によって、別途検証されます。

まとめると、次の関係にあります。

  • Tot ── 純粋な全域計算というエフェクトの宣言

  • termination checking ── 再帰が実際に停止することの、独立した検証

この２つが揃うことで、F* の型検査は、「この関数は任意の nat 入力について、必ず m >= 1 の値を返して停止する」ことを保証することができるようになります。

これは、C言語の世界での ACSL（ANSI/ISO C Specification Language）や、Java 界隈の JML（Java Modeling Language）の事前条件・事後条件を、型システムに統合したもの とご理解いただけます。

pic_16.jpg

例５ ── 実世界での応用 ── HTTPS/TLS の暗号ライブラリ

F* の代表的な応用例は、HACL（High-Assurance Cryptographic Library）* です。

HACL* 公式サイト

  • 公式サイト

HACL* はどう動いているのか？

F* で書かれた検証済みコードは、そのままの形で実行されるのではなく、Low* という「C言語に近い、Fのサブセット言語」を経由して、安全で高速な C コードとして抽出・コンパイルされます。

つまり、開発者は F* で数学的に検証された仕様を書くことで、その検証結果をそのまま保ったまま、実行時性能に優れたCコードを得られる、という設計です。

pic_17.jpg

HACL* の産業利用について

HACL* の検証済みコードは、暗号ライブラリや主要なソフトウェア基盤への統合実績を持つと HACL* プロジェクトが公表しています。

具体的な採用箇所や現在の構成の詳細は、HACL* 公式ドキュメントや各プロジェクトの現行ドキュメントをご確認ください。

Python エンジニアへの含意。

Python の暗号処理（cryptography パッケージなど）は、多くの場合、裏側でC拡張として OpenSSL や他の暗号ライブラリを呼び出しています。

篩型言語で検証されたコードが、実世界の暗号インフラの一部を担うようになりつつある という現状を、Python エンジニアの皆様にご理解いただければ、これから触れる形式検証の世界の「実務との距離感」が掴めるはずです。

篩型言語による産業実装が、皆様が今日使っているブラウザや OS、そして Python の暗号処理の裏側の技術基盤にまで、少しずつ広がりつつある
── これが、F* の実世界での姿です。

第５部 ── Typed Racket の refinement 機能のコード例と読み方

Typed Racket の refinement/dependent typing 機能 は、Lisp/Scheme の構文で 篩型的な記述を可能にします。

例１ ── 篩型の基本構文

【概念説明用のスニペット】
Andrew Kent 氏の Racket ブログ記事（2017年）と Typed Racket 公式ドキュメントに基づく概念説明用コードです。

実装の詳細と動作可能性は、Typed Racket 公式ドキュメントの最新版をご確認ください。

(Refine [v : Integer] (> v 0))

Python エンジニアのための解説。

Refine が、篩型を表すキーワードです。

[v : Integer] の部分は「整数 v」、(> v 0) の部分は「v > 0」を意味します。

つまり、この型は 「正の整数」 を表しています。

Racketは Lisp系 なので、括弧の入れ子で全部を書きます。

例２ ── 42 だけを含む型

【概念説明用のスニペット】

(ann 42 (Refine [n : Integer] (<= n 42)))

Python エンジニアのための解説。

ann は「型注釈(annotation)」で、「値 42 に、(Refine [n : Integer] (<= n 42)) という型をつける」と読めます。

「42 以下の整数」全体の型を作り、そこに 42 を入れています。

InfoQ の記事(2018年)で紹介された、Racket の篩型の代表例です。

例３ ── ベクトルの安全なアクセス

【概念説明用のスニペット】

(: safe-ref1 (All (A) (-> ([v : (Vectorof A)]
                           [n : (v) (Refine [i : Natural]
                                (< i (vector-length v)))])
                            A)))

Python エンジニアのための解説。

Racket の構文なので括弧が多いですが、要点はこうです。

第2引数 n の型 (Refine [i : Natural] (< i (vector-length v))) は、「自然数 i で、かつ i < ベクトル v の長さ」を意味します。

つまり、「ベクトルの範囲内のインデックスだけを受け付ける」型です。

Python でいえば xs[n] を実行するときに assert 0 <= n < len(xs) を書くパターンを、型で強制する発想です。

配列の範囲外アクセスに関するバグを、Typed Racket の型検査の段階で捕捉できる という 篩型/依存関数型の代表的な使い方 です。

例４ ── 前提条件を使った別の書き方

【概念説明用のスニペット】

(: safe-ref2 (All (A) (-> ([v : (Vectorof A)]
                           [n : Natural])
                          #:pre (v n) (< n (vector-length v))
                          A)))

Python エンジニアのための解説。

同じ「安全なベクトルアクセス」を、#:pre という前提条件(precondition)構文で書いた版です。

型の中に条件を埋め込むのではなく、関数のシグネチャの前提として明示的に書くスタイルです。

こちらの記法のほうが、Hoare論理の事前条件を書き慣れた方には自然に読めます。

例５ ── 戻り値の性質

【概念説明用のスニペット】

(-> ([x : Integer] [y : Integer]) 
    (Refine [z : Integer] (and (>= z x) (>= z y))))

Python エンジニアのための解説。

これは、「2つの整数を受け取り、両方以上の値を返す関数」 の型です。

戻り値の型 (Refine [z : Integer] (and (>= z x) (>= z y))) が、「z >= x かつ z >= y」を宣言しています。

これはPython でいえば max(x, y) 相当の関数の型を篩型で書いた例です。

戻り値の性質を、機械が検証できる形で書くことができる　ことが、篩型の威力です。

第６部 ── 依存型言語 Idris 2 との使い分け

ここが本記事の核心の１つです。

Python エンジニアの皆様が最も疑問に思われるのは、次の点でしょう。

「依存型と篩型は、なにが違うのか。 どう使い分けるのか。」

pic_18.jpg

第６部ではこの問いに答えます。

依存型と篩型の共通点：「値を型に持ち込む」発想は同じ

まずは、両者の共通点から解説します。

依存型言語（Idris 2、Agda、Lean 4、Rocq）と、篩型言語（LiquidHaskell、F、Typed Racket の refinement 機能*）はいずれも、 「値の情報を、型のレベルに持ち込む」 ことを目指しています。

Pythonの型ヒントが「値の集合の名前（int、str、list）を型に書く」ものだとすれば、依存型と篩型は「値そのものや、値の条件を型に書く」ものです。

pic_19.jpg

（相違点１） 表現の仕方

依存型の書き方（Idris 2） 

data Vect : Nat -> Type -> Type where
  Nil  : Vect Z a
  (::) : a -> Vect k a -> Vect (S k) a

Python エンジニアのための補足。

ここで Z はゼロ(Zero)、S k は「k の次の数」(Successor)を表す、ペアノ自然数の記法です。

つまり Z は 0、S Z は 1、S (S Z) は 2 に対応します。

関数型言語では、自然数をコンストラクタで再帰的に構築するこの流儀が広く使われています。

上のコードは、「空の Vect は長さ Z、要素を１つ足した Vect は長さが $Sk$(元の長さ $k$ の次)になる」ことを、型のレベルで直接、宣言しています。

「長さが型に組み込まれた Vect n a という型を直接定義する」書き方です。

長さ n そのものが、型の一部として書かれています。

篩型の書き方（LiquidHaskell） 

{-@ type VectN a N = {v:[a] | len v == N} @-}

{-@ append :: xs:[a] -> ys:[a] 
             -> {v:[a] | len v = len xs + len ys} @-}

「既存のリスト型 [a] に、len v == N という 述語 をつけて、『長さがNのリスト』を表現する」書き方です。

長さは、リスト型の外から述語として付与しています。

（相違点２） 検査の仕組み

依存型の検査。

依存型の検査は、言語処理系の中の型検査器が、静的検査フェーズで評価と型検査を組み合わせて行います。

Idris 2、Agda、Lean 4、Rocq は、それぞれ独自の依存型を持つ、新しい言語処理系です。

そのため、依存型を導入するには、新しい言語処理系ごと採用する必要があります。

 

篩型の検査。

篩型の検査は、SMT ソルバー(Z3 など)に、条件式を渡して自動証明させます。

LiquidHaskell は Haskell の GHC プラグイン、Typed Racket の refinement 機能は Typed Racket モジュールの一部として、既存の言語処理系に「後付け」できます。

そのため、既存の Haskell や Racket のコード資産を保ちながら、篩型の機能を追加できます。

（相違点３）表現力

一般には、依存型のほうが、広い種類の依存関係を表現できます。

依存型は、型の構成要素として値を直接扱えるため、たとえば「行列の積 $A × B$ が定義できるのは、$A$ の列数と $B$ の行数が等しいときだけ」といった性質を、型のレベルで直接表現できます。

篩型でも、リストの長さや値の範囲といった依存関係を記述することは可能です。
しかし、述語の複雑さに応じて、SMT ソルバーが解けなくなる場合があります。

ただし、両者の境界は言語設計によって異なります。

たとえば F* は、篩型と依存型を統合し、さらにエフェクトと termination checking を組み合わせた設計で、両者の使い分けそのものを内部化しています。

「篩型と依存型」という二分法は、初学者が全体像を掴むための便宜的な区分としてご理解ください。

pic_20.jpg

上記の二分法を敢えて用いた上で表現するならば、篩型のほうが、自動検査が効きやすいと考えれます。

篩型が扱う述語は、多くの場合、整数の線形演算、比較、論理演算といった、SMT ソルバーが得意な範囲に収まります。

そのため、皆様がコードを書くだけで、機械が自動で証明を完成させてくれることが多いです。

依存型の場合、複雑な性質になると、皆様自身が証明のヒントを書く必要が出てきます。

「証明のヒント」とは、少し馴染みのない表現ですので、簡潔にご説明します。

依存型言語では、複雑な性質を「型」として書いたとき、型検査器が、 「この型は本当に成り立つか」を人間のプログラマ助けなしに自力で判定することができない場面 があります。

依存型言語 における**「証明のヒント」とは、まさにこの「手順を追った説明」を、機械が読める形式で書き下すこと**です。

具体的には、次のようなものです。

  • 補題（lemma）の適用 ── 「先に証明されたこの補題を、ここで使えば、この性質が成り立つ」と型検査器に指示する
     
  • 帰納法の展開 ── 「リストの長さについて、この帰納段階を明示的に展開せよ」と型検査器に指示する
     
  • 書き換え規則（rewrite）の適用 ── 「この等式を、ここで両辺に適用せよ」と型検査器に指示する
     
  • タクティク（tactic）の呼び出し ── Lean 4、Rocq、Agda などでは、証明を組み立てるための小さなプログラム（タクティク）を、開発者自身が書き下す

篩型言語では、こうしたヒントの多くを SMT ソルバーが自動的に構築してくれるため、開発者は主に「型に述語を書く」ことに集中できます。

これに対し、依存型言語では、開発者が『機械と対話しながら証明を組み立てる』作業が必要になる場面があります。

この点が、依存型言語の学習コストが高いと言われる主な理由の１つです。

Agentic codeで人間が担うべき部分はAI Agentに委ねられるか？

では、これらの「証明のヒント」を、AI エージェントに任せて自動化できないのでしょうか。

先行記事の定理証明・形式検証はいまから学ぶ価値があるかでも触れましたが、この論点は、皆様が業務で AI エージェントを使い始めた場面で、必ず直面するであろう問いです。

結論としては、以下のようになるのではないかと本記事執筆者は考えています。

AI エージェントに任せて自動処理できる部分と、原理的に自動化しにくい部分の両方があります。

AI エージェントに任せやすい部分としては、以下を挙げることができます。

  • 定型的な補題の適用
    ── 「リストの長さについての標準的な補題」「自然数の加法の交換法則」といった、証明支援系のライブラリに登録されている補題を状況に応じて適用する作業は大規模言語モデルが得意な領域です
     
  • タクティクの候補提示
    ── Lean 4 の exact?、apply?、hint といった対話的タクティクの支援機能はAI エージェントとの相性が非常によく、次にどのタクティクを試すべきかを、AI が候補として提示することが実用段階に入りつつあります
     
  • 既存の証明パターンの再利用
    ── 過去に検証された類似のコードから証明の骨格を提示する作業は、AI エージェントに任せられます
     

AI エージェントに任せにくいと考えらえる部分としては、以下が考えらえるのではないでしょうか。
 

  • 本質的に新しい数学的洞察を要する証明
    ── 単なるパターンマッチングでは到達できない「この問題の本質は、こういう抽象化にある」という洞察は、AI エージェントが単独で構築するのは、現時点では非常に困難です
     
  • 証明の正しさそのものの保証
    ── AI エージェントが提示した証明が本当に正しいかは、証明支援系（Lean 4、Rocq、Agda など）が最終的に判定します。AI エージェントの提示を鵜呑みにすることはできず、証明支援系による機械的な最終検証が不可欠です
     
  • 仕様そのものが正しいかの判断
    ── そもそも「何を証明するべきか」という仕様の設計は、人間の専門家の判断に大きく依存します。
    AI エージェントに委ねすぎると、間違った命題を正しく証明してしまう危険があります
     
    この危険を具体的に理解いただくため、ソフトウェア工学の歴史における３つの有名な事例をご紹介します。いずれも「ソフトウェアは仕様通りに動作していたが、仕様そのものに問題があったために大きな事故につながった」事例です。
     

事例１ ── Boeing 737 MAX の MCAS（Maneuvering Characteristics Augmentation System）

2018年10月の Lion Air Flight 610、2019年3月の Ethiopian Airlines Flight 302、合わせて346名の犠牲者を出した2つの墜落事故は、いずれも MCAS という機体自動制御ソフトウェアの設計欠陥に起因していました。

MCAS のソフトウェアは、仕様通りに正しく動作していました。仕様書には、次のように書かれていました。

「単一の AOA（Angle of Attack、迎角）センサーの読み値が閾値を超えたら、機体の水平尾翼を下向きに制御し、機首を強制的に下げる」

問題は仕様そのものにありました。

AOA センサーは機体の左右に２つ搭載されていたにもかかわらず、MCAS の仕様は「単一のセンサーに依存する」 という設計になっており、単一障害点（single point of failure） が仕様レベルで組み込まれていたのです。

事故後の設計改修では、「2つの AOA センサーの読み値を比較し、両者が一致するときのみ作動する」という仕様レベルでの冗長性 が導入されました。

（出典）

Boeing CEO Dennis Muilenburg の議会証言（2019年10月）
FAA の Boeing 737 MAX 審査の要約報告書

FAA Summary of the Boeing 737 MAX Return-to-Service

事例２ ── Therac-25 放射線治療装置

1985年から1987年の間に、Atomic Energy of Canada Limited（AECL）が製造した Therac-25 放射線治療装置により、少なくとも6名の患者が、想定の最大100倍の致死量の放射線を照射され、深刻な負傷または死亡に至りました。

先行モデルの Therac-6 および Therac-20 には、機体誤動作時に照射を物理的に阻止するハードウェアインターロックが搭載されていました。

しかし、Therac-25 ではコスト削減のため、ハードウェアインターロックが除去され、ソフトウェア側のチェックだけに安全性を依存させるという設計変更が行われました。

ソフトウェアは仕様通りに動作していたものの、仕様レベルでのハードウェア冗長性が省略された結果、レースコンディション等のソフトウェア不具合を物理的に阻止する最後の砦がなくなっていたのです。

（出典）
Nancy Leveson & Clark S. Turner, An Investigation of the Therac-25 Accidents, IEEE Computer, July 1993（この分野の定説的な学術論文）。

UMN 掲載の Therac-25 事例研究、Ethics Unwrapped Therac-25 事例研究
 

事例３ ── Ariane 5 ロケット

1996年6月4日、欧州宇宙機関（ESA）の Ariane 5 ロケットの初飛行（Ariane 501）は、打ち上げから約37秒後に爆発し、約3億7,000万ドル相当の科学衛星4基が失われました。

原因は、慣性基準システム（Inertial Reference System, IRS）のソフトウェアにありました。

このソフトウェアは、先行モデル Ariane 4 用に開発されたものが、Ariane 5 で再利用されていました。

Ariane 4 の飛行条件では、水平速度は 16 ビット符号付き整数の範囲に収まっていました。
Ariane 4 のソフトウェアは、この Ariane 4 の運用条件の範囲内では、仕様通りに正しく動作していました。

しかし Ariane 5 は Ariane 4 より速く、より急な軌道を持つ次世代機でした。

Ariane 5 の水平速度は 16 ビット符号付き整数の範囲を超え、整数オーバーフローが発生し、慣性基準システムが停止、機体が制御を失い、自動的な自爆装置により破壊されました。

ESA インクワイアリーボードの公式報告書は、この事故の原因を 「慣性基準システムのソフトウェアにおける仕様および設計の誤り（specification and design errors in the software of the inertial reference system）」 と結論付けています。

（出典）
ESA インクワイアリーボード公式報告書（1996年）。

ESA 公式プレスリリース ── Ariane 501 Inquiry Board Report
 

これら３つの事例に共通する教訓

いずれの事例においても、ソフトウェアは仕様通りに動作していました。
ソフトウェア実装レベルでは、決定的なバグはありませんでした。

問題は、仕様そのものにあったのです。

  • Boeing 737 MAX ── 「単一のセンサーに依存する」という仕様の欠陥
  • Therac-25 ── 「ハードウェアインターロックなしでソフトウェアだけで安全を担保する」という仕様の欠陥
  • Ariane 5 ── 「Ariane 4 の仕様は、Ariane 5 でも成立する」という仕様の暗黙の前提

もし当時、AI エージェントに、これらのソフトウェアの証明を委ねていたとしたら、AI エージェントはこう証明したはずです。

「MCAS のソフトウェアは、仕様通りに正しく動作する」
「Therac-25 のソフトウェアは、仕様通りに正しく動作する」
「Ariane 4 の慣性基準ソフトウェアは、Ariane 4 の仕様通りに正しく動作する」

これらの証明は、論理的にはすべて正しい のです。

しかし、仕様そのものが誤っていた（または、新しい運用環境では成立しなくなっていた） ため、これらの「正しい証明」が、数百名の犠牲者を防ぐことも、数億ドルのロケットを守ることもできませんでした。

AI エージェントは、「間違った命題を、正しく証明してしまう」
── これが、AI エージェントに全てを委ねてはいけない、最も本質的な理由 です。

依存型プログラミングにおいても、AI エージェントが得意なのは「与えられた仕様に対する証明の構築」であり、「そもそもその仕様が正しいかの判断」は、皆様のような領域の専門家の役割として残り続けます。

pic_21.jpg

この構造は、Python プログラマの皆様が Agentic Coding（AI エージェントによるコーディング支援）を業務に導入するときの構造と、実は同型です。

「AI に書かせたコードを、テストで検証する」という Pythonの実務と、「AI に提示させた証明を、証明支援系で検証する」という依存型言語の実務は、『AI が生成し、機械が検証する』という同じ枠組みの上に立っています。

この意味で、依存型プログラミングは、Agentic Coding 時代の仕様駆動開発（spec-driven development）と自然に接続する、と申し上げてよいでしょう。

pic_22.jpg

 
なお、篩型・依存型プログラミングを、Agentic Coding の仕様駆動開発スタイルで実践する具体的なイメージについては、別の記事で改めてご紹介する予定です。

本記事では、皆様に**「AI エージェントの支援がある時代においても、篩型・依存型プログラミングの学習には意義がある」**という視点を、先取りしてお伝えするにとどめます。

使い分けの実践的な指針

Pythonエンジニアの皆様に、実務での使い分けの指針をご提示します。

篩型を選ぶべき場合

  • 既存の Haskell、Racket、OCaml、F# などの資産を活かしながら、型を強化したいとき
     
  • 検証したい性質が、「値の範囲、比較、論理式、リストの長さ」といった、SMT ソルバーが得意な範囲に収まるとき
     
  • 皆様自身が証明を書くのではなく、機械に自動で証明させたいとき
     
  • 実世界の産業コードに、段階的に検証を導入したいとき

pic_24.jpg

依存型を選ぶべき場合

  • 数学の定理を形式化したいとき（HoTT、ホモトピー型理論、圏論など）
     
  • 検証したい性質が、SMTソルバーが扱えないほど複雑である場合（高次の量化、複雑な帰納構造など）
     
  • 皆様自身が証明の詳細を書き、機械に形式的に検査させたいとき
     
  • 新しい言語処理系（Idris 2、Agda、Lean 4、Rocq）を採用する余地があるとき

pic_25.jpg

F* のようにハイブリッドを選ぶべき場合。

  • 実務のコード検証と数学的な深い証明の両方を行いたいとき
     
  • SMTソルバーで自動証明できる部分は自動で、できない部分は明示的な証明で埋めたいとき
     
  • 暗号ライブラリ、OS カーネル、コンパイラといった、産業レベルの高信頼ソフトウェアを構築したいとき

篩型と依存型は敵対する概念ではありません。 F* が示すように、両者は自然に統合できます。

pic_23.png

第７部 ── 篩型が輝く実務の場面

Python エンジニアの皆様に、篩型 が実務で活きる場面を、具体的にお伝えします。

場面１ ── 金融計算での符号の保証

金額、残高、金利は、通常は非負であるべきです。

Python では、次のように書きます。

def calculate_interest(balance: float, rate: float) -> float:
    if balance < 0 or rate < 0:
        raise ValueError("negative")
    return balance * rate

篩型なら、こう書けます。

val calculate_interest : balance:{v:float | v >= 0.0} 
                       -> rate:{v:float | v >= 0.0}
                       -> {v:float | v >= 0.0}

実行時のガード節が不要になり、そもそも負の値を渡すコードがコンパイルできなくなります。

金融、会計、税務のような、符号や範囲の間違いが致命的な業界で、篩型の価値は非常に高いです。

場面２ ── 配列の範囲外アクセスの防止

Python の IndexError、
C 言語のバッファオーバーフロー

これらはいずれも**「範囲外アクセス」**です。

篩型なら、インデックスの型を「配列の長さより小さい非負整数」に絞れば、範囲外アクセスの多くを、静的検証時の段階で検出できます。

Typed Racket の safe-ref1 の例がまさにこれです。

場面３ ── ゼロ除算の防止

先ほど何度も見てきた例です。
除数の型を「非ゼロの数」に絞れば、ゼロ除算のケースを型検査の段階で捕捉することができます。

科学技術計算、機械学習の損失関数、統計処理など、ゼロ除算が潜みやすい分野で有効です。

場面４ ── REST API の入力バリデーション

Pydantic の役割の一部を、静的検証時に完結させられます。

「メールアドレスの形式」
「日付の妥当性」
「文字列の長さ制限」

といった、API のリクエスト検証内容を型として記述することができます。

もちろん、外部からの入力自体は実行時にパースする必要があります。
（この点は Pydanticと同じ）

しかし、パース後の処理コード全体を通じて、「もう検証済みの値である」ことが型で保証されます。

場面５ ── SQL クエリの安全性

「エスケープ済みの文字列」
「妥当なテーブル名」
「範囲内の LIMIT 値」

といった SQL インジェクション対策の状態を型で表現できます。

「未エスケープの文字列を、エスケープ済みの文字列を要求する関数に渡した」場合、篩型言語の型検査で拒否 されます。

篩型は、セキュリティに関わる状態の追跡に向いています。

場面６ ── 暗号ライブラリ

F* の HACL*（High-Assurance Cryptographic Library）では、AES、SHA-256、Curve25519、Ed25519、Poly1305 などの暗号プリミティブが篩型と依存型を用いて実装・検証されています。

具体的には、メモリ安全性、機能仕様との整合性、いくつかのアルゴリズムに対する定数時間実行（constant-time execution） などの明示された性質が形式的に検証されています。

HACL* の検証済みコードは、暗号ライブラリや主要なソフトウェア基盤への統合実績を持つと、HACL* プロジェクトが公表しています。

具体的な採用箇所や現在の構成の詳細は、HACL* 公式ドキュメントをご確認ください。

場面７ ── AI エージェントの規則の検証（将来の応用可能性）

これは、先行記事の形式検証記事(定理証明・形式検証はいまから学ぶ価値があるか)でも触れた領域です。

「エージェントがユーザーのメールを読み書きするとき、どんな不変条件を守るか」
$nbsp;
「LLM がツールを呼び出すとき、どんな入力の条件を満たすか」

といった規則を篩型で仕様として書き下す試みが、研究レベルで進みつつあります。

Python エコシステム（langchain、AutoGen、CrewAI）では、この領域で型による安全性の要求が高まりつつあります。

篩型が、この領域の主要ツールの１つとなる可能性がどれくらいあるのかは、今後の展開次第です。

pic_26.jpg

第7.5部 ── 同じ問題を３つの世界で解いてみる ── 表現力と検証の広さ・深さの比較

ここまでの議論を踏まえ、同じ問題を、Python の実行時検証、篩型言語（LiquidHaskell）、依存型言語（Idris 2）の3つの世界で解いてみます。

同じ性質を書こうとしたときに、それぞれの世界で何が起き、何が保証され、何が保証されないのか
── これを具体的に見てみます。

問題１ ── 「長さ n のベクトルと長さ m のベクトルを連結すると、長さ n+m のベクトルになる」

これは、依存型の入門書で必ず登場する古典的な問題です。

Python の実行時検証（annotated-types + beartype）で書いてみる

from typing import Annotated
from beartype import beartype
from beartype.vale import Is

# 長さ n のリストは、Python の型注釈だけでは表現できません
# 実行時に長さを assert することはできます

@beartype
def app_python(xs: list, ys: list) -> list:
    return xs + ys

# 実行時に、長さの性質を assert で表現
def app_python_checked(xs: list, ys: list) -> list:
    result = xs + ys
    assert len(result) == len(xs) + len(ys)  # 実行時にチェック
    return result

Python では、「長さ n のリスト」という型を型システムのレベルで表現できません。
リストの型 list に、長さの情報は含まれていないためです。

beartype の Is[lambda xs: len(xs) == n] のような書き方も可能ですが、n が具体的な数（たとえば 3）ではなく変数として、他のリストの長さと連動するような表現は、Python の型システムの範囲を超えます。

したがって、Python では実行時に assert で長さを確認するしかありません。

しかも、assert は関数の中で書く必要があり、呼び出し側の型としては表現されません。

下流のコードは「連結後のリストの長さが必ず len(xs) + len(ys) である」ことを、型として知ることができません。

篩型言語 LiquidHaskell で書いてみる

【概念説明用のスニペット】

{-@ append :: xs:[a] -> ys:[a] 
             -> {v:[a] | len v = len xs + len ys} @-}
append :: [a] -> [a] -> [a]
append []     ys = ys
append (x:xs) ys = x : append xs ys

LiquidHaskell では、戻り値の型 {v:[a] | len v = len xs + len ys} に、「連結後のリスト v の長さは、xs の長さと ys の長さの和と等しい」 という性質を述語として書き込むことができます。

この性質は、静的検証時に SMT ソルバーが自動で証明します。

実装を間違えて要素を1つ落としてしまうと、SMT ソルバーが「len v = len xs + len ys」を証明できず、LiquidHaskellの検証を通過できません。

Python と決定的に異なるのは、この性質が「戻り値の型」として下流のコードに伝わることです。

append の結果を受け取ったコードは、「このリストの長さは len xs + len ys である」ことを、型を通じて知っています。

依存型言語 Idris 2 で書いてみる

【概念説明用のスニペット】

app : Vect n a -> Vect m a -> Vect (n + m) a
app Nil       ys = ys
app (x :: xs) ys = x :: app xs ys

Idris 2 では、リストの長さそのものを、型の一部として直接扱うことができます。

Vect n a は「要素の型が $a$ で、長さが $n$ のベクトル」という型で、$n$ は型のレベルの自然数です。

app 関数の型 Vect n a -> Vect m a -> Vect (n + m) a は、「長さ n のベクトルと長さ m のベクトルを受け取り、長さ n+m のベクトルを返す」 ことを、そのまま宣言しています。

Idris 2 の型検査器は、この型宣言と実装の一致を、SMT ソルバーの支援なしに、型理論の枠内で直接検査します。

LiquidHaskell がSMTソルバーに証明を委ねるのに対し、Idris 2は型検査器自身が構文的・意味論的に検査します。

３つの世界の対比

観点 Python 実行時検証 LiquidHaskell(篩型) Idris 2(依存型)
長さを型に埋め込む 不可 述語として 型そのものとして
長さ違反の検出タイミング 実行時(assert) 静的検証時(SMT) 静的検証時(型検査器)
下流コードに長さが伝わるか 伝わらない 型を通じて伝わる 型を通じて伝わる
SMT ソルバーへの依存 なし あり(Z3 等) なし(型理論)
述語の複雑化への耐性 実行時なら任意 SMT が解ける範囲 型検査器が判定できる範囲

**要するに、以下のようになります。

  • Python では「実行後に間違いに気付く」
  • LiquidHaskell では「静的検証時に SMT が間違いを検出する」
  • Idris 2 では「型検査そのものが間違いを排除する」

上から順に、保証の性質が段階的に強くなります。**

問題２ ── 「ソートされたリストに要素を挿入すると、結果もソートされている」

これは、篩型の力 が特に鮮明に表れる問題です。

Python の実行時検証で書いてみる

from typing import Annotated
from beartype import beartype
from beartype.vale import Is

def is_sorted(xs: list) -> bool:
    return all(xs[i] <= xs[i+1] for i in range(len(xs) - 1))

# 「ソート済み」を型として表現する試み
SortedList = Annotated[list, Is[lambda xs: is_sorted(xs)]]

@beartype
def insert_python(x: int, xs: SortedList) -> SortedList:
    # 挿入位置を探して、ソート済みを保つように挿入
    for i, y in enumerate(xs):
        if x <= y:
            return xs[:i] + [x] + xs[i:]
    return xs + [x]

Python でも beartype.vale.Is[lambda xs: is_sorted(xs)] を使えば、「ソート済みリスト」という型を、実行時検証の枠内で表現できます。

しかし、これは実行時に is_sorted を全要素チェックすることになり、O(n) のオーバーヘッドが発生します。

また、insert_python の実装が本当にソート性を保っているかは、実行時にたまたま与えられた入力でしか確認できません。

さらに、この関数を呼び出す側の型注釈にも SortedList を書く必要があり、下流の関数が「これはソート済みだ」と信じるためには、全チェーンで実行時検証のオーバーヘッドを払う必要があります。

篩型言語 LiquidHaskell で書いてみる

【概念説明用のスニペット】

{-@ measure isSorted :: [Int] -> Bool
    isSorted []       = True
    isSorted [x]      = True
    isSorted (x:y:xs) = x <= y && isSorted (y:xs)
  @-}

{-@ insert :: x:Int -> {xs:[Int] | isSorted xs} 
            -> {v:[Int] | isSorted v} @-}
insert :: Int -> [Int] -> [Int]
insert x [] = [x]
insert x (y:ys)
  | x <= y    = x : y : ys
  | otherwise = y : insert x ys

*LiquidHaskell では、measure isSorted として「ソート済み」の述語を定義し、insert の型として「ソート済みリストを受け取り、ソート済みリストを返す」ことを宣言します。

静的検証時に、SMT ソルバーがすべての入力パターンについて、insert がソート性を保つことを機械的に証明します。 実装が正しくないと、証明が失敗し、LiquidHaskell の検証を通過できません。

Python と決定的に異なるのは、実行時のオーバーヘッドがゼロであることです。

依存型言語 Idris 2 で書いてみる

Idris 2 でこの問題を扱うと、より深い所まで踏み込むことになります。

【概念説明用のスニペット、簡略化した例】

data SortedList : List Int -> Type where
  SortedNil  : SortedList []
  SortedOne  : (x : Int) -> SortedList [x]
  SortedCons : (x, y : Int) -> (x <= y = True) 
             -> SortedList (y :: ys) -> SortedList (x :: y :: ys)

解説（概念的な骨格のみ、簡略化しています）

Idris 2 では、「ソート済みリスト」そのものを、依存型として定義できます。

SortedList xs は「リスト xs がソート済みであることの証明」を、型として表現しています。

この定義に基づく insert を書くと、実装そのものが「ソート性の証明」を伴います。

しかし、これは Python プログラマの皆様にとってはかなり踏み込んだ内容です。

Idris 2 では「ソート性の証明」を、開発者が型のレベルで構築する必要があります。
SMTソルバーが自動でやってくれる LiquidHaskell とは、開発の負担がかなり異なります。

３つの世界の対比

  • Python の実行時検証
    ── ソート性を assert で確認できる。実行時オーバーヘッドあり。下流に情報が型として伝わらない。
     
  • LiquidHaskell の篩型
    ── ソート性を述語で書き、SMT ソルバーが自動で証明する。実行時オーバーヘッドゼロ。下流に情報が型として伝わる。「SMT ソルバーが解ける範囲の性質」なら、開発者は述語を書くだけでよい。
     
  • Idris 2 の依存型
    ── ソート性を型として表現し、実装そのものが証明を伴う。開発者に「証明を書く」負担が生じる。ただし、SMT ソルバーの限界を超える性質も原理的には表現できる。

問題３ ── 「銀行口座の残高は、いかなる時点でも負にならない」

金融業界に近い問題です。
この問題を通じて、３つの世界の「深さ」の違いをご覧いただきます。

Python の実行時検証で書いてみる

from typing import Annotated
from beartype import beartype
from beartype.vale import Is

NonNegBalance = Annotated[int, Is[lambda b: b >= 0]]

@beartype
def withdraw(balance: NonNegBalance, amount: int) -> NonNegBalance:
    result = balance - amount
    # 実行時、result が負なら BeartypeCallHintReturnViolation で拒否
    return result

これは Python でも書けます。

ただし、呼び出し側が withdraw(balance=100, amount=200) と書いてもコード自体は通り、実行時に初めて例外が発生します。

「引き出そうとしている amount が、balance を超えないこと」を、withdraw を呼び出す前に静的に保証する仕組みは、Python にはありません。

篩型言語 LiquidHaskell で書いてみる

【概念説明用のスニペット】

{-@ withdraw :: b:{Int | b >= 0} 
             -> a:{Int | a >= 0 && a <= b}
             -> {Int | v >= 0} @-}
withdraw :: Int -> Int -> Int
withdraw balance amount = balance - amount

LiquidHaskell では、amount の型に **「a >= 0 かつ a <= b(残高以下)」**という述語を書き込めます。

この関数を呼び出す側は、静的検証時に「引き出そうとしている amount が、balance を超えないこと」を SMT ソルバーで証明する必要があります。

証明できなければ、LiquidHaskell の検証を通過できません。

つまり、「引き出しすぎ」というバグは、実行前に必ず検出されます。
実行時に初めて気付くことはありません。

依存型言語 Idris 2 で書いてみる

Idris 2 でも、同様の性質を型として表現できます。

しかし、この問題では、篩型のLiquidHaskellと依存型のIdris 2の間に、表現の広さの違いはあまり出ません。

というのも、この問題で必要な述語は「整数の比較と算術」に収まるため、SMT ソルバーが得意な領域であり、LiquidHaskell の自動証明でも十分に扱えるためです。

Idris 2 の依存型が真価を発揮するのは、SMTソルバーが扱いにくい「複雑な帰納構造」「高階の量化」「複雑な代数的性質」を扱う場面です。

pic_27.jpg

３つの世界の対比

問題３は、「SMT ソルバーが得意な領域」の範囲内で解ける問題の代表例です。

  • Python
    ── 実行時に例外で拒否できるが、静的な保証は与えられない。呼び出し側は「引き出しすぎ」のコードをそのまま書けてしまう。

  • LiquidHaskell
    ── 「amount <= balance」を型に述語として書き込み、SMT ソルバーが静的に証明する。呼び出し側は、この条件を満たさないコードを書くこと自体が拒否される。

  • Idris 2
    ── 依存型で表現することもできるが、この問題では LiquidHaskell の SMT ソルバー自動証明の便利さが上回る。

この対比から学べること。

すべての問題で「依存型が最強」ではありません。

問題の性質次第では、篩型とSMTソルバーの組み合わせが依存型より実装しやすく、開発負担も軽いという場面が実務では多く存在します。

pic_28.jpg

３つの世界の使い分けの結論

３つの問題例を通じて確認できた結論は以下です。

Python の実行時検証（annotated-types、beartype、Pydantic）
値の制約を型注釈に書き、実行時に自動検証させる仕組み。

書きやすさと導入容易性が最大の強み。

  • 実行時オーバーヘッドを許容できる場面
  • 外部からの入力を検証する場面
  • 既存のPython資産を活かす場面

で最適です。

しかし、下流のコードに「検証済みの情報」を型として伝えることは、限定的です。

篩型言語（LiquidHaskell、F、Typed Racket の refinement 機能）*

述語を型システムに組み込み、SMT ソルバーの支援で静的に検証する仕組み。

「値の範囲、比較、リストの長さ、整列性、単純な代数的関係」など、SMT ソルバーが得意な範囲では、Python では実現できない静的保証を提供します。

実行時オーバーヘッドはゼロ、下流のコードに情報が型として伝わります。

依存型言語（Idris 2、Agda、Lean 4、Rocq）

値の情報を型に直接埋め込み、型理論の枠内で検査する仕組み。

  • 「複雑な帰納構造」
  • 「高階の量化」
  • 「数学的な定理の証明」

など、SMT ソルバーの限界を超える性質も原理的には表現可能です。

ただし、開発者に「証明を書く」負担が生じます。

数学の形式化、暗号や OS カーネルの形式検証、AI エージェントの完全な規則検証で必要になります。

結論

Python の型ヒントから、篩型、依存型へと進むにつれ、「値の性質を型で保証する力」が段階的に強くなっていきます。

その一方で、開発の負担と、必要な処理系の学習コストも、段階的に増していきます。

どの水準の保証が必要とされるかは業務の性質次第

金融、暗号、医療、航空、AI エージェントの完全検証、数学の形式化
── これらの領域では、Python の実行時検証を超える保証が必要になります。

それ以外の多くの領域では、Python + Pydantic + beartype で十分な場合が多いです。

pic_29.png

本節のコード例と参考文献

  • 問題１（ベクトル連結)のコード例は、Idris 2 公式ドキュメントの Vect 定義、LiquidHaskell 公式チュートリアル(Programming with Refinement Types）の append 例とPython + beartype/annotated-types の公式ドキュメントを参照して作成しました。
     
  • 問題２（ソート済みリスト）のコード例は、Ranjit Jhala, Niki Vazou, Refinement Types: A Tutorial(arXiv 2020)の insert 例とIdris 2 公式ドキュメントのソート関連の型定義を参照しました。
     
  • 問題３（銀行口座の残高）は、Yaron Minsky, Anil Madhavapeddy, Jason Hickey, Real World OCaml の金融ドメイン向けの型設計とF* 公式チュートリアルの Hoare 論理風検証の例を参照しました。

いずれも実際に動作させる際は、各言語処理系の環境構築とバージョンに応じた微修正が必要になる場合があります。

第8部 ── Python の型ヒントとの関係

Pythonエンジニアの皆様が、日々使っている型ヒント。
Pythonの型ヒントと篩型はどうつながるのでしょうか。

まず、Python の実行時バリデーション（Pydantic、beartype、annotated-types）と、篩型言語の refinement type は、思想は近くとも、検査の仕組みと保証の性質が異なります。

そのことを、次の比較表で整理します。

比較表 ── Python の実行時バリデーションと、篩型言語の refinement types

観点 Python + Pydantic / beartype / annotated-types Refinement Type Language(LiquidHaskell、F* 等)
条件を型に表現する できる できる
入力値の検査タイミング 関数呼び出し時(実行時) 静的検証時(コンパイル前あるいは型検査フェーズ)
SMT ソルバーによる自動証明 通常しない する処理系がある(Z3 等)
述語の含意の推論 限定的(実行時の値ベース) 型システムと検証器が静的に行う
戻り値の性質を下流のコードで利用 通常は追跡されない 型として追跡される
証明責任の所在 開発者と実行時ライブラリ コンパイラ・SMT ソルバー
型検査の成功が示すもの 型構造の整合性 プログラムの正しさに関する形式的な保証(処理系による)
外部入力への対応 強い(Pydantic の主要用途) 別途パース・検証が必要
既存 Python への導入 容易(pip install で即座) 別言語の学習・処理系導入が必要

要するに、Python の実行時バリデーションは「述語を実行時にチェックする」仕組みです。

篩型言語は、「述語を型システムの一部として静的な型検査に組み込む」仕組みです。

「検査タイミングの違い」 は、両者の違いの中で最も分かりやすい部分ですが、実際にはそれ以上の質的な違い があります。

Curry-Howard 対応との関係

「Curry-Howard 対応」は、この違いの背景にある根本的な考え方です。

「型」を「定理(証明すべき条件)」とみなし、プログラムを「その証明」とみなすカリー・ハワード同型対応の発想** に立てば、篩型言語における型検査は、そのまま「述語が満たされることの証明を構築する作業」になります。

SMT ソルバーが述語 v > 0 を自動で証明できるとき、それは Curry-Howard 対応の意味で、「v > 0 という命題に対する証明を、機械が自動で構築した」ことに他なりません。

Pythonの実行時バリデーションでは、この「証明の構築」は行われません。
「実行時に、その値が述語を満たしているかを検査する」だけです。

pic_31.png

この違い が、比較表の各行に現れてきます
この点を踏まえたうえで、Python側の各機能を見ていきます。

Python の typing.Annotatedの発想は篩型に近い

Python 3.9 以降、typing.Annotated という記法があります。

from typing import Annotated
from pydantic import Field

PositiveInt = Annotated[int, Field(gt=0)]

これは、「int に、追加のメタデータ（$gt=0$、つまり $> 0$）を付与した型」です。

篩型の {v:int | v > 0} と、書き方の発想は近いです。

ただし、Python では、この検査は主に 実行時に 行われ、Python 標準の型検査器(mypy、pyright)は原則としてこのメタデータの意味論を検証しません。

Pydantic の PositiveInt、EmailStr、conint

Pydantic には、こうした「条件付きの型」が最初から用意されています。

  • PositiveInt(正の整数)
  • NonNegativeInt(非負の整数)
  • EmailStr(メールアドレス形式)
  • conint(gt=0, lt=100)(0より大、100未満の整数)

これらは、篩型の記述の発想を、Python の実行時バリデーションに取り入れたもの、とご理解いただけます。

篩型言語と Pydantic の違いは、上の比較表に整理したとおり、検査タイミングだけではなく、証明責任と保証の性質にまで及びます。

実務の指針 ── Python エンジニアが、今日から取り組めること

Python エンジニアの皆様は、次の順序で、篩型的な発想を実務に取り入れられます。

ステップ1(今日から)。 次章「Python における篩型ライブラリの現状」でご紹介する annotated-types と beartype を、業務コードに導入する。

ステップ2(1〜2ヶ月)。 LiquidHaskell か F* を、週末プロジェクトで触ってみる(篩型の実際の書き方を体験)。

ステップ3(必要が生じたら)。 業務の重要コンポーネント(認証、決済、暗号処理)を、F* で書き直すことを検討する。

「Python から離れずに、篩型的な発想の大部分を取り入れる」ことは、既に十分可能です。 詳しくは次章で。

第９部 ── Python における篩型ライブラリの現状

皆様は以下の疑問を抱かれるかもしれません。

「関数型言語に行かなくても、Python でも篩型ができるライブラリはないのか?」

「純粋な篩型言語」ほどの完全性はありませんが、篩型の大部分の実用効果をPythonで得られるライブラリは、すでに複数、実用段階で存在します。

公式ドキュメント、PyPI、GitHub、Python 公式の Discussion、mypy Issue、arXiv 論文を実読して確認できた内容をご報告します。

現状１ ── Python 標準の typing.Annotated(PEP-593)が、篩型の入口

Python 3.9(2020年)で正式導入された typing.Annotated が、Python における篩型の基盤です。

PEP-593 は、「型 T に、追加のメタデータ x を付与する」記法 Annotated[T, x] を導入しました。

型検査器(mypy、pyright)は、原則としてメタデータ x を無視し、T として型検査します。しかし、ランタイムのツールやライブラリは、__metadata__ 属性で x を取り出し、実行時に検査に使えます。

これが、Python の篩型ライブラリすべての共通基盤です。

現状２ ── annotated-types ライブラリ（共通の制約メタデータ標準）

「Python における篩型メタデータの、事実上の共通標準」の位置にあるライブラリです。

Pydantic に依存しません。

Pydantic、msgspec、cattrs、他の複数のバリデーションライブラリが、annotated-types を共通の入力として受け入れる設計になっています。

MIT ライセンス、pure Python、依存関係なし。

Pydantic 公式ドキュメントは、annotated-types を使えば「Pydantic-agnostic に(Pydantic に依存しない形で)制約を書ける」と明示的に推奨しています。Python の型注釈エコシステム全体で共有される、共通基盤の位置にあります。

from typing import Annotated
from annotated_types import Gt, Lt, Len, MultipleOf, Predicate

# 18 より大きい整数
Age = Annotated[int, Gt(18)]

# 長さが 1 以上 100 以下の文字列
UserName = Annotated[str, Len(1, 100)]

# 素数の整数リスト。 任意の Python 関数を述語として使える
def is_prime(n: int) -> bool:
    ...
PrimeInt = Annotated[int, Predicate(is_prime)]

Predicate(is_prime) の部分に注目してください。

「任意の Python 関数を、型に添える述語として使える」 ── これが、F* の {v:int | is_prime v} や LiquidHaskell の {v:Int | isPrime v} に、思想として非常に近い記法です。

annotated-types が提供する制約は、Gt、Ge、Lt、Le(比較)、MultipleOf(倍数)、Interval(範囲)、Len、MinLen、MaxLen(長さ)、Timezone、Predicate(任意の述語)などです。

現状３ ── beartype の beartype.vale.Is ── ラムダでその場に述語を書ける

Python の runtime type checker として、O(1) の実行時型検査を保証する pure-Python ライブラリです。

特筆すべきは、beartype.vale モジュールが提供する「バリデータ DSL」です。

awesome-python-typing に「Unbearably fast O(1) runtime type-checking in pure Python」として筆頭格で紹介されています。

Python 3.13(2024年、PEP 747 の TypeForm 導入)以降の型システム進化にも追随しています。

具体例（公式ドキュメントより）を示します。

from beartype import beartype
from beartype.vale import Is
from typing import Annotated

# ラムダで、その場に述語を書ける
PositiveInt = Annotated[int, Is[lambda x: x >= 0]]
NonEmptyStr = Annotated[str, Is[lambda s: len(s) > 0]]

# バリデータの合成(かつ、または、否定)も可能
BoundedInt = Annotated[int, Is[lambda x: x >= 0] & Is[lambda x: x < 100]]

@beartype
def process_age(age: PositiveInt):
    return age

process_age(25)   # OK
process_age(-1)   # BeartypeCallHintParamViolation(実行時に例外)

この記法は、篩型言語 LiquidHaskell の {v:Int | v >= 0} と、書き方の表面では類似しています。

ただし、両者の性質は異なります。LiquidHaskell は述語を型システムに組み込み、SMT ソルバーの支援を受けて静的に検証します。一方、beartype はランタイム型チェックとして、関数呼び出し時にラムダを評価します。両者を分ける詳しい違いは、第8部の比較表をご参照ください。

&(かつ)、|(または)、~(否定)による述語の合成は、篩型言語における述語の論理演算に相当する構造を、Python 上で表現するものです。

 

現状４ ── Pydantic の Field(...) と AfterValidator

Python における実行時データバリデーションの、事実上の標準ライブラリです。
Field による制約と AfterValidator による任意関数の適用で、篩型的な発想を業務コードに導入できます。

Pydantic V2 のパフォーマンス特性

Pydantic V2 では、バリデーションの中核部分が pydantic-core として Rust で書き直され、Python 側は薄いラッパーとして動作しています。

これにより、V1 に比べて数倍から十数倍の高速化が実現されました。

しかし、これが本記事の文脈で意味することは、単なる高速化ではありません。

Pydantic V2 は、Rust による極めて高速な実行時検証を実現していますが、それでも「実行時」に検査を行う仕組みであることには変わりありません。

「コンパイル前に静的検証を終える」篩型言語（F、LiquidHaskell）とは、依然として異なるパラダイムに立ちます。*

「Rust による超高速な実行時検証」も、「静的型検査時の SMT 証明」も、それぞれ異なる工学的な選択です。

Pythonプログラマの皆様が、Pydantic V2 で「速い実行時検査」の恩恵をすでに受けています。
しかしそれは静的検証とは別物です。

この対比を明確にご理解いただくことが、本記事の重要なポイントです。

FastAPI、LangChain、AutoGen、CrewAI など、Python の主要な AI/Web フレームワークが Pydantic を採用しています。**「Python プログラマの多くが、値の制約を型注釈に近い形で書く発想を、日常業務に取り込んでいる」**と言える状況です。

具体例（Pydantic 公式ドキュメントより）を示します。

from typing import Annotated
from pydantic import Field, TypeAdapter, ValidationError

# Pydantic の Field 構文
PositiveInt = Annotated[int, Field(gt=0)]

# annotated-types の Gt を使った Pydantic-agnostic な書き方
from annotated_types import Gt
PositiveInt = Annotated[int, Gt(0)]

ta = TypeAdapter(PositiveInt)
ta.validate_python(1)    # OK(pydantic-core の Rust コードが高速に検証)
ta.validate_python(-1)   # ValidationError(実行時の値ベースの検査結果)

現状５ ── FLAT-PY（2025年、学術研究段階）── Python 用の「本格的な」篩型テストフレームワーク

  • 論文（arXiv、2025年1月20日投稿）
    Fengmin Zhu, Andreas Zeller「FLAT: Formal Languages as Types」
    CISPA Helmholtz Center for Information Security（ドイツ）
    https://arxiv.org/abs/2501.11501
     
    Fengmin Zhu、Andreas Zeller の両氏（CISPA Helmholtz Center for Information Security、ドイツ）による2025年の学術研究で提案されたPython 用の篩型テストフレームワークです。

refine(base, predicate) という構文で {x:t | e} を表現し、AST 変換で必要な型 assertion を自動注入します。

メール、URL、JSON のような形式言語（formal language）を型として扱える点が独自です。

具体例を論文から引用して示します。
 
【概念説明用のスニペット】

def refine(base: type, predicate: Any) -> RefinementType
def lang(name: str, rules: str) -> LangType

# 整数の算術式のような形式言語を型として定義
IntExp = lang('IntExp', """
    start: (number op)* number;
    number: [0-9]+;
    op: "+" | "-";
""")

（コードの出典）

  • Fengmin Zhu, Andreas Zeller ,FLAT: Formal Languages as Types（arXiv preprint arXiv:2501.11501, 2025年1月20日投稿）
    CISPA Helmholtz Center for Information Security（ドイツ）による、Python 用の形式言語ベースの型テストフレームワーク FLAT-PY の学術論文。文脈自由文法（CFG）を型として扱う発想を、Python の実行時型検査に持ち込む研究です。
    https://arxiv.org/abs/2501.11501
     
  • 拡張版（2026年 ACM 公式出版）── ACM Transactions on Software Engineering and Methodology
    https://dl.acm.org/doi/10.1145/3799978

2025年発表の学術研究段階であり、まだ広く実用に供されているものではありません。

しかし、「Python に本格的な篩型を持ち込む試みが、学界レベルで進行中」であることを示す重要な事例です。

現状６ ── typing.TypeIs(PEP 742、Python 3.13)── 篩型そのものではないが、関連する「型絞り込み」の仕組み

Python 3.13(2024年)で導入された、「型絞り込み(type narrowing)」用の仕組みです。

これは篩型そのものではありません。

ある関数が「引数が特定の型に属するかを判定する型述語（type predicate）」として振る舞うことを、型検査器に伝える仕組みです。

コード例を示します。

from typing import TypeIs

def is_int(x: object) -> TypeIs[int]:
    return isinstance(x, int)

def process(x: object):
    if is_int(x):
        # ここでは x は int として型検査器に扱われる(型絞り込み)
        return x * 2
    return 0

注意点。

TypeIs が扱うのは「x は int か」といった 型集合の絞り込み であって、「x は int かつ x > 0 か」といった 値の述語の型検査 ではありません。

つまり、TypeIs は篩型 {v:int | v > 0} を Python に持ち込むものではなく、篩型の「値の述語」の側面よりも、既存の型を静的に狭める側面に対応します。

Python 標準ライブラリに正式導入された、比較的新しい仕組みです。

Python 型システムに「述語関数による型絞り込み」の考え方が公式に採用された注目すべき進展です。

ただし、これを「Python における篩型の導入」と表現するのは正確ではないため、本記事では「篩型に関連する型絞り込み機能」として位置付けます。

現状７ ── mypy Issue #560 ── 本格的な篩型の Python 導入は、まだ議論段階

2015年1月に提起された、mypy に本格的な篩型 Refine[C, f] を導入する提案です。
「needs discussion」ラベルのまま10年以上議論が続いており、公式には未実装のままです。

なぜ実装されないのか。

提案者自身が言及しているとおり、静的検証時に述語 f の妥当性を機械的に検証するには、SMT ソルバーの統合など、mypy の設計思想を超える機能が必要になります。

Python の動的型付けの文化と、静的検証時の SMT 検証の哲学は根本的に相性が悪いのです。
そのため、Python における本格的な篩型の静的検証時 SMT 検証は、当面、実現の見込みが立っていません。

pic_30.png

現状８ ── Python.org Discussion「篩型の仕様の明確化」(2024年)

2024年に Python.org で開始された「Python 型システム内の篩型（Literal、LiteralStr など）の仕様を、より明確にすべきではないか」という公式ディスカッションがあります。

Pythonの型システムの中に、すでに篩型的な機能（Literal、LiteralStr など）が存在しており、それらを体系的に整理する必要が認識されつつあります。

現状の総合評価 ── Python プログラマは得たもの、まだ得ていないもの

以上を踏まえた総合的な整理をご報告します。

Python プログラマが、いま既に得ているもの。

  • typing.Annotated + annotated-types + beartype の組み合わせで、篩型言語で表現される述語のうち、単純な範囲・比較・長さ・任意の実行時判定関数といった広い範囲は、実行時検査として書ける

  • Pydantic で、入力データバリデーションを、篩型の記述に近い記法で書ける

  • TypeIs により、型絞り込みが公式に型検査器に理解される

  • ラムダによる述語、任意の Python 関数による述語、述語の論理合成(かつ、または、否定)、いずれも表現可能

Python プログラマが、まだ得ていないもの。

  • 静的な型検査時に、SMT ソルバーによる自動証明を行う仕組み(LiquidHaskell、F* の核心的な機能)

  • 依存型に基づく、値の情報を型のレベルで体系的に追跡する仕組み(Idris 2 の Vect 型のように、実装間違いを型検査時に排除する機能)

  • 形式検証されたコードの、他言語への抽出(F* から C や OCaml への抽出、HACL* のような産業レベルの暗号ライブラリ検証)

  • 証明の再利用と、証明の合成(定理証明支援系のように、証明を他の証明の中で使う仕組み)

それゆえに、Racket や Idris 2、Lean 4、F* を学ぶ価値がある

Python の annotated-types + beartype + Pydantic は、実務レベルで有効です。

多くの Python プログラマにとって、日常業務における値の制約違反の相当部分は、これらのライブラリで実行時に自動検出できるようになります。

しかし、これらは実行時の関数呼び出し段階でのチェックであり、静的な保証にはなりません。

そして、次のような場面では、Python の実行時ライブラリでは原理的に届かない領域が存在します。

 

  • 金融・暗号・医療・航空など、「実行して初めてバグが分かる」ことが許されない分野

  • AI エージェントの規則を、実行前に静的に検証したい場面

  • 数学の定理を、機械で厳密に証明したい場面

  • OS カーネル、コンパイラ、ネットワークスタックのような、「実行時のオーバーヘッドが厳しく制限される基盤層」

これらの領域では、型検査時に静的な検証を行う篩型言語(F、LiquidHaskell)や、依存型言語(Idris 2、Lean 4、Rocq、Agda)* が必要になります。

Python で実用上の制約検証を行い、より強い保証が必要な部分だけを、Racket、Idris 2、F などの形式検証の対象にする ── これが、皆様が採り得る現実的なアプローチです。*

先行記事(定理証明・形式検証はいまから学ぶ価値があるか)で、また今後公開予定の学習ロードマップ地図の記事で、こうした言語を学ぶ経路をご紹介する予定です。

**第９部の主要参考文献。

  • PEP 593 Flexible function and variable annotations (Till Varoquaux, Konstantin Kashin ら、2019年)
    typing.Annotated の言語仕様。本節の基盤となる Python 標準仕様。
    https://peps.python.org/pep-0593/
     
  • PEP 742Narrowing types with TypeIs (Jelle Zijlstra、2024年)
    Python 3.13 で導入された TypeIs の言語仕様。
    https://peps.python.org/pep-0742/
     
  • annotated-types ライブラリ公式リポジトリ(Samuel Colvin ら、MIT License)
    Pydantic に依存しない制約メタデータの共通標準ライブラリ。
    https://github.com/annotated-types/annotated-types
     
  • beartype 公式ドキュメント(Cecil Curry ら、MIT License)
    Python の O(1) 実行時型検査ライブラリ。beartype.vale バリデータ DSL を含む。
    https://beartype.readthedocs.io/
     
  • Pydantic V2 と pydantic-core(Samuel Colvin ら、MIT License)
    Rust で書かれた pydantic-core の公式リポジトリ。Pydantic V2 のパフォーマンス特性を裏付ける。
    https://github.com/pydantic/pydantic-core
     
  • Marco Vassena, Peter Buitelaar 他 FLAT: Formal Languages as Types (arXiv preprint arXiv:2501.11501、2025年)
    Python 用の篩型テストフレームワーク FLAT-PY の学術論文。
    https://arxiv.org/abs/2501.11501
     
  • κeen「静的型付け言語のパラメータ多相の話」
    Python プログラマ向けに、篩型と依存型の違いを分かりやすく解説した日本語記事。「篩型は既存の言語に後付けできる」という重要な指摘を含む。
    https://zenn.dev/blackenedgold/articles/e06dadc4c3921f
     
  • mypy Issue #560 Request: allow refinement types (Jukka Lehtosalo 他、2015年提起、議論継続中)
    mypy に本格的な篩型を導入する提案。10年以上議論が続いている。
    https://github.com/python/mypy/issues/560

第１０部 ── 学び始めるための最短経路

篩型を、皆様が実際にご自身の手で試すための、最短経路をご提示します。

経路A ── LiquidHaskell から入る（Haskell の経験がある皆様）

もし、皆様が Haskell を少しでもご経験でしたら、LiquidHaskell が最短です。

Haskell の既存のコードに、{-@ ... @-} 注釈を追加していくだけで、篩型が始められます。

経路B ── F* から入る（篩型と依存型を両方見たい皆様）

F* は、篩型と依存型の両方を持つので、「篩型ってどんなもの?」を最初から幅広く体験できます。

「実世界の暗号ライブラリで使われている実力」を、皆様が直接体感できます。

経路C ── Typed Racket の refinement 機能から入る（Lisp/Scheme の経験がある皆様）

もし、皆様が Lisp や Scheme をご経験でしたら、Typed Racket の refinement/dependent typing 機能が親しみやすいでしょう。

 

経路D ── まず Python の Pydantic で「篩型的な発想」に慣れる

Haskell も Racket も触ったことがない、という皆様には、まず Python の Pydantic で、篩型的な発想に慣れることをお勧めします。

PositiveInt、conint、Annotated を日常的に使うことで、「値の条件を型に書く」感覚が身につきます。

その後、LiquidHaskell か F* に進めば、「実行時ではなく静的検証時に検証される」ことの威力が、身体で分かります。

第１１部 ── よくある疑問

Python エンジニアの皆様が、この記事を読まれて抱かれるであろう疑問に、まとめてお答えします。

疑問１ ── SMT ソルバーが自動で全部やってくれるなら、なぜ皆使わないのか

SMT ソルバーには限界があります。

線形演算、比較、リストの長さ、集合演算は得意です。

しかし、再帰的な関数や、複雑な帰納構造、非線形演算(乗算、指数、対数)は苦手です。

そのため、篩型で書ける述語には実践上の制約があります。
「なんでも書ける」わけではありません。

疑問２ ── 篩型を書くのに、どのくらいの学習コストがかかるか

Python の型ヒントを書いている皆様なら、篩型の基本(値の条件を書く)は、1週間で慣れます。

ただし、「証明できる述語」と「証明できない述語」の勘所を掴むには、1〜2ヶ月かかります。

「まず書いてみて、検証に失敗したら、述語を単純化する」というサイクルを繰り返すのが、実践的な習得法です。

疑問３ ── Python に篩型を導入する動きはないのか

部分的にはあります。

Pydantic の実行時検査、typing.Annotated、mypy の高度な型機能などが、篩型的な発想を Python に持ち込む試みです。

しかし、静的検証時に SMT ソルバーで検証する本格的な篩型を Python に入れるプロジェクトは、まだ広く普及していません。

Python の動的型付けの文化と、静的検証時 SMT 検証の哲学は、根本的に相性が悪いためです。

そのため、篩型の実力を体験するには、篩型を持つ言語（LiquidHaskell、F* など）に触れるのが早道です。

疑問４ ── 篩型と依存型、初学者はどちらから始めるべきか

Python エンジニアの皆様には、まず篩型から使い始めることをお勧めします。

理由は３つあります。

  • 篩型のほうが、Python の型ヒントからの発想の延長線に近い
     
  • 篩型のほうが、SMTソルバーの自動証明で楽できる
     
  • 篩型のほうが、既存のPython資産を活かしやすい（Pydantic、mypy との接続）

依存型は、篩型の限界を感じてから、次のステップとして学ぶのが自然です。

第12部 ── エピローグ 研究の最前線 ── 篩型で「バグの実在」を保証する新しい方向

ここまで見てきた篩型は、いずれも「安全性(safety)」を保証する仕組みでした。

「この関数はゼロ除算を起こさない」

「このリストは常に整列している」

「この暗号ライブラリはメモリ安全である」

いずれも、「バグがない」ことを保証するものです。

ところが、篩型システムは、いま逆方向にも研究が進みつつあります。

京都大学 五十嵐研究室の研究 ── 到達可能性を検証する篩型システム

佐藤聡太、松下祐介、末永幸平、五十嵐淳「関数型言語の到達可能性を検証する篩型システム」(PPL 2026)

 

位置付け。

京都大学大学院情報学研究科の五十嵐研究室で進められている、篩型システムの新しい方向性を示す研究です。

従来の篩型システム(F*、LiquidHaskell、Typed Racket など)は「安全性 ── バグがない」を保証しますが、この研究は「到達可能性 ── バグが実在する」を保証する篩型システムを提案しています。

背景と意義。

この研究は、Peter W. O'Hearn による Incorrectness Logic(2019年、手続き型言語向け)の発想を、関数型言語に篩型として持ち込むものです。

「型検査に成功すること」が、「バグが実在すること」を保証する ── 従来と逆の発想の型システム、とご理解いただけます。

なぜこれが重要かというと、バグ発見のためのテスト、ファジング、シンボリック実行といった技術と、篩型システムを橋渡しする可能性があるからです。

「あるプログラムに、この入力を与えると、確実に不正な状態に到達する」ことを、型で証明できる ── これは、セキュリティ研究や品質保証の分野に、新しい理論的基盤を提供する可能性を持ちます。

篩型は、Python プログラマの日常業務に取り入れられる実用ツールでありながら、同時に、いまも学術的な発展が続いている生きた研究分野です。

##第１２部の主要参考文献。

  • 佐藤聡太、松下祐介、末永幸平、五十嵐淳「関数型言語の到達可能性を検証する篩型システム」(日本ソフトウェア科学会 第28回プログラミングおよびプログラミング言語ワークショップ PPL 2026 ポスター、京都大学 五十嵐研究室)

従来の「安全性」を保証する篩型システムから、「到達可能性」を保証する新しい方向への研究提案。
https://www.fos.kuis.kyoto-u.ac.jp/pdf/posters/satos.ppl2026.pdf
 

  • Peter W. O'Hearn「Incorrectness Logic」(Proceedings of the ACM on Programming Languages, POPL 2020)
    京大の研究の理論的背景。手続き型言語における「バグの存在の証明」の論理体系。
    https://dl.acm.org/doi/10.1145/3371078

６つの技術の一覧比較

長い記事を最後までお読みいただきありがとうございます。

ここに、本記事で扱った6つの技術を、5つの観点で比較する1枚の結論表をお示しします。

この表を頭の中の地図として持ち帰っていただければ、皆様が実務や学習の場面で「今どこにいて、次にどこへ進めるか」が見えてくるはずです。

技術 条件を表す場所 検証時期 自動証明 値の型レベル追跡
Python + Pydantic 実行時バリデーション(pydantic-core が Rust 実装で高速) 実行時 なし 限定的
Python + beartype 実行時型検査(ラムダで述語を書ける) 実行時 なし 限定的
Python + annotated-types 型注釈メタデータ(Pydantic-agnostic な共通基盤) 実行時(ライブラリに依存) なし 限定的
LiquidHaskell refinement predicate(Haskell に GHC プラグインで後付け) 静的検証時 SMT ソルバー(Z3) あり
F* refinement + dependent type + effect + termination 静的検証時 SMT ソルバー + 明示的な証明 強い
Idris 2 dependent type(値を型に直接埋め込む) 静的型検査時 型検査器自身が判定 非常に強い
Lean 4 / Rocq / Agda 命題と証明(Curry-Howard 対応) 静的型検査時 支援あり(タクティク・戦術) 非常に強い

この表の読み方

上の行から下の行へ進むにつれ、「値の性質を型で保証する力」が段階的に強くなっていきます。

同時に、開発の負担、必要な処理系の学習コスト、コミュニティのサイズと成熟度も段階的に変化します。

  • Python の実行時ライブラリは、pip install で今日から使えます。Python 資産をそのまま活かせます。
     
  • LiquidHaskell、F、Idris 2* は、それぞれ別の言語処理系の学習が必要ですが、静的な保証が得られます。
  •  
  • Lean 4、Rocq、Agda は、数学の定理の形式化や、産業レベルの高信頼ソフトウェアの検証に向いています。

皆様がどの水準の保証を必要とするかは、業務の性質次第です。

金融、暗号、医療、航空、AI エージェントの完全検証、数学の形式化
── これらの領域では、上の表の下側の技術が必要になります。

それ以外の多くの領域では、Python + Pydantic + beartype で十分な場合が多いです。

pic_33.png

本記事の冒頭の全体地図と、この結論表を、皆様の頭の中の地図としてお持ち帰りください。

おわりに ── 篩は、値をふるいにかけ、正しさを残す

篩型という名前は、古代からの「ふるい」の道具の発想を、型システムに持ち込んだものです。

値の海の中から、条件を満たすものだけを、機械が選り分けてくれる。

Python エンジニアの皆様が日々使っている型ヒントは、その延長線上に、静的な型検査の段階で条件を検証する世界を持っています。

その世界の入口が、LiquidHaskell、F*、Typed Racket の refinement 機能、そして京都大学で研究されている新しい方向性の篩型システムです。

皆様が今日から annotated-types、beartype、Pydantic で「値の条件を型に書く」ことを始めれば、篩型の考え方の入口には、すでに立たれています。

その先には、型検査時に機械が静的に検証してくれる世界が開かれています。

入口となる公式資料は、いずれも無料で公開されています。

最初の篩を皆様のコードに組み込んでみてください。

pic_32.jpg

参考 ── ブックマークにお勧めの主要ハブ

以下は、皆様がブックマークに登録しておくと便利な、主要ハブへのリンクをまとめたものです。

LiquidHaskellのハブ

F* のハブ

Typed Racket の refinement機能のハブ

篩型の主要学術文献 ── 本記事執筆にあたって参照した論文

Python 篩型ライブラリの公式ドキュメント

先行記事および今後の関連記事

出典についての注記。

本記事の教材の記述は、記事本文中に掲載した各書籍・サイトの公式ページの情報に基づいています。
各教材の最新バージョンや、内容の細部は変化しますので、正確な情報は公式サイトでご確認ください。

篩型・依存型の分野は日進月歩で発展しており、本記事で紹介した経路が唯一の正解ではありません。

皆様がご自身の関心に応じて、自由に経路を組み替えていただけるように、記事本文の各解説段落で、教材ごとの位置付けと評判を丁寧に記述しました。

1
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
1
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?