述語付き部分型は、述語の検査をどこで払うかで分かれる

解釈 出典: Ada Reference Manual 3.2、SPARK 2014 Rationale: Type Predicates、PVS、Lean Language Reference: Subtypesほか(根拠の確度を参照) 2026-11-07 作成

Adaのsubtypeは「型 + 値の制約」で、新しい型を作らない。

subtype Digit is Integer range 0 .. 9;

DigitとIntegerは同じ型なので自由に混ぜて書け、Digitの変数への代入や引数渡しの時点で範囲を検査し、外れていればConstraint_Errorを上げる。規格の定義は「型の部分型は、その型と、その型の値への制約の組である」で、部分型の値は制約を満たす型の値である。

これは篩型{x: Integer | 0 ≤ x ≤ 9}そのもので、Ada固有のものではない。同じ形の型を持つ言語は多い。違いは「この値は述語を満たすか」という義務を、誰が、いつ払うかにある。

Adaのsubtypeは、Pascalの部分範囲型への批判から出てきた

値の範囲で絞った型そのものはAdaより前にある。Pascal(Wirth 1971)の部分範囲型0..9がそれで、Adaのrange制約と中身は同じである。

ただしPascalでは、部分範囲を型として扱ったことが問題にされた。Habermann (1973)は、Pascalの問題は主に範囲・型・構造の混同から来ていると批判し、Welsh, Sneeringer, Hoare (1977)もPascalの曖昧さと危うさを列挙している。

Adaの設計理由書(Ada 83 Rationale §4.1)は、この批判を名指しで受けている。

Several difficulties in the types of Pascal that have been noted by Habermann and others [Hab 73, WSH 77] are overcome in Ada by the notion of subtype.

— Ada 83 Rationale §4.1

Adaがやったのは、静的な性質と動的な性質を2つの概念に分けたことである。型は値の集合と、適用できる演算などの静的な性質を持つ。部分型は型に制約を足したもので、制約を満たすかは一般に動的に検査する。名前を付けた部分型は「型名 + 制約」の略記にすぎないので、新しい型は作らない。つまりAdaの新しさは範囲で絞ることではなく、絞った結果を型と呼ばないと決めたことにある。

Ada 83の時点ではこの区別もまだ曖昧で、「型は部分型でもあった」。Ada 95で整理し直されている(Ada 95 Rationale)。

同じ理由書の§4.4(Constraints and Subtypes)は、制約の違反は原則として実行時にCONSTRAINT_ERRORで報告すると書いたうえで、コンパイラは一部の違反をコンパイル時に報告でき、前の検査で成功が保証された検査は省けるとしている。例でも代入ごとに「static check」「dynamic check」を書き分けている。静的に決まる分は静的に、残りを実行時にという分け方は、2006年のhybrid type checkingの20年前、1986年版の設計理由書に既にある(判定できない部分型は、拒否も受理もせず実行時の検査に回す)。違いは、Adaが静的に分かった違反を不正なプログラムにはせず、報告にとどめることである。

一般的な部分型との違い

型理論やオブジェクト指向でいう部分型(S <: T)は、別の型だが、Tが要る所でSの値を使ってよいという関係である。Adaのsubtypeは同じ型の値を絞ったもので、同じ語でも中身が違う。

違いが一番はっきり出るのは向きである。一般的な部分型は「Tが要る所にSを渡す」一方向だけを静的に許す。Adaの部分型どうしは型検査の上では同じ型なので、両方向とも書けて、狭くなる方向だけを代入の時点で実行時に検査する。

演算の結果が基の型になるので、部分型は演算について閉じていない。Naturalどうしの引き算は負になりうるIntegerで、Naturalの変数に入れる時点で初めて検査される(Ada 83 Rationale §5.2)。

書き込みも違いが出る所である。Naturalの変数はIntegerの変数の代わりにならない。負の値を書き込めないからである。型理論では、読みも書きもできる参照の部分型は、読む向きには共変、書く向きには反変でなければならず、両方を満たすには不変(Ref S <: Ref TはS = Tのときだけ)にするしかない(Cornell CS611の講義ノート)。Adaはこれを型で禁じず、代入時の実行時検査で受けている。

重なる所もある。篩型で見ると{x: T | p} <: {x: T | q}は「pならばq」で成り立つので、値を絞った型は一般的な部分型の特殊な場合になる。ただしこの判定は一般には決定不能なので、Adaは静的に決めず実行時に回した(判定できない部分型は、拒否も受理もせず実行時の検査に回す)。

Adaにもオブジェクト指向の意味の部分型はある。Ada 95のtagged typeは型の拡張(単一継承)を持ち、各tagged type Tに対応するclass-wide type T'Classは、Tとその子孫の値をまとめて受け付ける(Ada 95 RM §3.9)。Adaはこれをsubtypeとは呼ばず、派生(derivation)の延長として扱っている。

払い方で並べる

実行時に検査する

• Ada — range制約は実行時検査。Ada 2012で任意の論理式を述語にできるStatic_Predicate / Dynamic_Predicateが入った。静的述語は許された形に限られる代わりに、case文の網羅性検査などに使える。動的述語は実行時に検査されるが、規格は全ての違反を捕まえることを要求していない(レコードの成分への代入後は検査されない)。
• Pascal — 部分範囲型0..9。基底型(host type)の値の区間で、Adaのsubtypeが出てくるきっかけになった(上記)。
• Nim — range[1..10]。外れるとRangeDefect。-d:dangerで全ての実行時検査を外せるので、検査は捨てられる前提の安全網になっている。
• Raku — subset BigInt of Int where * > 1_000_000。代入と引数の束縛でwhere節を検査する。
• Common Lisp — (and integer (satisfies evenp))は偶数の整数を表す型指定子。deftypeで名前を付けられる。述語は任意の型の値で呼ばれうるので、副作用を持たず、どんな値でも答えられるように書く。

Adaで面白いのは、違反が確実に分かっても警告にとどまることである。GNATは定数の範囲外代入に「Constraint_Error will be raised at run time」と警告するが、プログラムは不正ではない。Adaの範囲検査は型検査ではなく実行時の意味論として定義されているので、コンパイラは「この行は必ず例外を投げる」と言えても拒否する根拠を持たない。

hybrid type checkingはここを変えた。違反が反証できたものは型エラーとして拒否し、決められないものだけを実行時に回す(判定できない部分型は、拒否も受理もせず実行時の検査に回す)。

静的に払う

• SPARK — Adaの部分集合。述語に使える式を制限し、違反が起きないことを形式検証で示す。同じsubtypeの宣言を、Adaは実行時検査、SPARKは証明の対象として扱う。
• PVS — 述語部分型{x: T | p(x)}。型検査が決定不能になる代わりに、型検査器が型正当性条件(TCC: type-correctness condition)という証明責務を生成する。実際に出るTCCの大半は証明器が自動で片付ける。1/0は型が合わない。
• Lean — {x : α // p x}は値valと、それがpを満たす証明propertyの組。作るときに証明を渡すので、使う側は検査しない。実行時の表現はαと同じで、証明は消える。

LeanとPVSの違いは、証明を値の側が持つか、型検査の副産物として外に出すかである。LeanではSubtypeを作る人が証明を書く。PVSでは書いた式に応じて検査器が責務を出し、利用者が後で証明する。

Carinaの位置

Carinaのカスタム型も述語付き部分型である(カスタム型は独立の構成子ではなく篩型である)。値を完全評価してから所属を判定する(型は値の分類器である)ので、述語は任意の計算を含められる。

払い方はhybridに近い。型の段では、識別を持たない篩付きの受け側に対して判定を値の検査へ回すことがある。値の段では、planで分かる値はplanで判定し、分からない値はapplyでプロバイダに送る直前に判定する。

Adaと違うのは、plan時に確実に違反と分かったものはエラーにすることである。Adaの「必ず例外を投げるが合法」に当たるものは、Carinaでは「planは通るがapplyで必ず失敗する」になり、IaCでは途中まで作ったリソースが残る分だけ高くつく。

同じidentityの中ではAdaの形にする

2026-11-07に決まった変更(carina#4309)で、Carinaは二段構えになる。identityが違う型の間は一般的な(公称的な)部分型で、aws.iam.Role.Arn <: aws.Arnのような包摂の辺で判定する(公称軸ごとの幅部分型付けが再利用と混同防止を両立する)。identityが同じ型の間はAdaのsubtypeと同じで、長さやパターンの違いでは拒否せず、受け側の制約を値が分かった時点で検査する。identityがAdaの型、局所的な制約がAdaの制約に当たる。

きっかけはidentity_store_idである。awscc.sso.Instance.identity_store_idはCFNのスキーマで長さ1..64・パターン^[a-zA-Z0-9-]*$、受け側のawscc.identitystore.Group.identity_store_idは長さ1..36・パターン^d-[0-9a-f]{10}$|^<uuid>$で、identityは同じidentity_store_id()である。篩型の部分型として見ると、64は36に収まらないので拒否になる。実際のIDはd-と16進10桁で、受け側に必ず収まる。

この拒否は判定できないこと(hybrid type checkingの「?」)から来ていない。宣言どうしなら「含まれない」と決められる。問題は宣言の側で、送り側の1..64は実際の値の集合を緩く書いた記述にすぎなかった。信用できるのはidentityの一致のほうで、局所的な制約は値の性質ではなく受け側の要求として扱う、という判断になる。Adaの理由書が制約を型から切り離して動的な性質としたのと同じ筋である。

#型システム #篩型 #部分型 #型理論