Skip to content

Commit

Permalink
Do not evaluate types away (tweag#1954)
Browse files Browse the repository at this point in the history
Before this change, types used in a term would be evaluated away to
their corresponding contract (a function) automatically. Note that the
only meaningful usage of types right now is to pass them as argument for
`std.contract.apply`.

This eager conversion loses information; either for error messages (for
example, using a type in the wrong place will complain that something
has type "function" and might point to inside Nickel internals instead
of the actual user-written type). Moreover, in preparation for boolean
combinators for contracts, we want to be able to remember the original
form of a type as much as possible.

Finally, it might be useful for users to introspect types as well, for
example to implement custom contract combinators.

For all these reasons, and because there's no apparent drawback, this
commit makes type normal values, that aren't evaluated further. A new
case in the `%contrat/apply%` primop simply performs the conversion to
contract lazily, once they are actually applied, instead of where they
are defined. `%typeof%` and `std.typeof` are updated accordingly with
the new `'Type` tag.
  • Loading branch information
yannham authored Jun 12, 2024
1 parent 808b268 commit c7fc4a1
Show file tree
Hide file tree
Showing 6 changed files with 13 additions and 9 deletions.
3 changes: 2 additions & 1 deletion core/src/closurize.rs
Original file line number Diff line number Diff line change
Expand Up @@ -290,7 +290,8 @@ pub fn should_share(t: &Term) -> bool {
| Term::Enum(_)
| Term::Fun(_, _)
// match acts like a function, and is a WHNF
| Term::Match {..} => false,
| Term::Match {..}
| Term::Type(_) => false,
_ => true,
}
}
Expand Down
5 changes: 0 additions & 5 deletions core/src/eval/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -859,11 +859,6 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
env,
}
}
// Evaluating a type turns it into a contract.
Term::Type(ty) => Closure {
body: ty.contract()?,
env,
},
// Function call if there's no continuation on the stack (otherwise, the function
// is just an argument to a primop or to put in the eval cache)
Term::Fun(x, t) if !has_cont_on_stack => {
Expand Down
5 changes: 5 additions & 0 deletions core/src/eval/operation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -236,6 +236,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
Term::Array(..) => "Array",
Term::Record(..) | Term::RecRecord(..) => "Record",
Term::Lbl(..) => "Label",
Term::Type(_) => "Type",
Term::ForeignId(_) => "ForeignId",
_ => "Other",
};
Expand Down Expand Up @@ -1527,6 +1528,10 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
);

match *t1 {
Term::Type(ref typ) => Ok(Closure {
body: typ.contract()?,
env: env1,
}),
Term::Fun(..) | Term::Match { .. } => Ok(Closure {
body: RichTerm {
term: t1,
Expand Down
4 changes: 2 additions & 2 deletions core/src/term/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -894,6 +894,7 @@ impl Term {
Term::SealingKey(_) => Some("SealingKey".to_owned()),
Term::Sealed(..) => Some("Sealed".to_owned()),
Term::Annotated(..) => Some("Annotated".to_owned()),
Term::Type(_) => Some("Type".to_owned()),
Term::ForeignId(_) => Some("ForeignId".to_owned()),
Term::Let(..)
| Term::LetPattern(..)
Expand All @@ -906,7 +907,6 @@ impl Term {
| Term::Import(_)
| Term::ResolvedImport(_)
| Term::StrChunks(_)
| Term::Type(_)
| Term::ParseError(_)
| Term::RuntimeError(_) => None,
}
Expand Down Expand Up @@ -941,6 +941,7 @@ impl Term {
| Term::EnumVariant {..}
| Term::Record(..)
| Term::Array(..)
| Term::Type(_)
| Term::ForeignId(_)
| Term::SealingKey(_) => true,
Term::Let(..)
Expand All @@ -958,7 +959,6 @@ impl Term {
| Term::ResolvedImport(_)
| Term::StrChunks(_)
| Term::RecRecord(..)
| Term::Type(_)
| Term::ParseError(_)
| Term::RuntimeError(_) => false,
}
Expand Down
4 changes: 3 additions & 1 deletion core/src/typecheck/operation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,8 @@ pub fn get_uop_type(
mk_uty_arrow!(branches.clone(), branches.clone(), branches),
)
}
// Dyn -> [| 'Number, 'Bool, 'String, 'Enum, 'Function, 'Array, 'Record, 'Label, 'Other |]
// Dyn -> [| 'Number, 'Bool, 'String, 'Enum, 'Function, 'Array, 'Record, 'Label,
// 'ForeignId, 'Type, 'Other |]
UnaryOp::Typeof => (
mk_uniftype::dynamic(),
mk_uty_enum!(
Expand All @@ -37,6 +38,7 @@ pub fn get_uop_type(
"Record",
"Label",
"ForeignId",
"Type",
"Other"
),
),
Expand Down
1 change: 1 addition & 0 deletions core/stdlib/std.ncl
Original file line number Diff line number Diff line change
Expand Up @@ -3367,6 +3367,7 @@
'Array,
'Record,
'ForeignId,
'Type,
'Other
|]
| doc m%"
Expand Down

0 comments on commit c7fc4a1

Please sign in to comment.