Repository: tweag/nickel
Pull request #1995 (2024-07-15 19:27:03)

Add boolean contract combinators to the stdlib
Depends on #1987

This commit adds the boolean combinators `one_of`, `not` and `all_of` to the contract module of the stdlib. They are implemented in the obvious way, by making immediate decisions based on the immediate part of their contract operands. The limitations and possible work around are detailed in the documentation and in the manual.

I considered the addition of `one_of`, to adhere to the JSON schema terminology, but it turns out that it seems pretty useless for the time being, because record contracts are mostly delayed and I couldn't come up with a simple compelling example that would work in the current setting, where `one_of` would be needed over `any_of`. The standard example is two record contracts with an non-empty intersection, like `{employee_id, name, ..}` and `{student_id, name, ..}`, but this can't work as expected currently as the check for missing fields is delayed. I suspect we need to wait for proper full eager versions of builtin record contracts for a simple example (one can write the previous example with specialized custom contracts, but it starts to be involved - the fact that I can't come up with a short example to put in the documentation of the function leads me to think that it's too early to introduce this function)

jneem: I think `oneOf` is pretty useless in general, not just in nickel...
yannham: > I think oneOf is pretty useless in general, not just in nickel...

Yeah, it's hard to think of a good, natural use-case. I imagine they might exist. Let's implement it lazily: wait for someone to come with a need for it.

Otherwise, it's ready to review now @jneem (sorry about the early ping, I requested your review too soon, before adding tests)
dpulls[bot]: :tada: All dependencies have been resolved !

