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.

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

Adding dictionary constructor to subsumption rule #1998

Merged
merged 8 commits into from
Jul 19, 2024

Conversation

Eckaos
Copy link
Contributor

@Eckaos Eckaos commented Jul 17, 2024

No description provided.

@Eckaos Eckaos marked this pull request as ready for review July 17, 2024 13:53
@@ -2416,6 +2416,9 @@ pub fn subsumption(
Ok(())
}
(TypeF::Array(a), TypeF::Array(b)) => subsumption(state, ctxt, *a.clone(), *b.clone()),
(TypeF::Dict { type_fields: a, .. }, TypeF::Dict { type_fields: b, .. }) => {
subsumption(state, ctxt.clone(), *a.clone(), *b.clone())
Copy link
Member

Choose a reason for hiding this comment

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

Why do we need to clone everywhere here? couldn't we just match on inferred_inst and not &inferred_inst and take ownership of the subcomponents?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Because this line,

(_,_) => checked.unify(inferred_inst, state, &ctxt)

and

else {
    checked.unify(inferred_inst, state, &ctxt)
}

I need to pattern match on &inferred_inst to not move the ownership. If I try to pattern match on inferred_inst, I can't refer to inferred_inst anymore because the ownership has moved.

I found an alternative with using only one pattern matching but it is a bit long and unreadable i think.

match (inferred_inst, &checked) {
        (
            UnifType::Concrete {
                typ: TypeF::Record(rrows),
                ..
            },
            UnifType::Concrete {
                typ: TypeF::Dict { type_fields, .. },
                ..
            },
        ) => {
            for row in rrows.iter() {
                match row {
                    GenericUnifRecordRowsIteratorItem::Row(a) => {
                        subsumption(state, ctxt.clone(), a.typ.clone(), *type_fields.clone())?
                    }
                    GenericUnifRecordRowsIteratorItem::TailUnifVar { id, .. } =>
                    // We don't need to perform any variable level checks when unifying a free
                    // unification variable with a ground type
                    // We close the tail because there is no garanty that
                    // { a : Number, b : Number, _ : a?} <= { _ : Number}
                    {
                        state
                            .table
                            .assign_rrows(id, UnifRecordRows::concrete(RecordRowsF::Empty))
                    }
                    GenericUnifRecordRowsIteratorItem::TailConstant(id) => {
                        Err(UnifError::WithConst {
                            var_kind: VarKindDiscriminant::RecordRows,
                            expected_const_id: id,
                            inferred: checked.clone(),
                        })?
                    }
                    _ => (),
                }
            }
            Ok(())
        }
        (
            UnifType::Concrete {
                typ: TypeF::Array(a),
                ..
            },
            UnifType::Concrete {
                typ: TypeF::Array(b),
                ..
            },
        )
        | (
            UnifType::Concrete {
                typ: TypeF::Dict { type_fields: a, .. },
                ..
            },
            UnifType::Concrete {
                typ: TypeF::Dict { type_fields: b, .. },
                ..
            },
        ) => subsumption(state, ctxt.clone(), *a, *b.clone()),
        (inferred_inst, _) => checked.unify(inferred_inst, state, &ctxt),
    }

I don't really see a middle ground between the two alternatives.

Copy link
Member

Choose a reason for hiding this comment

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

I think this one is fine, although I don't see why you still need to take &checked as a reference (which causes you to clone it in the UnifError::WithConst.

It's true that let-type has the bad side effect of consuming the scrutinee. If you really want to avoid repeating the UnifTypeConcrete (IMHO again, it's not that bad), you can use a match for the outer level as well:

match (inferred_inst, checked) {
        (
            UnifType::Concrete {
                typ: typ1,
                var_levels_data: data1,
            },
            UnifType::Concrete {
                typ: typ2,
                var_levels_data: data2,
            },
        ) => match (typ1, typ2) {
            (
                TypeF::Record(rrows),
                TypeF::Dict {
                    type_fields,
                    flavour,
                },
            ) => {
                for row in rrows.iter() {
                    match row {
                        GenericUnifRecordRowsIteratorItem::Row(a) => {
                            subsumption(state, ctxt.clone(), a.typ.clone(), *type_fields.clone())?
                        }
                        GenericUnifRecordRowsIteratorItem::TailUnifVar { id, .. } =>
                        // We don't need to perform any variable level checks when unifying a free
                        // unification variable with a ground type
                        // We close the tail because there is no garanty that
                        // { a : Number, b : Number, _ : a?} <= { _ : Number}
                        {
                            state
                                .table
                                .assign_rrows(id, UnifRecordRows::concrete(RecordRowsF::Empty))
                        }
                        GenericUnifRecordRowsIteratorItem::TailConstant(id) => {
                            let checked = UnifType::Concrete {
                                typ: TypeF::Dict {
                                    type_fields: type_fields.clone(),
                                    flavour: flavour.clone(),
                                },
                                var_levels_data: data2,
                            };

                            Err(UnifError::WithConst {
                                var_kind: VarKindDiscriminant::RecordRows,
                                expected_const_id: id,
                                inferred: checked,
                            })?
                        }
                        _ => (),
                    }
                }
                Ok(())
            }
            (TypeF::Array(a), TypeF::Array(b)) => subsumption(state, ctxt, *a, *b),
            (TypeF::Dict { type_fields: a, .. }, TypeF::Dict { type_fields: b, .. }) => {
                subsumption(state, ctxt.clone(), *a, *b)
            }
            (typ1, typ2) => {
                let inferred_inst = UnifType::Concrete {
                    typ: typ1,
                    var_levels_data: data1,
                };

                let checked = UnifType::Concrete {
                    typ: typ2,
                    var_levels_data: data2,
                };

                checked.unify(inferred_inst, state, &ctxt)
            }
        },
        (inferred_inst, checked) => checked.unify(inferred_inst, state, &ctxt),
    }

The annoying thing is that you have to reconstruct checked and all when you need them back, which is a bit cumbersome. So all in all I'm personally leaning to your one big pattern matching solution.

The thing is, cloning types isn't free, so it's not a question of style. In general we shouldn't clone things just because it's easier to write, unless the clone is arguably invisible or we don't care anymore about performance (say in the error path).

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I changed &checked with checked in the pattern match.
But since with the pattern match, I can't refer to checked in the error construction. I made a clone before the pattern match and I need to clone in the construction of the error because it is in a loop. I don't think cloning in the error is a problem for performance because it is thrown immediately.

    let checked_for_err = &checked.clone();
    match (inferred_inst, checked) {
        (
            UnifType::Concrete {
                typ: TypeF::Record(rrows),
                ..
            },
            UnifType::Concrete {
                typ: TypeF::Dict { type_fields, .. },
                ..
            },
        ) => {
            for row in rrows.iter() {
                match row {
                    GenericUnifRecordRowsIteratorItem::Row(a) => {
                        subsumption(state, ctxt.clone(), a.typ.clone(), *type_fields.clone())?
                    }
                    GenericUnifRecordRowsIteratorItem::TailUnifVar { id, .. } =>
                    // We don't need to perform any variable level checks when unifying a free
                    // unification variable with a ground type
                    // We close the tail because there is no garanty that
                    // { a : Number, b : Number, _ : a?} <= { _ : Number}
                    {
                        state
                            .table
                            .assign_rrows(id, UnifRecordRows::concrete(RecordRowsF::Empty))
                    }
                    GenericUnifRecordRowsIteratorItem::TailConstant(id) => {
                        Err(UnifError::WithConst {
                            var_kind: VarKindDiscriminant::RecordRows,
                            expected_const_id: id,
                            inferred: checked_for_err.clone(),
                        })?
                    }
                    _ => (),
                }
            }
            Ok(())
        }
        (
            UnifType::Concrete {
                typ: TypeF::Array(a),
                ..
            },
            UnifType::Concrete {
                typ: TypeF::Array(b),
                ..
            },
        )
        | (
            UnifType::Concrete {
                typ: TypeF::Dict { type_fields: a, .. },
                ..
            },
            UnifType::Concrete {
                typ: TypeF::Dict { type_fields: b, .. },
                ..
            },
        ) => subsumption(state, ctxt.clone(), *a, *b),
        (inferred_inst, checked) => checked.unify(inferred_inst, state, &ctxt),
    }

Copy link
Member

Choose a reason for hiding this comment

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

You can look at my example. I rebuild checked when needed for the error reporting, so that it saves a clone() if we don't take the error path. Your solution is reasonable as well, that's just one clone (but we still do one more clone that in my proposal)

Copy link
Member

@yannham yannham left a comment

Choose a reason for hiding this comment

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

Looks good! This "need to reconstruct data previously deconstructed for errors" is a bit annoying, but it's part of the life of a Rustacean, unfortunately 🙃

@yannham
Copy link
Member

yannham commented Jul 19, 2024

@Eckaos ping me when you're done, so that I can merge this.

@Eckaos
Copy link
Contributor Author

Eckaos commented Jul 19, 2024

I think i'm done ! @yannham

@yannham yannham added this pull request to the merge queue Jul 19, 2024
Merged via the queue into tweag:master with commit e9770b0 Jul 19, 2024
4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants