Skip to content

Commit

Permalink
Remove the double contract application introduced in #1194 (#1625)
Browse files Browse the repository at this point in the history
Because of #1228 we syntactically forbid contracts from containing free
type variables. This was implemented in #1271 and #1272. As a result,
the double contract application in #1194 became dead code. This PR
removes the `%dualize%` primop, the `dualize` field in `Label` and the
double application logic when constructing recursive environments for
records.
  • Loading branch information
vkleen authored Sep 22, 2023
1 parent bcb0f71 commit f3d7430
Show file tree
Hide file tree
Showing 8 changed files with 4 additions and 77 deletions.
40 changes: 2 additions & 38 deletions core/src/eval/fixpoint.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
//! Compute the fixpoint of a recursive record.
use super::{merge::RevertClosurize, *};
use crate::{label::Label, position::TermPos};
use crate::position::TermPos;

// Update the environment of a term by extending it with a recursive environment. In the general
// case, the term is expected to be a variable pointing to the element to be patched. Otherwise,
Expand Down Expand Up @@ -87,43 +87,7 @@ pub fn rec_env<'a, I: Iterator<Item = (&'a LocIdent, &'a Field)>, C: Cache>(

let with_ctr_applied = RuntimeContract::apply_all(
RichTerm::new(Term::Var(id_value), value.pos),
field.pending_contracts.iter().cloned().flat_map(|ctr| {
// This operation is the heart of our preliminary fix for
// [#1161](https://github.com/tweag/nickel/issues/1161). Whenever we detect
// the presence of free type variables in a contract, by witnessing a
// nonempty type environment in the label, we need to not just apply the
// original contract but also its dual. The rationale here is that a record
// field that recursively depends on another of type `T`, say, should be
// considered a function with domain `T`. Consequently, the same contract
// that would be a applied to the argument of a function of type `T -> Dyn`
// should be applied to the recursive reference.
//
// Thus, the recursive reference must satisfy the contract for `T` as well
// as the "dual" contract `T.dualize()`; the latter is defined to be the
// domain contract for a function of type `T -> Dyn`. This sublety only
// matters if `T` contains free type variables because only then does
// `T.dualize()` differ from `T` at all.
//
// We expect to implement a way of solving this dilemma without essentially
// applying every contract twice. This will likely involve a rewriting of
// contracts corresponding to free variables which is yet to be proved
// sound.
if ctr.label.type_environment.is_empty() {
vec![ctr]
} else {
vec![
ctr.clone(),
RuntimeContract {
contract: ctr.contract,
label: Label {
polarity: ctr.label.polarity.flip(),
dualize: true,
..ctr.label
},
},
]
}
}),
field.pending_contracts.iter().cloned(),
value.pos,
);

Expand Down
12 changes: 0 additions & 12 deletions core/src/eval/operation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1155,18 +1155,6 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
Err(mk_type_error!("label_push_diag", "Label"))
}}
}
UnaryOp::Dualize() => {
match_sharedterm! {t, with {
Term::Lbl(label) => {
Ok(Closure::atomic_closure(RichTerm::new(
Term::Bool(label.dualize),
pos_op_inh,
)))
}
} else {
Err(mk_type_error!("dualize", "Label"))
}}
}
}
}

Expand Down
5 changes: 0 additions & 5 deletions core/src/label.rs
Original file line number Diff line number Diff line change
Expand Up @@ -303,10 +303,6 @@ pub struct Label {
/// polymorphic contracts to decide which actions to take when encountering a `forall`.
pub type_environment: HashMap<SealingKey, TypeVarData>,

/// Signal to a polymorphic contract that it should generate the dual contract. Part of the
/// preliminary fix for [#1161](https://github.com/tweag/nickel/issues/1161).
pub dualize: bool,

/// The name of the record field to report in blame errors. This is set
/// while first transforming a record as part of the pending contract generation.
/// Contract applications outside of records will have this field set to `None`.
Expand Down Expand Up @@ -523,7 +519,6 @@ impl Default for Label {
arg_pos: Default::default(),
path: Default::default(),
type_environment: Default::default(),
dualize: false,
field_name: None,
}
}
Expand Down
2 changes: 0 additions & 2 deletions core/src/parser/grammar.lalrpop
Original file line number Diff line number Diff line change
Expand Up @@ -667,7 +667,6 @@ UOp: UnaryOp = {
"record_empty_with_tail" => UnaryOp::RecordEmptyWithTail(),
"trace" => UnaryOp::Trace(),
"label_push_diag" => UnaryOp::LabelPushDiag(),
"dualize" => UnaryOp::Dualize(),
};

MatchCase: MatchCase = {
Expand Down Expand Up @@ -1051,7 +1050,6 @@ extern {
"trace" => Token::Normal(NormalToken::Trace),
"insert_type_variable" => Token::Normal(NormalToken::InsertTypeVar),
"lookup_type_variable" => Token::Normal(NormalToken::LookupTypeVar),
"dualize" => Token::Normal(NormalToken::Dualize),

"has_field" => Token::Normal(NormalToken::HasField),
"map" => Token::Normal(NormalToken::Map),
Expand Down
2 changes: 0 additions & 2 deletions core/src/parser/lexer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -210,8 +210,6 @@ pub enum NormalToken<'input> {
InsertTypeVar,
#[token("%lookup_type_variable%")]
LookupTypeVar,
#[token("%dualize%")]
Dualize,

#[token("%seal%")]
Seal,
Expand Down
6 changes: 0 additions & 6 deletions core/src/term/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1174,11 +1174,6 @@ pub enum UnaryOp {
/// This primop shouldn't be used directly by user a priori, but is used internally during e.g.
/// contract application.
LabelPushDiag(),

/// Return the value of the `dualize` field in a label. Used by polymorphic contracts to check
/// if they are being invoked to generate a dual contract, as part of the preliminary fix for
/// [#1161](https://github.com/tweag/nickel/issues/1161).
Dualize(),
}

impl fmt::Display for UnaryOp {
Expand Down Expand Up @@ -1227,7 +1222,6 @@ impl fmt::Display for UnaryOp {
RecordEmptyWithTail() => write!(f, "record_empty_with_tail"),
Trace() => write!(f, "trace"),
LabelPushDiag() => write!(f, "label_push_diag"),
Dualize() => write!(f, "dualize"),
}
}
}
Expand Down
3 changes: 0 additions & 3 deletions core/src/typecheck/operation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -207,9 +207,6 @@ pub fn get_uop_type(
// Morally: Lbl -> Lbl
// Actual: Dyn -> Dyn
UnaryOp::LabelPushDiag() => (mk_uniftype::dynamic(), mk_uniftype::dynamic()),
// Morally: Lbl -> Bool
// Actual: Dyn -> Bool
UnaryOp::Dualize() => (mk_uniftype::dynamic(), mk_uniftype::bool()),
})
}

Expand Down
11 changes: 2 additions & 9 deletions core/stdlib/internals.ncl
Original file line number Diff line number Diff line change
Expand Up @@ -37,15 +37,8 @@
# blaming polymorphic contracts.
%seal% sealing_key (%chng_pol% label) value,

"$forall" =
let flip = match {
'Positive => 'Negative,
'Negative => 'Positive,
}
in
fun sealing_key polarity contract label value =>
let polarity = if %dualize% label then flip polarity else polarity in
contract (%insert_type_variable% sealing_key polarity label) value,
"$forall" = fun sealing_key polarity contract label value =>
contract (%insert_type_variable% sealing_key polarity label) value,

"$enums" = fun case label value =>
if %typeof% value == 'Enum then
Expand Down

0 comments on commit f3d7430

Please # to comment.