Patch:
diff --git a/core/src/typecheck/mod.rs b/core/src/typecheck/mod.rs
index cedaec2b..114faa06 100644
--- a/core/src/typecheck/mod.rs
+++ b/core/src/typecheck/mod.rs
@@ -2383,45 +2383,43 @@ pub fn subsumption(
     checked: UnifType,
 ) -> Result<(), UnifError> {
     let inferred_inst = instantiate_foralls(state, &mut ctxt, inferred, ForallInst::UnifVar);
-    match (&inferred_inst, &checked) {
-        (
-            UnifType::Concrete {
-                typ: TypeF::Record(rrows),
-                ..
-            },
-            UnifType::Concrete {
-                typ: TypeF::Dict { type_fields, .. },
-                ..
-            },
-        ) => {
-            for row in rrows.iter() {
-                match row {
-                    GenericUnifRecordRowsIteratorItem::Row(a) => {
-                        subsumption(state, ctxt.clone(), a.typ.clone(), *type_fields.clone())?
-                    }
-                    GenericUnifRecordRowsIteratorItem::TailUnifVar { id, .. } =>
-                    // We don't need to perform any variable level checks when unifying a free
-                    // unification variable with a ground type
-                    // We close the tail because there is no garanty that
-                    // { a : Number, b : Number, _ : a?} <= { _ : Number}
-                    {
-                        state
-                            .table
-                            .assign_rrows(id, UnifRecordRows::concrete(RecordRowsF::Empty))
-                    }
-                    GenericUnifRecordRowsIteratorItem::TailConstant(id) => {
-                        Err(UnifError::WithConst {
-                            var_kind: VarKindDiscriminant::RecordRows,
-                            expected_const_id: id,
-                            inferred: checked.clone(),
-                        })?
+    if let (UnifType::Concrete { typ: typ1, .. }, UnifType::Concrete { typ: typ2, .. }) =
+        (&inferred_inst, &checked)
+    {
+        match (typ1, typ2) {
+            (TypeF::Record(rrows), TypeF::Dict { type_fields, .. }) => {
+                for row in rrows.iter() {
+                    match row {
+                        GenericUnifRecordRowsIteratorItem::Row(a) => {
+                            subsumption(state, ctxt.clone(), a.typ.clone(), *type_fields.clone())?
+                        }
+                        GenericUnifRecordRowsIteratorItem::TailUnifVar { id, .. } =>
+                        // We don't need to perform any variable level checks when unifying a free
+                        // unification variable with a ground type
+                        // We close the tail because there is no garanty that
+                        // { a : Number, b : Number, _ : a?} <= { _ : Number}
+                        {
+                            state
+                                .table
+                                .assign_rrows(id, UnifRecordRows::concrete(RecordRowsF::Empty))
+                        }
+                        GenericUnifRecordRowsIteratorItem::TailConstant(id) => {
+                            Err(UnifError::WithConst {
+                                var_kind: VarKindDiscriminant::RecordRows,
+                                expected_const_id: id,
+                                inferred: checked.clone(),
+                            })?
+                        }
+                        _ => (),
                     }
-                    _ => (),
                 }
+                Ok(())
             }
-            Ok(())
+            (TypeF::Array(a), TypeF::Array(b)) => subsumption(state, ctxt, *a.clone(), *b.clone()),
+            (_, _) => checked.unify(inferred_inst, state, &ctxt),
         }
-        (_, _) => checked.unify(inferred_inst, state, &ctxt),
+    } else {
+        checked.unify(inferred_inst, state, &ctxt)
     }
 }
 
diff --git a/core/stdlib/std.ncl b/core/stdlib/std.ncl
index 4f3d22ec..1c5871ce 100644
--- a/core/stdlib/std.ncl
+++ b/core/stdlib/std.ncl
@@ -1175,6 +1175,7 @@
           ),
 
     Sequence
+      | Array Dyn -> Dyn
       | doc m%"
           Apply multiple contracts from left to right.
 
@@ -1381,6 +1382,7 @@
       },
 
     apply
+      : Dyn -> Dyn -> Dyn -> Dyn
       | doc m%"
           Applies a contract to a label and a value. Either aborts the execution
           with a broken contract error if the contract fails, or proceeds with
@@ -1481,6 +1483,13 @@
         %contract/apply% contract (%label/push_diag% label) value,
 
     apply_as_custom
+      : Dyn -> Dyn -> Dyn -> [|
+        'Ok Dyn,
+        'Error {
+          message | String | optional,
+          notes | Array String | optional
+        }
+      |]
       | doc m%"
           Variant of `std.contract.apply` which returns `'Error {..}` upon
           immediate failure of the contract instead of aborting the execution
@@ -1514,6 +1523,136 @@
       = fun contract label value =>
         %contract/apply_as_custom% contract (%label/push_diag% label) value,
 
+    any_of
+      | Array Dyn -> Dyn
+      | doc m%"
+          Builds a contract that checks if the value satisfies at least one of
+          the given contracts. More precisely, `any_of` applies each contract in
+          order and returns the result of the first one that doesn't fail
+          immediately (that is, the first one which returns the value `'Ok _`).
+
+          **Important** `any_of` is only an approximation of what you could
+          expect from an `or` operation on contracts. Because `any_of` must
+          preserve the lazyness of contracts, it means that it has to
+          pick the right branch by relying only on the immediate part of each
+          contract, and not on the delayed part.
+
+          Fortunately, `any_of` is an overstrict approximation, in that it might
+          reject more values than what you expect, but it'll never let invalid
+          values slip through.
+
+          Typically, `std.contract.any_of [{ foo | String }, { foo | Number }]`
+          will behave exactly as `{ foo | Number }`, because the immediate part
+          of the built-in record contracts can't discriminate between the two
+          possibilities. In particular, perhaps surprisingly, the value `{foo =
+          1+1}` is rejected. Please refer to the boolean combinators section of
+          the contract chapter of the manual for a more detailed
+          explanation of the limitations of `any_of` and other boolean
+          combinators, as well as how to work around them.
+
+          # Examples
+
+          ```nickel
+          let Date = std.contract.any_of [
+            String,
+            {
+              day | Number,
+              month | Number,
+              year | Number
+            }
+          ]
+          in
+
+          { day = 1, month = 1, year = 1970 } | Date
+          ```
+        "%
+      = fun contracts =>
+        %contract/custom%
+          (
+            fun label value =>
+              std.array.fold_left
+                (
+                  fun acc Contract =>
+                    acc
+                    |> match {
+                      # if the previous contracts failed, we keep trying the
+                      # next
+                      'Error _ =>
+                        let label =
+                          %label/with_message%
+                            "any_of: a delayed check of the picked branch failed"
+                            label
+                        in
+                        std.contract.apply_as_custom Contract label value,
+                      # if one contract succeeded before, we just forward the
+                      # value
+                      ok => ok,
+                    }
+                )
+                ('Error {})
+                contracts
+              |> match {
+                'Error _ =>
+                  'Error {
+                    message = "any_of: value didn't match any of the contracts",
+                  },
+                ok => ok,
+              }
+          ),
+
+    all_of
+      : Array Dyn -> Dyn
+      | doc m%"
+          Builds a contract that checks if the value satisfies all of the given
+          contracts. `all_of` is just an alias for `std.contract.Sequence`, to
+          maintain consistency with `std.contract.any_of` and other JSON
+          Schema-style combinators.
+
+          As opposed to other boolean combinators such as `not` or `any_of`,
+          `all_of` work as you expect most of the time, including on contracts
+          with a delayed part. The only contracts for which `all_of` is
+          overstrict are function contracts. In general, you shouldn't use
+          function contracts with contract combinators.
+          ```
+        "%
+      = std.contract.Sequence,
+
+    not
+      | Dyn -> Dyn
+      | doc m%"
+          Builds a contract that checks if the value doesn't satisfy the given
+          contract. More specifically, `not Contract` will accept `value` if the
+          application of `Contract` to `value` fails immediately, returning
+          `'Error {..}`.
+
+          **Important**: as for other boolean combinators, `not` is only an
+          overstrict approximation of what you could expect. For example,
+          `std.contract.not (Array Number)` will reject `["a"]`, because the
+          check that elements are numbers is delayed. See the boolean
+          combinators section of the contract chapter of the manual for a more
+          detailed explanation of the limitations of `not` and other boolean
+          combinators, as well as how to work around them.
+
+          # Examples
+
+          ```nickel
+          let NotNumber = std.contract.not Number in
+          "a" | NotNumber
+            => "a"
+          ```
+        "%
+      = fun Contract =>
+        %contract/custom%
+          (
+            fun label value =>
+              value
+              |> std.contract.apply_as_custom Contract label
+              |> match {
+                'Ok _ => 'Error { message = "not: value matched the immediate part of the contract" },
+                error => 'Ok value,
+              }
+          ),
+
     unstable
       | doc m%"
           The unstable module gathers contracts that are used right now in the
diff --git a/doc/manual/contracts.md b/doc/manual/contracts.md
index 130de7b3..16db8a99 100644
--- a/doc/manual/contracts.md
+++ b/doc/manual/contracts.md
@@ -386,7 +386,6 @@ builtin contract `[| 'Foo Contract |]` parametrized by `Contract`:
     _ => 'Error {},
   })
 
