Contract elision for static types

core/src/eval/mod.rs

@@ -703,10 +703,21 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                 // avoiding repeated contract application. Annotations could then be a good way of
                 // remembering which contracts have been applied to a value.
                 Term::Annotated(annot, inner) => {
-                    let contracts = annot.all_contracts()?;
+                    // We apply the contract coming from the static type annotation separately as
+                    // it is optimized.
+                    let static_contract = annot.static_contract();
+                    let contracts = annot.pending_contracts()?;
                     let pos = inner.pos;
+                    let inner = inner.clone();
+
+                    let inner_with_static = if let Some(static_ctr) = static_contract {
+                        static_ctr?.apply(inner, pos)
+                    } else {
+                        inner
+                    };
+
                     let inner_with_ctr =
-                        RuntimeContract::apply_all(inner.clone(), contracts.into_iter(), pos);
+                        RuntimeContract::apply_all(inner_with_static, contracts.into_iter(), pos);
 
                     Closure {
                         body: inner_with_ctr,

core/src/stdlib.rs

@@ -68,7 +68,11 @@ pub mod internals {
     generate_accessor!(bool);
     generate_accessor!(string);
     generate_accessor!(array);
+    generate_accessor!(array_dyn);
     generate_accessor!(func);
+    generate_accessor!(func_dom);
+    generate_accessor!(func_codom);
+    generate_accessor!(func_dyn);
     generate_accessor!(forall_var);
     generate_accessor!(forall);
     generate_accessor!(fail);
@@ -77,6 +81,7 @@ pub mod internals {
     generate_accessor!(record);
     generate_accessor!(dict_type);
     generate_accessor!(dict_contract);
+    generate_accessor!(dict_dyn);
     generate_accessor!(record_extend);
     generate_accessor!(forall_tail);
     generate_accessor!(dyn_tail);

core/src/term/mod.rs

@@ -287,6 +287,15 @@ impl RuntimeContract {
         RuntimeContract { contract, label }
     }
 
+    /// Generate a runtime contract from a type used as a static type annotation and a label. Use
+    /// the guarantees of the static type system to optimize and simplify the contract.
+    pub fn from_static_type(labeled_typ: LabeledType) -> Result<Self, UnboundTypeVariableError> {
+        Ok(RuntimeContract {
+            contract: labeled_typ.typ.contract_static()?,
+            label: labeled_typ.label,
+        })
+    }
+
     /// Map a function over the term representing the underlying contract.
     pub fn map_contract<F>(self, f: F) -> Self
     where
@@ -579,6 +588,15 @@ impl TypeAnnotation {
             .collect::<Result<Vec<_>, _>>()
     }
 
+    /// Build the contract derived from the static type annotation, applying the specific
+    /// optimizations along the way.
+    pub fn static_contract(&self) -> Option<Result<RuntimeContract, UnboundTypeVariableError>> {
+        self.typ
+            .as_ref()
+            .cloned()
+            .map(RuntimeContract::from_static_type)
+    }
+
     /// Convert all the contracts of this annotation, including the potential type annotation as
     /// the first element, to a runtime representation.
     pub fn all_contracts(&self) -> Result<Vec<RuntimeContract>, UnboundTypeVariableError> {

core/src/transform/gen_pending_contracts.rs

@@ -32,7 +32,7 @@ pub fn transform_one(rt: RichTerm) -> Result<RichTerm, UnboundTypeVariableError>
             .map(|v| -> Result<RichTerm, UnboundTypeVariableError> {
                 if let Some(labeled_ty) = &field.metadata.annotation.typ {
                     let pos = v.pos;
-                    let contract = RuntimeContract::try_from(labeled_ty.clone())?;
+                    let contract = RuntimeContract::from_static_type(labeled_ty.clone())?;
                     Ok(contract.apply(v, pos))
                 } else {
                     Ok(v)

core/src/typ.rs

@@ -927,6 +927,99 @@ impl Type {
         .unwrap()
     }
 
+    /// Static typing guarantees make some of the contract checks useless, assuming that blame
+    /// safety holds. This function simplifies `self` for contract generation, assuming it is part
+    /// of a static type annotation, by eliding some of these useless subcontracts.
+    ///
+    /// # Simplifications
+    ///
+    /// - `forall`s in positive positions are removed, and the corresponding type variable is
+    ///   substituted for a `Dyn` contract. In consequence, [Self::contract()] will generate
+    ///   optimized contracts as well (for example, `forall a. Array a -> a` becomes `Array Dyn ->
+    ///   Dyn`, where `Array Dyn` will be translated to `$array_dyn` which has a constant-time
+    ///   overhead while `Array a` is linear in the size of the array.
+    /// - All positive occurrences of first order contracts (that is, anything but a function type)
+    /// are turned to `Dyn` contracts.
+    fn optimize_static(self) -> Self {
+        fn optimize_rrows(
+            rrows: RecordRows,
+            vars_elide: &HashSet<LocIdent>,
+            polarity: Polarity,
+        ) -> RecordRows {
+            RecordRows(rrows.0.map(
+                |typ| Box::new(optimize(*typ, vars_elide, polarity)),
+                |rrows| Box::new(optimize_rrows(*rrows, vars_elide, polarity)),
+            ))
+        }
+
+        fn optimize(typ: Type, vars_elide: &HashSet<LocIdent>, polarity: Polarity) -> Type {
+            let mut pos = typ.pos;
+
+            let optimized = match typ.typ {
+                TypeF::Arrow(dom, codom) => TypeF::Arrow(
+                    Box::new(optimize(*dom, vars_elide, polarity.flip())),
+                    Box::new(optimize(*codom, vars_elide, polarity)),
+                ),
+                // TODO: don't optimize only VarKind::Type
+                TypeF::Forall {
+                    var,
+                    var_kind: VarKind::Type,
+                    body,
+                } if polarity == Polarity::Positive => {
+                    let mut var_owned = vars_elide.clone();
+                    var_owned.insert(var);
+                    let result = optimize(*body, &var_owned, polarity);
+                    // we keep the position of the body, not the one of the forall
+                    pos = result.pos;
+                    result.typ
+                }
+                TypeF::Forall {
+                    var,
+                    var_kind,
+                    body,
+                } => TypeF::Forall {
+                    var,
+                    var_kind,
+                    body: Box::new(optimize(*body, vars_elide, polarity)),
+                },
+                TypeF::Var(id) if vars_elide.contains(&id) => TypeF::Dyn,
+                v @ TypeF::Var(_) => v,
+                // Any first-order type on positive position can be elided
+                _ if matches!(polarity, Polarity::Positive) => TypeF::Dyn,
+                // Otherwise, we still recurse into non-primitive types
+                TypeF::Record(rrows) => TypeF::Record(optimize_rrows(rrows, vars_elide, polarity)),
+                TypeF::Dict {
+                    type_fields,
+                    flavour,
+                } => TypeF::Dict {
+                    type_fields: Box::new(optimize(*type_fields, vars_elide, polarity)),
+                    flavour,
+                },
+                TypeF::Array(t) => TypeF::Array(Box::new(optimize(*t, vars_elide, polarity))),
+                // All other types don't contain subtypes, it's a base case
+                t => t,
+            };
+
+            Type {
+                typ: optimized,
+                pos,
+            }
+        }
+
+        optimize(self, &HashSet::new(), Polarity::Positive)
+    }
+
+    /// Return the contract corresponding to a type which appears in a static type annotation. Said
+    /// contract must then be applied using the `ApplyContract` primitive operation.
+    ///
+    /// [Self::contract_static] uses the fact that the checked term has been typechecked to
+    /// optimize the generated contract.
+    pub fn contract_static(self) -> Result<RichTerm, UnboundTypeVariableError> {
+        let mut sy = 0;
+        self.optimize_static()
+            .subcontract(HashMap::new(), Polarity::Positive, &mut sy)
+    }
+
     /// Return the contract corresponding to a type, either as a function or a record. Said
     /// contract must then be applied using the `ApplyContract` primitive operation.
     pub fn contract(&self) -> Result<RichTerm, UnboundTypeVariableError> {
@@ -966,10 +1059,24 @@ impl Type {
             TypeF::Number => internals::num(),
             TypeF::Bool => internals::bool(),
             TypeF::String => internals::string(),
-            //TODO: optimization: have a specialized contract for `Array Dyn`, to avoid mapping an
-            //always successful contract on each element.
+            // Array Dyn is specialized to array_dyn, which is constant time
+            TypeF::Array(ref ty) if matches!(ty.typ, TypeF::Dyn) => internals::array_dyn(),
             TypeF::Array(ref ty) => mk_app!(internals::array(), ty.subcontract(vars, pol, sy)?),
             TypeF::Symbol => panic!("Are you trying to check a Sym at runtime?"),
+            // Similarly, any variant of `A -> B` where either `A` or `B` is `Dyn` get specialized
+            // to the corresponding builtin contract.
+            TypeF::Arrow(ref s, ref t) if matches!((&s.typ, &t.typ), (TypeF::Dyn, TypeF::Dyn)) => {
+                internals::func_dyn()
+            }
+            TypeF::Arrow(ref s, ref t) if matches!(s.typ, TypeF::Dyn) => {
+                mk_app!(internals::func_codom(), t.subcontract(vars, pol, sy)?)
+            }
+            TypeF::Arrow(ref s, ref t) if matches!(t.typ, TypeF::Dyn) => {
+                mk_app!(
+                    internals::func_dom(),
+                    s.subcontract(vars.clone(), pol.flip(), sy)?
+                )
+            }
             TypeF::Arrow(ref s, ref t) => mk_app!(
                 internals::func(),
                 s.subcontract(vars.clone(), pol.flip(), sy)?,
@@ -1016,6 +1123,12 @@ impl Type {
             }
             TypeF::Enum(ref erows) => erows.subcontract()?,
             TypeF::Record(ref rrows) => rrows.subcontract(vars, pol, sy)?,
+            // `{_: Dyn}` and `{_ | Dyn}` are equivalent, and both specialied to the constant-time
+            // `dict_dyn`.
+            TypeF::Dict {
+                ref type_fields,
+                flavour: _,
+            } if matches!(type_fields.typ, TypeF::Dyn) => internals::dict_dyn(),
             TypeF::Dict {
                 ref type_fields,
                 flavour: DictTypeFlavour::Contract,

core/stdlib/internals.ncl

@@ -2,7 +2,7 @@
   # Internal operations. Can't be accessed from user code because `$` is not a
   # valid starting character for an identifier.
 
-  # Contract implementations
+  # Builtin contract implementations
   "$dyn" = fun _label value => value,
 
   "$num" = fun label value => if %typeof% value == 'Number then value else %blame% label,
@@ -19,9 +19,58 @@
     else
       %blame% label,
 
+  # A specialized version of `$array $dyn`, but which is constant time.
+  "$array_dyn" = fun label value =>
+    if %typeof% value == 'Array then
+      value
+    else
+      %blame% label,
+
   "$func" = fun domain codomain label value =>
     if %typeof% value == 'Function then
-      (fun x => %apply_contract% codomain (%go_codom% label) (value (%apply_contract% domain (%chng_pol% (%go_dom% label)) x)))
+      (
+        fun x =>
+          %apply_contract%
+            codomain
+            (%go_codom% label)
+            (value (%apply_contract% domain (%chng_pol% (%go_dom% label)) x))
+      )
+    else
+      %blame% label,
+
+  # A specialied version of `_ -> Dyn`
+  "$func_dom" = fun domain label value =>
+    if %typeof% value == 'Function then
+      (
+        fun x =>
+          value
+            (
+              %apply_contract%
+                domain
+                (%chng_pol% (%go_dom% label))
+                x
+            )
+      )
+    else
+      %blame% label,
+
+  # A specialied version of `Dyn -> _`
+  "$func_codom" = fun codomain label value =>
+    if %typeof% value == 'Function then
+      (
+        fun x =>
+          %apply_contract%
+            codomain
+            (%go_codom% label)
+            (value x)
+      )
+    else
+      %blame% label,
+
+  # A specialied version of `Dyn -> Dyn`
+  "$func_dyn" = fun label value =>
+    if %typeof% value == 'Function then
+      value
     else
       %blame% label,
 
@@ -116,6 +165,14 @@
     else
       %blame% (%label_with_message% "not a record" label),
 
+  # A specialized version of either `{_ | Dyn}` or `{_ : Dyn}` (which are
+  # equivalent), but which is constant time.
+  "$dict_dyn" = fun label value =>
+    if %typeof% value == 'Record then
+      value
+    else
+      %blame% (%label_with_message% "not a record" label),
+
   "$forall_tail" = fun sealing_key constr acc label value =>
     let current_polarity = %polarity% label in
     let polarity = (%lookup_type_variable% sealing_key label).polarity in

doc/manual/syntax.md

@@ -822,7 +822,7 @@ parsed as such:
 ```nickel #repl
 > let MyDyn = fun label value => value in
     {foo = 1, bar | MyDyn = "foo"} : {foo : Number, bar : MyDyn}
-{ bar = "foo", foo = 1, }
+{ bar | MyDyn = "foo", foo = 1, }
 ```
 
 ## Metadata