Skip to content

Commit

Permalink
WIP: end of quick-look like approach
Browse files Browse the repository at this point in the history
  • Loading branch information
@yannham
yannham committed Jul 25, 2023
1 parent acd0651 commit fb7feda
Show file tree
Hide file tree
Showing 2 changed files with 69 additions and 76 deletions.
7 changes: 7 additions & 0 deletions core/src/term/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -514,6 +514,7 @@ impl TypeAnnotation {
.collect::<Result<Vec<_>, _>>()
}

/// Set the `field_name` attribute of the labels of the type and contracts annotations.
pub fn with_field_name(self, field_name: Option<Ident>) -> Self {
TypeAnnotation {
types: self.types.map(|t| t.with_field_name(field_name)),
Expand All @@ -524,6 +525,12 @@ impl TypeAnnotation {
.collect(),
}
}

/// Return `true` if this annotation is empty, i.e. hold neither a type annotation nor
/// contracts annotations.
pub fn is_empty(&self) -> bool {
self.types.is_none() && self.contracts.is_empty()
}
}

impl From<TypeAnnotation> for LetMetadata {
Expand Down
138 changes: 62 additions & 76 deletions core/src/typecheck/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,6 @@ use crate::{
environment::Environment as GenericEnvironment,
error::TypecheckError,
identifier::Ident,
position::TermPos,
stdlib as nickel_stdlib,
term::{
record::Field, LabeledType, RichTerm, StrChunk, Term, Traverse, TraverseOrder,
Expand Down Expand Up @@ -1897,14 +1896,12 @@ fn check<L: Linearizer>(
// follow the inference discipline, following the Pfennig recipe and the current type
// system specification (as far as typechecking is concerned, primitive operator
// application is the same as function application).
Term::Var(_)
| Term::Op1(..)
| Term::Op2(..)
| Term::OpN(..) => {
Term::Var(_) | Term::Op1(..) | Term::Op2(..) | Term::OpN(..) | Term::Annotated(..) => {
let inferred = infer(state, ctxt.clone(), lin, linearizer, rt)?;

// We call to `subsumption` to perform the switch from infer mode to checking mode.
subsumption(state, ctxt, inferred, ty).map_err(|err| err.into_typecheck_err(state, rt.pos))
subsumption(state, ctxt, inferred, ty)
.map_err(|err| err.into_typecheck_err(state, rt.pos))
}
Term::Enum(id) => {
let row = state.table.fresh_erows_uvar(ctxt.var_level);
Expand Down Expand Up @@ -2034,8 +2031,7 @@ fn check<L: Linearizer>(
Ok(())
}
}

Term::Annotated(annot, rt) => check_annotated(state, ctxt, lin, linearizer, annot, rt, ty),

Term::SealingKey(_) => ty
.unify(mk_uniftype::sym(), state, &ctxt)
.map_err(|err| err.into_typecheck_err(state, rt.pos)),
Expand Down Expand Up @@ -2102,46 +2098,57 @@ fn check_field<L: Linearizer>(
) -> Result<(), TypecheckError> {
linearizer.add_field_metadata(lin, field);

check_with_annot(
state,
ctxt,
lin,
linearizer,
&field.metadata.annotation,
field.value.as_ref(),
ty,
field.value.as_ref().map(|v| v.pos).unwrap_or(id.pos),
)
// If there's no annotation, we simply check the underlying value, if any.
if field.metadata.annotation.is_empty() {
if let Some(value) = field.value.as_ref() {
check(state, ctxt, lin, linearizer, value, ty)
} else {
// It might make sense to accept any type for a value without definition (which would
// act a bit like a function parameter). But for now, we play safe and implement a more
// restrictive rule, which is that a value without a definition has type `Dyn`
ty.unify(mk_uniftype::dynamic(), state, &ctxt)
.map_err(|err| err.into_typecheck_err(state, id.pos))
}
} else {
let pos = field.value.as_ref().map(|v| v.pos).unwrap_or(id.pos);

let inferred = infer_with_annot(
state,
ctxt.clone(),
lin,
linearizer,
&field.metadata.annotation,
field.value.as_ref(),
)?;

subsumption(state, ctxt, inferred, ty).map_err(|err| err.into_typecheck_err(state, pos))
}
}

fn check_annotated<L: Linearizer>(
fn infer_annotated<L: Linearizer>(
state: &mut State,
ctxt: Context,
lin: &mut Linearization<L::Building>,
linearizer: L,
annot: &TypeAnnotation,
rt: &RichTerm,
ty: UnifType,
) -> Result<(), TypecheckError> {
check_with_annot(state, ctxt, lin, linearizer, annot, Some(rt), ty, rt.pos)
) -> Result<UnifType, TypecheckError> {
infer_with_annot(state, ctxt, lin, linearizer, annot, Some(rt))
}

/// Function handling the common part of typechecking terms with type or contract annotation, with
/// or without definitions. This encompasses both standalone type annotation (where `value` is
/// always `Some(_)`) as well as field definitions (where `value` may or may not be defined).
///
/// The last argument is a position to use for error reporting when `value` is `None`.
/// Function handling the common part of inferring the type of terms with type or contract
/// annotation, with or without definitions. This encompasses both standalone type annotation
/// (where `value` is always `Some(_)`) as well as field definitions (where `value` may or may not
/// be defined).
#[allow(clippy::too_many_arguments)] // TODO: Is it worth doing something about it?
fn check_with_annot<L: Linearizer>(
fn infer_with_annot<L: Linearizer>(
state: &mut State,
ctxt: Context,
lin: &mut Linearization<L::Building>,
mut linearizer: L,
annot: &TypeAnnotation,
value: Option<&RichTerm>,
ty: UnifType,
pos: TermPos,
) -> Result<(), TypecheckError> {
) -> Result<UnifType, TypecheckError> {
annot.iter().try_for_each(|ty| {
walk_type(state, ctxt.clone(), lin, linearizer.scope_meta(), &ty.types)
})?;
Expand All @@ -2157,13 +2164,7 @@ fn check_with_annot<L: Linearizer>(
let uty2 = UnifType::from_type(ty2.clone(), &ctxt.term_env);

check(state, ctxt.clone(), lin, linearizer, value, uty2.clone())?;
// The rule for an annotated term infers. We thus a switch from inference mode (`uty2`
// inferred from the annotation) to checked mode (checking against `ty`) via
// subsumption.
//
// In particular, `uty2` might very well be polymorphic, and thus needs instantiation,
// which is indeed taken care of by subsumption.
subsumption(state, ctxt, uty2, ty).map_err(|err| err.into_typecheck_err(state, pos))
Ok(uty2)
}
// A annotation without a type but with a contract switches the typechecker back to walk
// mode. If there are several contracts, we arbitrarily chose the first one as the apparent
Expand All @@ -2180,24 +2181,18 @@ fn check_with_annot<L: Linearizer>(
let LabeledType { types: ty2, .. } = ctr;

let uty2 = UnifType::from_type(ty2.clone(), &ctxt.term_env);
// subsumption(): cf previous case of the enclosing match (same logic)
subsumption(state, ctxt.clone(), uty2, ty)
.map_err(|err| err.into_typecheck_err(state, pos))?;

// If there's an inner value, we still have to walk it, as it may contain
// statically typed blocks.
// If there's an inner value, we have to walk it, as it may contain statically typed
// blocks.
if let Some(value) = value_opt {
walk(state, ctxt, lin, linearizer, value)
} else {
// TODO: we might have something to with the linearizer to clear the current
// metadata. It looks like it may be unduly attached to the next field definition,
// which is not critical, but still a bug.
Ok(())
walk(state, ctxt, lin, linearizer, value)?;
}

Ok(uty2)
}
// A non-empty value without a type or a contract annotation is typechecked in the same way
// as its inner value
(_, Some(value)) => check(state, ctxt, lin, linearizer, value, ty),
(_, Some(value)) => infer(state, ctxt, lin, linearizer, value),
// A empty value is a record field without definition. We don't check anything, and infer
// its type to be either the first annotation defined if any, or `Dyn` otherwise.
//
Expand All @@ -2209,25 +2204,15 @@ fn check_with_annot<L: Linearizer>(
.first()
.map(|labeled_ty| UnifType::from_type(labeled_ty.types.clone(), &ctxt.term_env))
.unwrap_or_else(mk_uniftype::dynamic);
ty.unify(inferred, state, &ctxt)
.map_err(|err| err.into_typecheck_err(state, pos))
Ok(inferred)
}
}
}

/// Infer a type for an expression.
///
/// `infer` corresponds to the inference mode of bidirectional typechecking. Nickel uses a mix of
/// bidirectional typechecking together with traditional ML-like unification. In practice, to avoid
/// duplicating a lot of rules for both checking mode and inference mode, the current [`check`]
/// function mixes both and inference simply corresponds to checking against a free unification
/// variable.
///
/// There is one important difference, though: because `check` always assumes it implements
/// checking mode, it will call to [subsumption] as well to switch back to checking mode.
///
/// Still, using this dedicated method - although it is a thin wrapper - helps making clear when
/// inference mode is used and when checking mode is used in the typechecking algorithm.
/// bidirectional typechecking and traditional ML-like unification.
fn infer<L: Linearizer>(
state: &mut State,
mut ctxt: Context,
Expand All @@ -2252,11 +2237,11 @@ fn infer<L: Linearizer>(
linearizer.add_term(lin, term, *pos, x_ty.clone());
Ok(x_ty)
}
// Theoretically, we might need to instantiate the type of head of the primop application,
// Theoretically, we need to instantiate the type of the head of the primop application,
// that is, the primop itself. In practice, `get_uop_type`,`get_bop_type` and
// `get_nop_type` returns type that are already instantiated with unification variable, to
// save building polymorphic type to only instantiate them immediately. Thus, in practice,
// the type of a primop is always monomorphic.
// `get_nop_type` return type that are already instantiated with free unification
// variables, to save building a polymorphic type to only instantiate it immediately. Thus,
// the type of a primop is currently always monomorphic.
Term::Op1(op, t) => {
let (ty_arg, ty_res) = get_uop_type(state, ctxt.var_level, op)?;
linearizer.add_term(lin, term, *pos, ty_res.clone());
Expand Down Expand Up @@ -2289,31 +2274,32 @@ fn infer<L: Linearizer>(
}
Term::App(e, t) => {
// If we go the full Quick Look route (cf [quick-look] and the Nickel type system
// specification), we will have a more advanced and specific process to guess the
// instantiation of the potential polymorphic type of the head of the application.
// Currently, we limit ourselves to predicative instantiation, and we can get by
// instantiating heading `foralls` with fresh unification variables.
// specification), we will have a more advanced and specific rule to guess the
// instantiation of the potentially polymorphic type of the head of the application.
// Currently, we limit ourselves to predicative instantiation, and we can get away
// by eagerly instantiating heading `foralls` with fresh unification variables.
let head_poly = infer(state, ctxt.clone(), lin, linearizer.scope(), e)?;
let head = instantiate_foralls(state, &mut ctxt, head_poly, ForallInst::UnifVar);

let dom = state.table.fresh_type_uvar(ctxt.var_level);
let codom = state.table.fresh_type_uvar(ctxt.var_level);
let arrow = mk_uty_arrow!(dom.clone(), codom.clone());

// "Match" the type of the head with `dom -> codom`
arrow.unify(head, state, &ctxt)
arrow
.unify(head, state, &ctxt)
.map_err(|err| err.into_typecheck_err(state, e.pos))?;

linearizer.add_term(lin, term, *pos, codom.clone());
check(state, ctxt.clone(), lin, linearizer, t, dom)?;
Ok(codom)
// subsumption(state, ctxt, tgt, ty).map_err(|err| err.into_typecheck_err(state, rt.pos))
}
Term::Annotated(annot, rt) => infer_annotated(state, ctxt, lin, linearizer, annot, rt),
_ => {
// The remaining cases can't produce polymorphic types, and thus we can reuse the
// checking code. The logic is the same, as inferring the type for those rules is
// equivalent to checking against a free unification variable. This saves use from
// duplicating all the remaining cases.
// checking code. Inferring the type for those rules is equivalent to checking against
// a free unification variable. This saves use from duplicating all the remaining
// cases.
let inferred = state.table.fresh_type_uvar(ctxt.var_level);
check(state, ctxt, lin, linearizer, rt, inferred.clone())?;
Ok(inferred.into_root(state.table))
Expand Down

0 comments on commit fb7feda

Please sign in to comment.