-
 > 'Foo 5 | FooOf Number
 'Foo 5
 
@@ -601,14 +600,14 @@ example:
 
 > {data = "", must_be_very_secure = false} | Secure
 error: non mergeable terms
-  ┌─ <repl-input-21>:1:36
+  ┌─ <repl-input-22>:1:36
   │
 1 │  {data = "", must_be_very_secure = false} | Secure
   │                                    ^^^^^    ------ originally merged here
   │                                    │
   │                                    cannot merge this expression
   │
-  ┌─ <repl-input-19>:2:34
+  ┌─ <repl-input-20>:2:34
   │
 2 │     must_be_very_secure | Bool = true,
   │                                  ^^^^ with this expression
@@ -675,7 +674,7 @@ contract to each element:
 
 > [1000, 10001, 2] | Array VeryBig
 error: contract broken by a value
-  ┌─ <repl-input-27>:1:16
+  ┌─ <repl-input-28>:1:16
   │
 1 │  [1000, 10001, 2] | Array VeryBig
   │                ^          ------- expected array element type
@@ -743,7 +742,7 @@ functions as parameters. Here is an example:
 > let apply_fun | (Number -> Number) -> Number = fun f => f 0 in
   apply_fun (fun x => "a")
 error: contract broken by the caller
-  ┌─ <repl-input-30>:1:29
+  ┌─ <repl-input-31>:1:29
   │
 1 │  let apply_fun | (Number -> Number) -> Number = fun f => f 0 in
   │                             ------ expected return type of a function provided by the caller
@@ -1058,3 +1057,155 @@ is wrapping the original value with delayed checks inside**. Doing so preserves
 laziness of the language and only triggers the checks when the values are used
 or exported in a configuration. This is the reason for general custom contracts
 to have an immediate part and a delayed part.
