Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix: Ensure that the constraints are checked and propagated fully #4798

Merged
merged 6 commits into from
May 30, 2022
Merged

fix: Ensure that the constraints are checked and propagated fully #4798

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
eb18540
fix: Always query the root variable for the constraint it is bound by
May 25, 2022
4ca3b4a
fix: Don't cause errors in default argument checking due to label req…
May 25, 2022
19e34e0
fix: Always add constraints to the root variable
May 25, 2022
56aa980
chore: make generate
May 27, 2022
b7bb60a
fix: (Actually) Always query the root variable for the constraint it …
May 27, 2022
4adc9b3
chore: make generate
May 27, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 24 additions & 2 deletions libflux/flux-core/src/semantic/infer.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -158,7 +158,7 @@ pub fn constrain(
) -> Result<(), Located<types::Error>> {
log::debug!("Constraint::Kind {:?}: {} => {}", loc.source, exp, act);
act.apply_cow(sub)
.constrain(exp, sub.cons())
.constrain(exp, sub)
.map_err(|error| Located {
location: loc.clone(),
error,
Expand All @@ -182,6 +182,28 @@ pub fn equal(
})
}

pub fn subsume(
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is the intent of the name subsume? Is this related to subtyping somehow? My understanding of your changes was that we are propagating the constraints to the root type. Is root type the supertype in this context? I had assumed that the root type was just the root type variable where all its sub type variables are all equal to it and we have a convention to associate the constraints with the root type.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is the intent of the name subsume? Is this related to subtyping somehow?

Yes, this change is for fix: Don't cause errors in default argument checking due to label requirements. I needed to change the check to use subsumption, else the default value (a string literal) would not get treated as a label and cause an error as the function required a label to be passed. It should probably have been a separate PR as it is a different change from fully checking the constraints fully.

Is root type the supertype in this context?

No. If multiple variables are unified the root is the variable that names the entire set.
Say you unify like this

A <> B
B <> C

D <> E

The set A, B, C may have the root A while D, E has the root E. Querying the root for B or C returns A in both cases which lets us know that they are unified while querying it for D will yield E so we know it is in a disjoint set from B, C (and A). Which variable in a set that ends up as the root is arbitrary and just a by product of how https://en.wikipedia.org/wiki/Disjoint-set_data_structure is implemented.

Specifically in this change I made sure that add a constraint on, for example, B (which has A as the root) we actually record the constraint on A. Before, when we added the constraint on B explicitly inference did not know that A and C were also constrained by this (hence lost).

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the explanation, helps clarify.

exp: &MonoType,
act: &MonoType,
loc: &SourceLocation,
sub: &mut Substitution,
) -> Result<MonoType, Located<Errors<types::Error>>> {
log::debug!(
"Constraint::Subsume {:?}: {} <===> {}",
loc.source,
exp,
act
);
exp.try_subsume(act, sub).map_err(|error| {
log::debug!("Unify error: {} <=> {} : {}", exp, act, error);

Located {
location: loc.clone(),
error,
}
})
}

/// Generalizes `t` without modifying the substitution.
pub(crate) fn temporary_generalize(
env: &Environment,
Expand Down Expand Up @@ -248,7 +270,7 @@ pub(crate) fn temporary_generalize(
pub fn generalize(env: &Environment, sub: &mut Substitution, t: MonoType) -> PolyType {
struct Generalize<'a> {
env_free_vars: Vec<Tvar>,
sub: &'a Substitution,
sub: &'a mut Substitution,
vars: Vec<(Tvar, Tvar)>,
}

Expand Down
82 changes: 59 additions & 23 deletions libflux/flux-core/src/semantic/nodes.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -167,6 +167,51 @@ impl InferState<'_, '_> {
}
}

fn subsume(&mut self, exp: &MonoType, act: &MonoType, loc: &ast::SourceLocation) -> MonoType {
match infer::subsume(exp, act, loc, self.sub) {
Ok(typ) => typ,
Err(err) => {
self.errors
.extend(err.error.into_iter().map(|error| Located {
location: loc.clone(),
error: error.into(),
}));
MonoType::Error
}
}
}

fn subsume_function(
&mut self,
call_expr: &CallExpr,
exp: &Function,
act: Function<(MonoType, &ast::SourceLocation)>,
) {
log::debug!(
"Subsume {:?}: {} <===> {}",
call_expr.callee.loc().source,
exp,
act.clone().map(|(typ, _)| typ),
);
if let Err(err) = exp.try_subsume_with(
&act,
self.sub,
|typ| (typ.clone(), call_expr.callee.loc()),
|error| Located {
location: call_expr.loc.clone(),
error,
},
) {
log::debug!(
"Unify error: {} <=> {} : {}",
exp,
act.clone().map(|(typ, _)| typ),
err
);
self.errors.extend(err.into_iter().map(Error::from));
}
}

fn error(&mut self, loc: ast::SourceLocation, error: ErrorKind) {
self.errors.push(located(loc, error));
}
Expand Down Expand Up @@ -1019,7 +1064,7 @@ impl FunctionExpr {

infer.solve(&ncons);

infer.equal(&exp, &default_func, &self.loc);
infer.subsume(&exp, &default_func, &self.loc);

Ok(())
}
Expand Down Expand Up @@ -1292,18 +1337,25 @@ impl CallExpr {
self.callee.infer(infer)?;
let mut req = MonoTypeMap::new();
let mut pipe = None;
for arg in &mut self.arguments {
arg.value.infer(infer)?;
}

for Property {
key: ref mut id,
value: ref mut expr,
key: id,
value: expr,
..
} in &mut self.arguments
} in &self.arguments
{
expr.infer(infer)?;
// Every argument is required in a function call.
req.insert(id.name.to_string(), (expr.type_of(), expr.loc()));
}
if let Some(ref mut p) = &mut self.pipe {

if let Some(p) = &mut self.pipe {
p.infer(infer)?;
}

if let Some(p) = &self.pipe {
pipe = Some(types::Property {
k: "<-".to_string(),
v: (p.type_of(), p.loc()),
Expand All @@ -1319,23 +1371,7 @@ impl CallExpr {

match &*self.callee.type_of().apply_cow(infer.sub) {
MonoType::Fun(func) => {
if let Err(err) = func.try_subsume_with(
&act,
infer.sub,
|typ| (typ.clone(), self.callee.loc()),
|error| Located {
location: self.loc.clone(),
error,
},
) {
log::debug!(
"Unify error: {} <=> {} : {}",
func,
act.map(|(typ, _)| typ),
err
);
infer.errors.extend(err.into_iter().map(Error::from));
}
infer.subsume_function(self, func, act);
}
callee => {
let act = act.map(|(typ, _)| typ);
Expand Down
37 changes: 30 additions & 7 deletions libflux/flux-core/src/semantic/sub.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ use std::{borrow::Cow, cell::RefCell, collections::BTreeMap, fmt, iter::FusedIte

use crate::semantic::{
fresh::Fresher,
types::{union, Error, MonoType, PolyType, SubstitutionMap, Tvar, TvarKinds},
types::{union, Error, Kind, MonoType, PolyType, SubstitutionMap, Tvar, TvarKinds},
};

use ena::unify::UnifyKey;
Expand Down Expand Up @@ -62,7 +62,7 @@ type UnificationTable = ena::unify::InPlaceUnificationTable<Tvar>;
impl From<SubstitutionMap> for Substitution {
/// Derive a substitution from a hash map.
fn from(values: SubstitutionMap) -> Substitution {
let sub = Substitution::default();
let mut sub = Substitution::default();
for (var, typ) in values {
// Create any variables referenced in the input map
while var.0 >= sub.table.borrow().len() as u64 {
Expand All @@ -75,6 +75,11 @@ impl From<SubstitutionMap> for Substitution {
}

impl Substitution {
/// Return a new empty substitution.
pub fn new() -> Substitution {
Substitution::default()
}

/// Return a new empty substitution.
pub fn empty() -> Substitution {
Substitution::default()
Expand Down Expand Up @@ -107,6 +112,25 @@ impl Substitution {
self.cons.get_mut()
}

/// Returns the real type or the root variable of `typ` if it is an variable.
/// Returns `typ` itself if it isn't a variable
pub(crate) fn real<'a>(&self, typ: &'a MonoType) -> Cow<'a, MonoType> {
match *typ {
MonoType::Var(var) => self
.try_apply(var)
.map(Cow::Owned)
.unwrap_or_else(|| Cow::Borrowed(typ)),
_ => Cow::Borrowed(typ),
}
}

pub(crate) fn satisfies(&self, v: Tvar, kind: Kind) -> bool {
self.cons
.borrow()
.get(&v)
.map_or(false, |kinds| kinds.contains(&kind))
}

/// Apply a substitution to a type variable.
pub fn apply(&self, tv: Tvar) -> MonoType {
self.try_apply(tv).unwrap_or(MonoType::Var(tv))
Expand Down Expand Up @@ -143,22 +167,21 @@ impl Substitution {

/// Unifies as a `Tvar` and a `MonoType`, recording the result in the substitution for later
/// lookup
pub fn union_type(&self, var: Tvar, typ: MonoType) -> Result<(), Error> {
pub fn union_type(&mut self, var: Tvar, typ: MonoType) -> Result<(), Error> {
match typ {
MonoType::Var(r) => self.union(var, r),
_ => {
self.table.borrow_mut().union_value(var, Some(typ.clone()));

let mut cons = self.cons.borrow_mut();
if let Some(kinds) = cons.remove(&var) {
if let Some(kinds) = self.cons().remove(&var) {
for kind in &kinds {
// The monotype that is being unified with the
// tvar must be constrained with the same kinds
// as that of the tvar.
typ.clone().constrain(*kind, &mut cons)?;
typ.clone().constrain(*kind, self)?;
}
if matches!(typ, MonoType::BoundVar(_)) {
cons.insert(var, kinds);
self.cons().insert(var, kinds);
}
}
}
Expand Down
55 changes: 55 additions & 0 deletions libflux/flux-core/src/semantic/tests/labels.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -274,3 +274,58 @@ fn optional_label_undefined() {
"#]],
}
}

#[test]
fn default_arguments_do_not_try_to_treat_literals_as_strings_when_they_must_be_a_label() {
test_infer! {
config: AnalyzerConfig{
features: vec![Feature::LabelPolymorphism],
..AnalyzerConfig::default()
},
env: map![
"max" => r#"(<-tables: stream[{ A with L: B }], ?column: L) => stream[{ A with L: B }]
where A: Record,
B: Comparable,
L: Label"#,
],
src: r#"
f = (
column="_value",
tables=<-,
) =>
tables
// `column` would be treated as `string` instead of a label when checking the
// default arguments
|> max(column: column)
"#,
exp: map![
"f" => r#"(<-tables:stream[{C with A:B}], ?column:A) => stream[{C with A:B}] where A: Label, B: Comparable, C: Record"#,
],
}
}

#[test]
fn constraints_propagate_fully() {
test_infer! {
config: AnalyzerConfig{
features: vec![Feature::LabelPolymorphism],
..AnalyzerConfig::default()
},
env: map![
"aggregateWindow" => r#"(fn:(<-:stream[B], column:C) => stream[D], ?column:C) => stream[E]"#,
"max" => r#"(<-tables: stream[{ A with L: B }], ?column: L) => stream[{ A with L: B }]
where A: Record,
B: Comparable,
L: Label"#,
],
src: r#"
x = aggregateWindow(
fn: max,
column: "_value",
)
"#,
exp: map![
"x" => "stream[E]",
],
}
}
Loading