制約と default

この章では、制約と default の意味を定義する。

制約

制約は、値が満たすべき条件を表す。

Int
String
>= 1
<= 65535
/Hello! .*/

制約は & により合成できる。

Port = Int & >= 1 & <= 65535;
NarrowedPort = Port & > 443;

制約合成の意味は、すべての制約を同時に満たすことである。

A & B = A と B の両方を満たす値または制約

矛盾する制約はエラーになる。

Int & String       # エラー
>= 10 & <= 5       # エラーになりうる

最小の組み込み制約は以下である。

String
Int
Float
Bool

追加の述語制約はライブラリまたは組み込みとして提供できる。

IPv4Address

正規表現リテラルは文字列制約として使える候補である。

Host = /^\d{1,3}\.\d{1,3}\.\d{1,3}\.\d{1,3}$/;

ただし、組み込み向け実装では正規表現エンジンを optional feature にできる。軽量実装では代表的な制約を組み込み述語として提供してもよい。

Host = IPv4Address;

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 は abstract value に付随する fallback thunk として保持できる。これにより、default 値自体も必要になるまで評価しない。

RuntimeValue =
  Concrete(ConcreteValue)
  Abstract {
    constraints: Vec<Constraint>
    default: Option<Thunk>
  }

明示値は Concrete として表現し、default を保持しない。 Abstract & Concrete が成功した場合、制約検証後に Concrete になり、default は消える。

同じフィールドに複数の default が合成された場合の詳細規則は未確定である。現時点の単純な方針は以下である。

この方針により、& は制約を保った合成、// は上書き操作として説明できる。