+
+## Boolean combinators
+
+The stdlib features a set of boolean combinators for contracts:
+`std.contract.all_of`, `std.contract.any_of` and `std.contract.not`.
+
+It's important to note that those combinators are only *approximations* of what
+you could expect from boolean operations. Fortunately, they are overstrict
+approximation, in that they might reject more values, but will never let invalid
+values slip through.
+
+The reason is, once again, the presence of delayed contracts.
+
+### Combining delayed contracts
+
+Let `Foo` be the contract `std.contract.any_of [{ foo | String }, {foo |
+Number}]`. Like all built-in contracts and contract combinators, `any_of` is
+designed to preserve lazyness and delayed checks, so it can't evaluate the field
+`foo` to determine if it's a number or a string, as it's a delayed check of each
+built-in record contract. In particular, checking the value `{foo = 1+1}`
+against `Foo` will fail: `any_of` will run `{foo | String}`, whose immediate
+part will succeed (the shape matches) and return `'Ok {foo | String = 1+1}`.
+From there, `any_of` has no way to know that the delayed check will eventually
+fail, and such delayed failures aren't catchable. Thus, the branch to pick is
+based on the immediate part, and `any_of` will pick `{Foo | String}`. When `foo`
+will be requested, the `String` contract will eventually be applied and will
+fail.
+
+That is, `{foo = 1+1} | Foo` will fail, which is surprising. `Foo` as defined
+here is essentially useless and equivalent to just `{Foo | String}`. As both
+branches have the same immediate part, they can't discriminate between values,
+and either `{foo | String}` will be picked, or both contracts will fail, but the
+`{foo | Number}` contract will never be picked.
+
+Similarly, `std.contract.any_of [Array Number, Array String]` will
+always behave as `Array Number`.
+
+On the other hand, `std.contract.any_of [Number, String]` will work as expected,
+because those contracts are immediate. More generally, boolean combinators work
+as expected on custom contracts built from predicates or validators (using
+`std.contract.from_predicate` and `std.contract.from_validator`).
+
+Some combinations of delayed contracts, such as `std.contract.any_of [{ foo |
+Number }, { bar | String }]` will also work as expected. In this case, the check
+for extra fields is immediate and will be sufficient to discriminate between the
+two branches immediately.
+
+**Important** Note that the check for missing fields is *delayed* in the
+built-in record contracts. When you apply a record contract, Nickel expects that
+all fields might not be present *yet*, but they are rather expected to be
+introduced by other parts of the configuration through merging. Instead of
+raising an error right away, missing fields are just introduced as fields
+without definition, which makes them delayed checks. Thus, `std.contract.any_of
+[{ foo | Number, bar | String}, {foo | Number}]` won't behave as expected, and
+will fail on `{foo = 1+1}`. Indeed, this combination will always pick the first
+contract, setting `bar` as a field without definition to be filled later. Once
+again, this combination is equivalent to its first element, the contract `{foo |
+Number, bar | String}` alone. Interestingly, swapping the two contracts makes
+`any_of` work as expected: `std.contract.any_of [{foo | Number}, {foo | Number,
+bar | String}]`. Because `any_of` tries contracts in order, and that extra
+fields *are* checked immediately, `{foo | Number}` will be able to reject a
+record with a `bar` field immediately. Note that in this particular example, the
+right way to write this contract is rather `{ foo | Number, bar | String |
+optional }` - no need to resort to `any_of`.
+
+### Customize the boolean behavior
+
+The limitations mentioned above are inherent to the lazy evaluation model of
+Nickel, and because we want the built-in contracts to preserve lazyness by
+default.
+
+However, if you hit this limitation, you can always decide to build a custom
+contract that will be able to discriminate between more values immediately, at
+the cost of evaluating more data immediately.
+
+For example, consider an encoding of an enum as a record with a tag and a value:
+accepted values are records of the shape `{tag, value}` where the value is a
+number if `tag` is `'Number`, or a string if `tag` is `'String`.
+
+A naive implementation is `std.contract.any_of [{ tag = 'String, value | String
+}, { tag = 'Number, value | Number }]`. This has the exact problem described in
+the previous section: this is equivalent to the contract `{ tag | 'String, value
+| String }`, and will reject the seemingly legal value `{ tag = 'Number, value =
+1+1 }`.
+
+The trick is to use a custom contract that will do more immediate checks. There
+are many different ways to approach this problem, depending on the specifics of
+each situation. Here, we'll write a little `Tagged` contract wrapper that takes
+a record contract, expects `tag` to exist and to be set to a fixed value, and
+will check if the provided value has a matching `tag` immediately.
+
+```nickel #repl
+> let Tagged = fun Contract =>
+  std.contract.custom (fun label =>
+    match {
+      value @ { tag, .. } if tag == Contract.tag =>
+        std.contract.apply_as_custom Contract label value,
+      { tag, .. } =>
+        'Error { message = "incompatible tag field" },
+      _ =>
+        'Error { message = "missing tag field" },
+    }
+  )
+
+> let NumberOrString = std.contract.any_of [
+    Tagged { tag = 'String, value | String },
+    Tagged { tag = 'Number, value | Number },
+  ]
+
+> { tag = 'Number, value = 1+1 } | NumberOrString
+{ tag = '"Number", value | Number = 2, }
+
+> { tag = 'String, value = "hello"} | NumberOrString
+{ tag = '"String", value | String = "hello", }
+
+> { tag = 'Number, value = "hello"} | NumberOrString
+error: contract broken by the value of `value`
+[...]
+```
+
+### Immediate version of built-in contracts
+
+In the future, we plan to provide alternative versions of built-in contracts,
+like `{ foo | Number, bar | String }` or `Array {_ | Number}`, but which are
+fully immediate with no delayed checks. This would allow to use them in boolean
+combinators with the intuitive semantics, at the price of needing to deeply
+evaluate all the content immediately. This might be useful when converting
+schemas from different tools to Nickel blindly without having to write a lot of
+custom contract boilerplate.
+
+As of today, those immediate versions are not yet available. It is advised to
+rely on custom wrappers in the meantime, as explained in the previous section.
+
+## Other combinators
+
+`any_of` has been used as a leading example, but `not` has the same limitations.
+For example, `["a"] | std.contract.not (Array Number)` will fail, as
+`std.contract.not (Array Number)` is essentially the same as `std.contract.not
+(Array Dyn)`, and will reject any array.
+
+On the other hand, `all_of` doesn't suffer from the same limitations, since it
+has to apply all contracts unconditionally.
+
+One exception worth noting is function contracts, which are mostly delayed, and
+might be overstrict with all boolean operators including `all_of`: `all_of
+[Number -> Number, String -> String]` will reject all values, including the
+identity function `fun x => x`, because it's the same contract as
+`std.contract.all_of [Number, String] -> std.contract.all_of[Number, String]`,
+but `std.contract.all_of [Number, String]` is void. Because `fun x => x` can be
+annotated with the `Number -> Number` and `String -> String` contracts
+individually, one could expect that the `any_of` combination would work as well,
+but it doesn't.


