Skip to content

Commit

Permalink
Introduce validators for building custom contracts (#1970)
Browse files Browse the repository at this point in the history
* Add validator as a form of custom contract

* Support validators in %contract/apply%

* Add from_validator primop and stdlib function

* Add tests for custom contract constructors

* Migrate stdlib to use validators

* Add documentation on validators

* Fix manual snippets

* Apply suggestions from code review

Co-authored-by: jneem <joeneeman@gmail.com>

---------

Co-authored-by: jneem <joeneeman@gmail.com>
  • Loading branch information
yannham and jneem authored Jun 24, 2024
1 parent dd0ccb1 commit 9969d9a
Show file tree
Hide file tree
Showing 23 changed files with 444 additions and 174 deletions.
12 changes: 12 additions & 0 deletions cli/tests/snapshot/inputs/errors/validator_custom_error.ncl
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
# capture = 'stderr'
# command = ['eval']
let Is42 = std.contract.from_validator (fun value =>
if value == 42 then
'Ok value
else
'Error {
message = "Value must be 42",
notes = ["This is a first custom note", "This is a second custom note"]
}
) in
43 | Is42
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
---
source: cli/tests/snapshot/main.rs
expression: err
---
error: contract broken by a value
Value must be 42
┌─ [INPUTS_PATH]/errors/validator_custom_error.ncl:12:1
1243 | Is42
^^ ---- expected type
│ │
applied to this expression
= This is a first custom note
= This is a second custom note
24 changes: 24 additions & 0 deletions core/src/eval/operation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1214,6 +1214,25 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
))
}
}
UnaryOp::ContractFromValidator => {
if matches!(&*t, Term::Fun(..) | Term::Match(_)) {
Ok(Closure {
body: RichTerm::new(
Term::CustomContract(CustomContract::Validator(RichTerm {
term: t,
pos,
})),
pos,
),
env,
})
} else {
Err(mk_type_error!(
"contract/from_validator",
"Function or MatchExpression"
))
}
}
UnaryOp::ContractCustom => {
if matches!(&*t, Term::Fun(..) | Term::Match(_)) {
Ok(Closure {
Expand Down Expand Up @@ -1588,6 +1607,11 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
.with_pos(pos1),
env: env1,
}),
Term::CustomContract(CustomContract::Validator(validator)) => Ok(Closure {
body: mk_app!(internals::validator_to_ctr(), validator.clone())
.with_pos(pos1),
env: env1,
}),
Term::Record(..) => {
let closurized = RichTerm {
term: t1,
Expand Down
2 changes: 2 additions & 0 deletions core/src/parser/grammar.lalrpop
Original file line number Diff line number Diff line change
Expand Up @@ -1082,6 +1082,7 @@ UOp: UnaryOp = {
"label/go_array" => UnaryOp::LabelGoArray,
"label/go_dict" => UnaryOp::LabelGoDict,
"contract/from_predicate" => UnaryOp::ContractFromPredicate,
"contract/from_validator" => UnaryOp::ContractFromValidator,
"contract/custom" => UnaryOp::ContractCustom,
"enum/embed" <Ident> => UnaryOp::EnumEmbed(<>),
"array/map" => UnaryOp::ArrayMap,
Expand Down Expand Up @@ -1515,6 +1516,7 @@ extern {
"contract/array_lazy_app" => Token::Normal(NormalToken::ContractArrayLazyApp),
"contract/record_lazy_app" => Token::Normal(NormalToken::ContractRecordLazyApp),
"contract/from_predicate" => Token::Normal(NormalToken::ContractFromPredicate),
"contract/from_validator" => Token::Normal(NormalToken::ContractFromValidator),
"contract/custom" => Token::Normal(NormalToken::ContractCustom),
"op force" => Token::Normal(NormalToken::OpForce),
"blame" => Token::Normal(NormalToken::Blame),
Expand Down
2 changes: 2 additions & 0 deletions core/src/parser/lexer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -202,6 +202,8 @@ pub enum NormalToken<'input> {
ContractRecordLazyApp,
#[token("%contract/from_predicate%")]
ContractFromPredicate,
#[token("%contract/from_validator%")]
ContractFromValidator,
#[token("%contract/custom%")]
ContractCustom,
#[token("%blame%")]
Expand Down
32 changes: 19 additions & 13 deletions core/src/pretty.rs
Original file line number Diff line number Diff line change
Expand Up @@ -142,7 +142,7 @@ fn needs_parens_in_type_pos(typ: &Type) -> bool {
term.as_ref(),
Term::Fun(..)
| Term::FunPattern(..)
| Term::CustomContract(CustomContract::Predicate(..))
| Term::CustomContract(_)
| Term::Let(..)
| Term::LetPattern(..)
| Term::Op1(UnaryOp::IfThenElse, _)
Expand Down Expand Up @@ -821,22 +821,28 @@ where
Str(v) => allocator.escaped_string(v).double_quotes(),
StrChunks(chunks) => allocator.chunks(chunks, StringRenderStyle::Multiline),
Fun(id, body) => allocator.function(allocator.as_string(id), body),
CustomContract(ContractNode::PartialIdentity(ctr)) => docs![
allocator,
"%contract/custom%",
docs![allocator, allocator.line(), ctr.pretty(allocator).parens()]
// Format this as the primop application `<custom contract constructor> <contract impl>`.
CustomContract(contract_node) => {
let (constructor, contract) = match contract_node {
ContractNode::Predicate(p) => ("%contract/from_predicate%", p),
ContractNode::Validator(v) => ("%contract/from_validator%", v),
ContractNode::PartialIdentity(pid) => ("%contract/custom%", pid),
};

docs![
allocator,
constructor,
docs![
allocator,
allocator.line(),
contract.pretty(allocator).parens()
]
.nest(2)
.group()
],
]
}
FunPattern(pat, body) => allocator.function(allocator.pat_with_parens(pat), body),
// Format this as the application `std.contract.from_predicate <pred>`.
CustomContract(ContractNode::Predicate(pred)) => docs![
allocator,
"%contract/from_predicate%",
docs![allocator, allocator.line(), pred.pretty(allocator).parens()]
.nest(2)
.group()
],
Lbl(_lbl) => allocator.text("%<label>").append(allocator.line()),
Let(id, rt, body, attrs) => docs![
allocator,
Expand Down
1 change: 1 addition & 0 deletions core/src/stdlib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -103,6 +103,7 @@ pub mod internals {
generate_accessor!(stdlib_contract_equal);

generate_accessor!(predicate_to_ctr);
generate_accessor!(validator_to_ctr);

generate_accessor!(rec_default);
generate_accessor!(rec_force);
Expand Down
55 changes: 35 additions & 20 deletions core/src/term/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -216,23 +216,24 @@ pub enum Term {
#[serde(skip)]
Type(Type),

/// A custom contract built using e.g. `std.contract.from_predicate`. Currently, custom
/// contracts can be partial identities (the most general form, which either blame or return
/// the value with potential delayed checks buried inside) or a predicate. Ideally, both
/// would fall under then `CustomContract` node.
///
/// Custom contracts built from `std.contract.custom` are stored in this node. Note that, for
/// backward compatibility, users can also use naked functions [Term::Fun] as a custom
/// contract. But this is discouraged and will be deprecated in the future.
///
/// The reason for having a separate node is that we can leverage the metadata for example to
/// implement a restricted `or` combinator on contracts, which needs to know which contracts
/// are built from predicates, or for better error messages in the future when parametric
/// contracts aren't fully applied ([#1460](https://github.com/tweag/nickel/issues/1460)).
///
/// Also, custom contracts aren't supposed to be applied using the standard function
/// application, because we need to perform additional bookkeeping upon application. So there's
/// no strong incentive to represent them as naked functions.
/// A custom contract built.
///
/// Custom contracts can be partial identities (the most general form, which either blame or
/// return the value with potential delayed checks buried inside), predicates or validator (see
/// [CustomContract].
///
/// Partial identity are built using `std.contract.custom`. Note that, for backward
/// compatibility, users can also use naked functions ([Term::Fun]) for partial identities
/// instead. But this is discouraged and will be deprecated in the future. Indeed, custom
/// contracts aren't supposed to be applied using the standard function application, because we
/// need to perform additional bookkeeping upon application, so there's no good reason to
/// represent them as naked functions.
///
/// Having a separate node lets us leverage the additional information for example to implement
/// a restricted `or` combinator on contracts, which needs to know which contracts support
/// booleans operations (predicates and validators), or for better error messages in the future
/// when parametric contracts aren't fully applied
/// ([#1460](https://github.com/tweag/nickel/issues/1460)).
#[serde(skip)]
CustomContract(CustomContract),

Expand Down Expand Up @@ -401,12 +402,16 @@ pub enum BindingType {
/// better error messages in some situations.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub enum CustomContract {
/// A generic custom contract, represented as a partial identity function of type `Label -> Dyn
/// -> Dyn`.
PartialIdentity(RichTerm),
/// A contract built from a predicate. The argument is a function of type
/// `Dyn -> Bool`.
Predicate(RichTerm),
/// A contract built from a validator. A validator is a function of type `Dyn -> [| 'Ok, 'Error
/// ReifiedLabel |]` where `ReifiedLabel` is a record with error reporting data (a message,
/// notes, etc.)
Validator(RichTerm),
/// A generic custom contract, represented as a partial identity function of type `Label -> Dyn
/// -> Dyn`.
PartialIdentity(RichTerm),
}

/// A runtime representation of a contract, as a term and a label ready to be applied via
Expand Down Expand Up @@ -1309,6 +1314,10 @@ pub enum UnaryOp {
/// a type constructor for custom contracts.
ContractFromPredicate,

/// Wrap a validator function as a [CustomContract]. You can think of this primop as a type
/// constructor for custom contracts.
ContractFromValidator,

/// Wrap a partial identity function as a [CustomContract]. You can think of this primop as a
/// type constructor for contracts.
ContractCustom,
Expand Down Expand Up @@ -1524,6 +1533,7 @@ impl fmt::Display for UnaryOp {
LabelGoArray => write!(f, "label/go_array"),
LabelGoDict => write!(f, "label/go_dict"),
ContractFromPredicate => write!(f, "contract/from_predicate"),
ContractFromValidator => write!(f, "contract/from_validator"),
ContractCustom => write!(f, "contract/custom"),
Seq => write!(f, "seq"),
DeepSeq => write!(f, "deep_seq"),
Expand Down Expand Up @@ -2109,6 +2119,10 @@ impl Traverse<RichTerm> for RichTerm {
let t = t.traverse(f, order)?;
RichTerm::new(Term::CustomContract(CustomContract::Predicate(t)), pos)
}
Term::CustomContract(CustomContract::Validator(t)) => {
let t = t.traverse(f, order)?;
RichTerm::new(Term::CustomContract(CustomContract::Validator(t)), pos)
}
Term::CustomContract(CustomContract::PartialIdentity(t)) => {
let t = t.traverse(f, order)?;
RichTerm::new(
Expand Down Expand Up @@ -2308,6 +2322,7 @@ impl Traverse<RichTerm> for RichTerm {
Term::Fun(_, t)
| Term::FunPattern(_, t)
| Term::CustomContract(CustomContract::Predicate(t))
| Term::CustomContract(CustomContract::Validator(t))
| Term::CustomContract(CustomContract::PartialIdentity(t))
| Term::EnumVariant { arg: t, .. }
| Term::Op1(_, t)
Expand Down
1 change: 1 addition & 0 deletions core/src/transform/free_vars.rs
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,7 @@ impl CollectFreeVars for RichTerm {
| Term::Sealed(_, t, _)
| Term::EnumVariant { arg: t, .. }
| Term::CustomContract(CustomContract::Predicate(t))
| Term::CustomContract(CustomContract::Validator(t))
| Term::CustomContract(CustomContract::PartialIdentity(t)) => {
t.collect_free_vars(free_vars)
}
Expand Down
2 changes: 1 addition & 1 deletion core/src/typecheck/mk_uniftype.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ macro_rules! mk_uty_arrow {
/// Multi-ary enum row constructor for types implementing `Into<TypeWrapper>`.
/// `mk_uty_enum_row!(id1, .., idn; tail)` correspond to `[| 'id1, .., 'idn; tail |]. With the
/// addition of algebraic data types (enum variants), individual rows can also take an additional
/// type parameter, specificed as a tuple: for example, `mk_uty_enum_row!(id1, (id2, ty2); tail)`
/// type parameter, specified as a tuple: for example, `mk_uty_enum_row!(id1, (id2, ty2); tail)`
/// is `[| 'id1, 'id2 ty2; tail |]`.
#[macro_export]
macro_rules! mk_uty_enum_row {
Expand Down
21 changes: 15 additions & 6 deletions core/src/typecheck/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1600,8 +1600,9 @@ fn walk<V: TypecheckVisitor>(
Term::EnumVariant { arg: t, ..}
| Term::Sealed(_, t, _)
| Term::Op1(_, t)
| Term::CustomContract(CustomContract::Predicate(t)) | Term::CustomContract(CustomContract::PartialIdentity(t))
=> walk(state, ctxt.clone(), visitor, t),
| Term::CustomContract(CustomContract::Predicate(t))
| Term::CustomContract(CustomContract::Validator(t))
| Term::CustomContract(CustomContract::PartialIdentity(t)) => walk(state, ctxt.clone(), visitor, t),
Term::Op2(_, t1, t2) => {
walk(state, ctxt.clone(), visitor, t1)?;
walk(state, ctxt, visitor, t2)
Expand Down Expand Up @@ -1925,7 +1926,7 @@ fn check<V: TypecheckVisitor>(
// Additionally, because this rule can't produce a polymorphic type (it produces a `Dyn`,
// or morally a `Contract` type, if we had one), we don't lose anything by making it a
// check rule, as for e.g. literals.
Term::CustomContract(CustomContract::Predicate(body)) => {
Term::CustomContract(CustomContract::Predicate(t)) => {
// The overall type of a custom contract is currently `Dyn`, as we don't have a better
// one.
ty.unify(mk_uniftype::dynamic(), state, &ctxt)
Expand All @@ -1936,13 +1937,21 @@ fn check<V: TypecheckVisitor>(
state,
ctxt,
visitor,
body,
t,
mk_uniftype::arrow(mk_uniftype::dynamic(), mk_uniftype::bool()),
)
}
Term::CustomContract(CustomContract::Validator(t)) => {
// The overall type of a custom contract is currently `Dyn`, as we don't have a better
// one.
ty.unify(mk_uniftype::dynamic(), state, &ctxt)
.map_err(|err| err.into_typecheck_err(state, rt.pos))?;

check(state, ctxt, visitor, t, operation::validator_type())
}
// See [^predicate-is-check]. We took `Predicate` as an example, but this reasoning applies
// to other kind of custom contracts, such as `PartialIdentity`.
Term::CustomContract(CustomContract::PartialIdentity(body)) => {
Term::CustomContract(CustomContract::PartialIdentity(t)) => {
// The overall type of a custom contract is currently `Dyn`, as we don't have a better
// one.
ty.unify(mk_uniftype::dynamic(), state, &ctxt)
Expand All @@ -1956,7 +1965,7 @@ fn check<V: TypecheckVisitor>(
mk_uniftype::dynamic()
);

check(state, ctxt, visitor, body, partial_id_type)
check(state, ctxt, visitor, t, partial_id_type)
}
Term::Array(terms, _) => {
let ty_elts = state.table.fresh_type_uvar(ctxt.var_level);
Expand Down
31 changes: 31 additions & 0 deletions core/src/typecheck/operation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -86,6 +86,9 @@ pub fn get_uop_type(
mk_uniftype::dynamic(),
),
// Morally returns a contract, but we don't have a proper type for that yet
// <validator_type()> -> Dyn (see `validator_type()` below for more details)
UnaryOp::ContractFromValidator => (validator_type(), mk_uniftype::dynamic()),
// Morally returns a contract, but we don't have a proper type for that yet
// (Dyn -> Dyn -> Bool) -> Dyn
UnaryOp::ContractCustom => (
mk_uty_arrow!(
Expand Down Expand Up @@ -562,3 +565,31 @@ pub fn get_nop_type(
),
})
}

/// Return the type of a validator, which is one way of representing a custom contract. This static
/// type is more rigid than the actual values accepted by `std.contract.from_validator`, because we
/// can't represent optional fields in the type system. But it's ok to be stricter in statically
/// typed code.
///
/// Also remember that custom contracts shouldn't appear directly in the source code of Nickel:
/// they are built using `std.contract.from_xxx` and `std.contract.custom` functions. We implement
/// typechecking for them mostly because we can (to avoid an `unimplemented!` or a `panic!`), but
/// we don't expect this case to trigger at the moment, so it isn't of the utmost importance.
///
/// The result represents the type `Dyn -> [| 'Ok, 'Error { message: String, notes: Array
/// String } |]`.
pub fn validator_type() -> UnifType {
mk_uty_arrow!(
mk_uniftype::dynamic(),
mk_uty_enum!(
"Ok",
(
"Error",
mk_uty_record!(
("message", mk_uniftype::str()),
("notes", mk_uniftype::array(mk_uniftype::str()))
)
)
)
)
}
Loading

0 comments on commit 9969d9a

Please sign in to comment.