init

doc/manual/souce/language/constraints-and-defaults.md

@@ -0,0 +1,134 @@
+# 制約と default
+
+この章では、制約と `default` の意味を定義する。
+
+## 制約
+
+制約は、値が満たすべき条件を表す。
+
+```n
+Int
+String
+>= 1
+<= 65535
+/Hello! .*/
+```
+
+制約は `&` により合成できる。
+
+```n
+Port = Int & >= 1 & <= 65535;
+NarrowedPort = Port & > 443;
+```
+
+制約合成の意味は、すべての制約を同時に満たすことである。
+
+```text
+A & B = A と B の両方を満たす値または制約
+```
+
+矛盾する制約はエラーになる。
+
+```n
+Int & String       # エラー
+>= 10 & <= 5       # エラーになりうる
+```
+
+## 組み込み制約
+
+最小の組み込み制約は以下である。
+
+```n
+String
+Int
+Float
+Bool
+```
+
+追加の述語制約はライブラリまたは組み込みとして提供できる。
+
+```n
+IPv4Address
+```
+
+## 正規表現制約
+
+正規表現リテラルは文字列制約として使える候補である。
+
+```n
+Host = /^\d{1,3}\.\d{1,3}\.\d{1,3}\.\d{1,3}$/;
+```
+
+ただし、組み込み向け実装では正規表現エンジンを optional feature にできる。
+軽量実装では代表的な制約を組み込み述語として提供してもよい。
+
+```n
+Host = IPv4Address;
+```
+
+## default
+
+`default` は制約ではない。
+`default` は、最終評価時に明示値が存在しない場合だけ使われる fallback 値である。
+
+```n
+port = NarrowedPort default 8080;
+```
+
+これは概念的には以下を表す。
+
+```text
+constraint = NarrowedPort
+value      = none
+default    = 8080
+```
+
+明示値が合成された場合、`default` は採用されない。
+
+```n
+MyConfig = {
+    port = NarrowedPort default 8080;
+};
+
+Config = MyConfig & {
+    port = 8000;
+};
+```
+
+この場合、最終値は `8000` である。
+`8080` は評価されない、または評価されても採用されない。
+
+明示値がない場合、最終 materialize 時に `default` が採用される。
+採用された default 値は、同じフィールドに定義された制約を満たす必要がある。
+
+```text
+constraint = NarrowedPort
+value      = none
+default    = 8080
+
+finalize => 8080 が NarrowedPort を満たせば成功
+```
+
+## default の内部表現
+
+`default` は fallback thunk として保持できる。
+これにより、default 値自体も必要になるまで評価しない。
+
+```text
+Cell {
+  constraint: ConstraintSet
+  value: Option<Value>
+  default: Option<Thunk>
+}
+```
+
+## default の合成
+
+同じフィールドに複数の `default` が合成された場合の詳細規則は未確定である。
+現時点の単純な方針は以下である。
+
+- `&` による default 同士の衝突はエラーにする。
+- 同一 default 値は許可してよい。
+- `//` による patch では右辺 default が左辺 default を置き換える。
+
+この方針により、`&` は制約を保った合成、`//` は上書き操作として説明できる。