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

Jump to bottom

Add a subsumption rule between record types and dictionary types #1977

Merged
merged 5 commits into from
Jul 1, 2024
Merged

Add a subsumption rule between record types and dictionary types #1977

Changes from 2 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
35ff633
Add subsumption rule between Record/Dictionary
Eckaos Jun 25, 2024
abbbe1f
Remove commented code
Eckaos Jun 25, 2024
00a9537
Remove clone in pattern match, replaced fold by a for loop, take into…
Eckaos Jun 26, 2024
c99634e
Update & add comments
Eckaos Jun 27, 2024
bb20fc9
Add integration tests
Eckaos Jun 27, 2024
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
24 changes: 23 additions & 1 deletion core/src/typecheck/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2420,7 +2420,29 @@ pub fn subsumption(
checked: UnifType,
) -> Result<(), UnifError> {
let inferred_inst = instantiate_foralls(state, &mut ctxt, inferred, ForallInst::UnifVar);
checked.unify(inferred_inst, state, &ctxt)
match (inferred_inst.clone(), checked.clone()) {
Copy link
Member

Choose a reason for hiding this comment

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

Suggested change
match (inferred_inst.clone(), checked.clone()) {
match (inferred_inst, checked) {

Those early clones are probably not needed. You might need to put a ref in the pattern matching though, as in:

           UnifType::Concrete {
                typ: TypeF::Record(ref rrows),
                ..
            },

(
UnifType::Concrete {
typ: TypeF::Record(rrows),
..
},
UnifType::Concrete {
typ: TypeF::Dict { type_fields, .. },
..
},
) => rrows.iter().fold(
Copy link
Member

Choose a reason for hiding this comment

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

If you don't build anything valuable in a fold, then you can probably get rid of it and just use a good old for loop:

for row in rrows {
    if  let GenericUnifRecordRowsIteratorItem::Row(a) = row {
        subsumption(state, ctxt.clone(), a.typ.clone(), *type_fields.clone())?;
    }
}

Ok(())

Ok(()),
|acc, row: GenericUnifRecordRowsIteratorItem<_>| -> Result<(), UnifError> {
match (row, &acc) {
(GenericUnifRecordRowsIteratorItem::Row(a), Ok(_)) => {
subsumption(state, ctxt.clone(), a.typ.clone(), *type_fields.clone())
}
_ => acc,
Copy link
Member

Choose a reason for hiding this comment

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

Now I'm thinking about something that I haven't thought about before. During type inference, we might have open record types, such as {foo : Number, bar : Number; tail} where the tail at the end means that this value can have more fields that we don't know yet.

If we try to subtype that with a dictionary, as in {foo : Number, bar : Number; ?a} <: {_ : Number}, we can't let the ?a be, because it might very much be instantiated with baz : String at some point. So we need to close the tail of the record.

Interestingly, we can put Dyn in the tail currently (instead of ?a) to say that we don't know anything about it, that those are some fields with Dyn type. I wonder if we could extend the type system to add other types, for example {foo : Number, bar : Number; Number} (or {foo : Number, bar : Number; _ : Number}) to say that the tail is unknown but fields must be numbers. That would probably be a better representation.

Anyhow, I'm just thinking out loud. Let's forget that, for now, I don't think we can do better than closing the tail of the record. In practice, this means that we need to also consider the cases:

  • GenericUnifRecordRowsIteratorItem::UnifVar { id, init_level}. In that case we need to unify this var with an empty row. Here is how it's done (note: it's done for enum rows below, but it's exactly the same for record rows; just change any "enum" to "record"):

    nickel/core/src/typecheck/pattern.rs

    Lines 129 to 133 in 9969d9a

    // We don't need to perform any variable level checks when unifying a free
    // unification variable with a ground type
    state
    .table
    .assign_erows(id, UnifEnumRows::concrete(EnumRowsF::Empty));

  • GenericUnifRecordRowsIteratorItem::TailConstant(id). In this case we must fail. We can raise a WithConst error - in the future we could have a dedicated error for better messages, but for now, that will do.

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

fn check_field<V: TypecheckVisitor>(
Expand Down
Loading