Repository: tweag/nickel
Pull request #625 (2022-02-24 16:08:52)

Remove Array aliasing Array Dyn
Depends on #622.

We originally transitioned from only one list type `List` to a parametrized list type `List Dyn`. At that time, we introduced an alias `List` for `List Dyn`, now being `Array` for `Array Dyn`, to let existing code (albeit tiny) untouched. It turns out this requires special casing in the parser today with the uniterm syntax, and takes syntax real estate without being strongly motivated (to this day, we've mostly written arrays parametrized by something more precise than `Dyn`).

This PRs removes the alias, forcing an `Array` type to always have a parameter. If this turns out to be really useful in practice later, we can always introduce it again.

dpulls[bot]: :tada: All dependencies have been resolved !

Patch:
diff --git a/doc/manual/contracts.md b/doc/manual/contracts.md
index eb85ba33..5db59533 100644
--- a/doc/manual/contracts.md
+++ b/doc/manual/contracts.md
@@ -433,9 +433,6 @@ error: contract broken by a value.
 [..]
 ```
 
-Recall that `Array` is an alias for `Array Dyn`, thus the `Array` contracts only
-checks that the value is an array.
-
 #### Functions
 
 A function contract `In -> Out` returns a wrapped function which, for each call,
diff --git a/doc/manual/typing.md b/doc/manual/typing.md
index 52e301d2..5b1b6a47 100644
--- a/doc/manual/typing.md
+++ b/doc/manual/typing.md
@@ -163,8 +163,7 @@ Let us now have a quick tour of the type system. The basic types are:
 
 The following type constructors are available:
 
-- **Array**: `Array T`. An array of elements of type `T`. When no `T` is specified, `Array`
-  alone is an alias for `Array Dyn`.
+- **Array**: `Array T`. An array of elements of type `T`.
 
   Example:
   ```nickel
diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop
index 7e0274a2..5f14aba2 100644
--- a/src/grammar.lalrpop
+++ b/src/grammar.lalrpop
@@ -241,6 +241,7 @@ Forall: Types =
 // also includes previous levels).
 Applicative: UniTerm = {
     "import" <s: StaticString> => UniTerm::from(Term::Import(OsString::from(s))),
+    AsUniTerm<TypeArray>,
     <t1: AsTerm<Applicative>> <t2: AsTerm<RecordOperand>> =>
         UniTerm::from(mk_app!(t1, t2)),
     <op: UOp> <t: AsTerm<RecordOperand>> => UniTerm::from(mk_term::op1(op, t)),
@@ -250,25 +251,9 @@ Applicative: UniTerm = {
     RecordOperand,
 };
 
-// The array type, potentially with an argument. Take precedence over
-// application: `Array Foo` is always interpreted as the type `Array` parametrized
-// by `Foo`, rather than the dynamic array type `Array Dyn` aliased to `Array` and
-// seen as a contract applied to term `Foo`.
-TypeArray: Types =
-    "Array" <TypeArrayParam?> => {
-        let ty = Box::new(<>.unwrap_or(Types(AbsType::Dyn())));
-        Types(AbsType::Array(ty))
-    };
-
-// Possible parameter for the array type. It's `TypeAtom` augmented with an
-// argument-less `Array`, which allows to parse `Array Array`. We can't add
-// argument-less `Array` to type atoms directly, as it would make `Array Foo`
-// ambiguous: could be parsed both as `Array` as a term applied to `Array` as a
-// term, or as the parametrized type `Array Array`).
-TypeArrayParam: Types = {
-    "Array" => Types(AbsType::Array(Box::new(Types(AbsType::Dyn())))),
-    AsType<Atom>,
-};
+// The parametrized array type.
+TypeArray: Types = "Array" <AsType<Atom>> =>
+    Types(AbsType::Array(Box::new(<>)));
 
 RecordOperand: UniTerm = {
     Atom,
@@ -680,7 +665,6 @@ InfixLazyBOpApp<UOp, LExpr, RExpr>: UniTerm =
 InfixExpr: UniTerm = {
     #[precedence(level="0")]
     Applicative,
-    AsUniTerm<TypeArray>,
 
     #[precedence(level="1")]
     "-" <AsTerm<InfixExpr>> =>
diff --git a/src/typecheck/operation.rs b/src/typecheck/operation.rs
index 127d71be..01cef877 100644
--- a/src/typecheck/operation.rs
+++ b/src/typecheck/operation.rs
@@ -141,7 +141,7 @@ pub fn get_uop_type(
             //mk_tyw_record!(; TypeWrapper::Ptr(state.table.fresh_var())),
             mk_typewrapper::array(AbsType::Str()),
         ),
-        // Dyn -> Array
+        // Dyn -> Array Dyn
         UnaryOp::ValuesOf() => (
             mk_typewrapper::dynamic(),
             mk_typewrapper::array(AbsType::Dyn()),
diff --git a/src/types.rs b/src/types.rs
index e20af57f..4bfe1dc0 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -365,7 +365,7 @@ impl Types {
 
         match &self.0 {
             Dyn() | Num() | Bool() | Str() | Var(_) => true,
-            Array(ty) if ty.0 == AbsType::Dyn() => true,
+            Flat(rt) if matches!(*rt.term, Term::Var(_)) => true,
             _ => false,
         }
     }
@@ -378,7 +378,6 @@ impl fmt::Display for Types {
             AbsType::Num() => write!(f, "Num"),
             AbsType::Bool() => write!(f, "Bool"),
             AbsType::Str() => write!(f, "Str"),
-            AbsType::Array(ty) if ty.0 == AbsType::Dyn() => write!(f, "Array"),
             AbsType::Array(ty) => {
                 write!(f, "Array ")?;
 
@@ -483,11 +482,10 @@ mod test {
         assert_format_eq("[|a, b, c, d|]");
         assert_format_eq("forall r. [|tag1, tag2, tag3 ; r|]");
 
-        assert_format_eq("Array");
         assert_format_eq("Array Num");
         assert_format_eq("Array (Array Num)");
         assert_format_eq("Num -> Array (Array Str) -> Num");
         assert_format_eq("Array (Num -> Num)");
-        assert_format_eq("Array (Array Array -> Num)");
+        assert_format_eq("Array (Array (Array Dyn) -> Num)");
     }
 }
diff --git a/stdlib/array.ncl b/stdlib/array.ncl
index 773c16e3..7bb1f8c2 100644
--- a/stdlib/array.ncl
+++ b/stdlib/array.ncl
@@ -209,7 +209,7 @@
         "%m
       = fun pred l => fold (fun x acc => if pred x then true else acc) false l,
 
-    elem : Dyn -> Array -> Bool
+    elem : Dyn -> Array Dyn -> Bool
       | doc m%"
         Results in true if the given element is a member of the array, false otherwise.
 
diff --git a/stdlib/record.ncl b/stdlib/record.ncl
index 64ced7fe..1adf436d 100644
--- a/stdlib/record.ncl
+++ b/stdlib/record.ncl
@@ -26,7 +26,7 @@
       "%m
     = fun r => %fields% r,
 
-    values | { ; Dyn} -> Array
+    values | { ; Dyn} -> Array Dyn
     | doc m%"
       Given a record, results in a array containing all the values in that record.
 


Test patch:
diff --git a/tests/contracts_fail.rs b/tests/contracts_fail.rs
index 3e89390c..82d6e32c 100644
--- a/tests/contracts_fail.rs
+++ b/tests/contracts_fail.rs
@@ -138,11 +138,11 @@ fn lists_contracts() {
         Err(Error::EvalError(EvalError::BlameError(..)))
     );
     assert_matches!(
-        eval("1 | Array"),
+        eval("1 | Array Dyn"),
         Err(Error::EvalError(EvalError::BlameError(..)))
     );
     assert_matches!(
-        eval("(fun x => x) | Array"),
+        eval("(fun x => x) | Array Dyn"),
         Err(Error::EvalError(EvalError::BlameError(..)))
     );
 
diff --git a/tests/pass/contracts.ncl b/tests/pass/contracts.ncl
index 8fcedbe9..6c408904 100644
--- a/tests/pass/contracts.ncl
+++ b/tests/pass/contracts.ncl
@@ -98,7 +98,7 @@ let Assert = fun l x => x || %blame% l in
   ({a = 0, b = 0, c = 0} | Contract) == {a = 0, b = 0, c = 0},
 
   // arrays 
-  ([1, "2", false] | Array) == [1, "2", false],
+  ([1, "2", false] | Array Dyn) == [1, "2", false],
   ([1, 2, 3] | Array Num) == [1, 2, 3],
   (["1", "2", "false"] | Array Str) == ["1", "2", "false"],
 
diff --git a/tests/pass/typechecking.ncl b/tests/pass/typechecking.ncl
index 19c9fb88..e339b523 100644
--- a/tests/pass/typechecking.ncl
+++ b/tests/pass/typechecking.ncl
@@ -102,7 +102,7 @@ let typecheck = [
   // arrays_simple
   [1, "2", false],
   //TODO: the type system may accept the following test at some point.
-  //([1, "2", false] : Array),
+  //([1, "2", false] : Array Dyn),
   ["a", "b", "c"] : Array Str,
   [1, 2, 3] : Array Num,
   (fun x => [x]) : forall a. a -> Array a,
diff --git a/tests/typecheck_fail.rs b/tests/typecheck_fail.rs
index 964e6636..ba076801 100644
--- a/tests/typecheck_fail.rs
+++ b/tests/typecheck_fail.rs
@@ -136,7 +136,7 @@ fn dynamic_record_simple() {
 #[test]
 fn simple_array() {
     assert_typecheck_fails!("[1, 2, false] : Array Num");
-    assert_typecheck_fails!("[(1 : Str), true, \"b\"] : Array");
+    assert_typecheck_fails!("[(1 : Str), true, \"b\"] : Array Dyn");
     assert_typecheck_fails!("[1, 2, \"3\"] : Array Str");
 }
 
@@ -144,7 +144,7 @@ fn simple_array() {
 fn arrays_operations() {
     assert_typecheck_fails!("(fun l => %head% l) : forall a b. (Array a -> b)");
     assert_typecheck_fails!(
-        "(fun f l => %elem_at% (%map% l f) 0) : forall a. (forall b. (a -> b) -> Array -> b)"
+        "(fun f l => %elem_at% (%map% l f) 0) : forall a. (forall b. (a -> b) -> Array Dyn -> b)"
     );
 }