4.6 KiB
制約と default
この章では、制約と default の意味を定義する。
制約
制約は、値が満たすべき条件を表す。
Int
String
>= 1
<= 65535
/Hello! .*/
制約は & により合成できる。
Port = Int & >= 1 & <= 65535;
NarrowedPort = Port & > 443;
制約合成の意味は、すべての制約を同時に満たすことである。
A & B = A と B の両方を満たす値または制約
矛盾する制約はエラーになる。
Int & String # エラー
> 10 & < 5 # エラー
Int & > 10 & < 11 # エラー。整数値の候補が存在しない
制約の正規化
& によって abstract value 同士を合成した場合、処理系は軽量に判定できる制約を正規化する。
正規化対象:
- primitive type 制約。
- 数値比較制約。
primitive type 制約は、異なる型が同時に要求された場合 conflict になる。
Int & Float
Int & String
数値比較制約は上下限として正規化される。
Int & >= 1 & <= 65535 & > 443
これは概念的に以下へ正規化される。
Type(Int)
> 443
<= 65535
上下限の交差が空であれば conflict になる。
Int 制約がある場合は、整数候補が存在するかも判定する。
> 10 & < 5 # conflict
Int & > 10 & < 11 # conflict
Int & >= 10 & <= 10 # OK
Int の比較制約は整数リテラルを使う。
Float の比較制約は整数リテラルまたは浮動小数リテラルを使える。
組み込み制約
最小の組み込み制約は以下である。
String
Int
Float
Bool
追加の述語制約はライブラリまたは組み込みとして提供できる。
IPv4Address
正規表現制約
正規表現リテラルは文字列制約として使える。
Host = /^\d{1,3}\.\d{1,3}\.\d{1,3}\.\d{1,3}$/;
正規表現制約は積み重ね可能である。 複数の正規表現制約が同じ abstract value に付与された場合、具体文字列はすべての正規表現制約に一致しなければならない。
String & /^a/ & /z$/
処理系は、正規表現制約同士の交差が空であるかを合成時に判定する必要はない。 つまり、以下は合成時には conflict にならず、具体値検証時に失敗する。
String & /^a$/ & /^b$/
正規表現エンジンは optional feature にできる。 正規表現 feature が無効な処理系では、正規表現制約の検証は unsupported feature diagnostic になる。 軽量実装では代表的な制約を組み込み述語として提供してもよい。
Host = IPv4Address;
default
default は制約ではない。
default は、最終評価時に明示値が存在しない場合だけ使われる fallback 値である。
port = NarrowedPort default 8080;
これは概念的には以下を表す。
Abstract {
constraints: [NarrowedPort]
default: 8080
}
明示値が合成された場合、default は採用されない。
MyConfig = {
port = NarrowedPort default 8080;
};
Config = MyConfig & {
port = 8000;
};
この場合、最終値は 8000 である。
8080 は評価されない、または評価されても採用されない。
明示値がない場合、最終 materialize 時に default が採用される。
採用された default 値は、同じフィールドに定義された制約を満たす必要がある。
Abstract {
constraints: [NarrowedPort]
default: 8080
}
finalize => 8080 が NarrowedPort を満たせば成功
default の内部表現
default は abstract value に付随する fallback thunk として保持できる。
これにより、default 値自体も必要になるまで評価しない。
RuntimeValue =
Concrete(ConcreteValue)
Abstract {
constraints: Vec<Constraint>
default: Option<Thunk>
}
明示値は Concrete として表現し、default を保持しない。
Abstract & Concrete が成功した場合、制約検証後に Concrete になり、default は消える。
default の合成
同じフィールドに複数の default が合成された場合の詳細規則は未確定である。
現時点の単純な方針は以下である。
&による default 同士の衝突はエラーにする。- 同一 default 値は許可してよい。
//による patch では右辺 default が左辺 default を置き換える。
この方針により、& は制約を保った合成、// は上書き操作として説明できる。