Test patch:
diff --git a/core/tests/integration/inputs/contracts/any_of_basic_fail.ncl b/core/tests/integration/inputs/contracts/any_of_basic_fail.ncl
new file mode 100644
index 00000000..0918e4cc
--- /dev/null
+++ b/core/tests/integration/inputs/contracts/any_of_basic_fail.ncl
@@ -0,0 +1,5 @@
+# test.type = 'error'
+#
+# [test.metadata]
+# error = 'EvalError::BlameError'
+true | std.contract.any_of [Number, String]
diff --git a/core/tests/integration/inputs/contracts/any_of_empty.ncl b/core/tests/integration/inputs/contracts/any_of_empty.ncl
new file mode 100644
index 00000000..7bcd30ab
--- /dev/null
+++ b/core/tests/integration/inputs/contracts/any_of_empty.ncl
@@ -0,0 +1,5 @@
+# test.type = 'error'
+#
+# [test.metadata]
+# error = 'EvalError::BlameError'
+null | std.contract.any_of []
diff --git a/core/tests/integration/inputs/contracts/any_of_record_delayed_fail.ncl b/core/tests/integration/inputs/contracts/any_of_record_delayed_fail.ncl
new file mode 100644
index 00000000..168ffdce
--- /dev/null
+++ b/core/tests/integration/inputs/contracts/any_of_record_delayed_fail.ncl
@@ -0,0 +1,9 @@
+# test.type = 'error'
+# eval = 'full'
+#
+# [test.metadata]
+# error = 'EvalError::BlameError'
+{ foo = 1, bar = 2, qux = true} | std.contract.any_of [
+  { foo | Number, bar | Number },
+  { foo | String, bar | Number, qux | Bool }
+]
diff --git a/core/tests/integration/inputs/contracts/any_of_record_immediate_fail.ncl b/core/tests/integration/inputs/contracts/any_of_record_immediate_fail.ncl
new file mode 100644
index 00000000..a94f4493
--- /dev/null
+++ b/core/tests/integration/inputs/contracts/any_of_record_immediate_fail.ncl
@@ -0,0 +1,8 @@
+# test.type = 'error'
+#
+# [test.metadata]
+# error = 'EvalError::BlameError'
+{ foo = 1, bar = 2, qux } | std.contract.any_of [
+  { foo | Number, bar | String },
+  { foo | String, bar | Number, baz | Bool }
+]
diff --git a/core/tests/integration/inputs/contracts/boolean_combinators.ncl b/core/tests/integration/inputs/contracts/boolean_combinators.ncl
new file mode 100644
index 00000000..9fc915b6
--- /dev/null
+++ b/core/tests/integration/inputs/contracts/boolean_combinators.ncl
@@ -0,0 +1,30 @@
+# test.type = 'pass'
+let Assert = std.test.Assert in
+
+[
+  { foo = 1 } | std.contract.any_of [ String, Bool, { .. }],
+  { foo = 1 }
+    | std.contract.any_of
+      [
+        { bar | String },
+        { baz | Bool },
+        { foo | Number }
+      ],
+  true | std.contract.not (std.contract.any_of [ Number, String ]),
+  let Is4Or5 =
+    std.contract.any_of
+      [
+        std.contract.from_predicate ((==) 4),
+        std.contract.from_predicate ((==) 5),
+      ]
+  in
+  [
+    3 | std.contract.not Is4Or5,
+    4 | Is4Or5,
+    5 | Is4Or5,
+  ],
+]
+# This forces each element to make sure contract checks are evaluated, but we
+# don't care about the precise value of `x`, and always return `true`
+|> std.array.map (fun x => x == x)
+|> std.test.assert_all
diff --git a/core/tests/integration/inputs/contracts/not_any_of_fail.ncl b/core/tests/integration/inputs/contracts/not_any_of_fail.ncl
new file mode 100644
index 00000000..053725f9
--- /dev/null
+++ b/core/tests/integration/inputs/contracts/not_any_of_fail.ncl
@@ -0,0 +1,5 @@
+# test.type = 'error'
+#
+# [test.metadata]
+# error = 'EvalError::BlameError'
+"a" | std.contract.not (std.contract.any_of [Number, String])
diff --git a/core/tests/integration/inputs/contracts/not_basic_fail.ncl b/core/tests/integration/inputs/contracts/not_basic_fail.ncl
new file mode 100644
index 00000000..cda3f308
--- /dev/null
+++ b/core/tests/integration/inputs/contracts/not_basic_fail.ncl
@@ -0,0 +1,5 @@
+# test.type = 'error'
+#
+# [test.metadata]
+# error = 'EvalError::BlameError'
+[] | std.contract.not (Array Number)
diff --git a/core/tests/integration/inputs/contracts/not_record_fail.ncl b/core/tests/integration/inputs/contracts/not_record_fail.ncl
new file mode 100644
index 00000000..c4a3c147
--- /dev/null
+++ b/core/tests/integration/inputs/contracts/not_record_fail.ncl
@@ -0,0 +1,5 @@
+# test.type = 'error'
+#
+# [test.metadata]
+# error = 'EvalError::BlameError'
+{ foo = 1, bar = 2} | std.contract.not {foo, bar}
diff --git a/core/tests/integration/inputs/typecheck/array_subtyping.ncl b/core/tests/integration/inputs/typecheck/array_subtyping.ncl
new file mode 100644
index 00000000..788bbd0f
--- /dev/null
+++ b/core/tests/integration/inputs/typecheck/array_subtyping.ncl
@@ -0,0 +1,5 @@
+# test.type = 'pass'
+let test : Array {foo : Number} = [{foo = 5}] in
+let test_func : Array {_ : Number} -> Array {_ : Number} = fun a => a in 
+let result : Array {_ : Number} = test_func test in 
+true