Skip to content

Commit

Permalink
[red-knot] add IntersectionBuilder (#12791)
Browse files Browse the repository at this point in the history
For type narrowing, we'll need intersections (since applying type
narrowing is just a type intersection.)

Add `IntersectionBuilder`, along with some tests for it and
`UnionBuilder` (renamed from `UnionTypeBuilder`).

We use smart builders to ensure that we always keep these types in
disjunctive normal form (DNF). That means that we never have deeply
nested trees of unions and intersections: unions flatten into unions,
intersections flatten into intersections, and intersections distribute
over unions, so the most complex tree we can ever have is a union of
intersections. We also never have a single-element union or a
single-positive-element intersection; these both just simplify to the
contained type.

Maintaining these invariants means that `UnionBuilder` doesn't
necessarily end up building a `Type::Union` (e.g. if you only add a
single type to the union, it'll just return that type instead), and
`IntersectionBuilder` doesn't necessarily build a `Type::Intersection`
(if you add a union to the intersection, we distribute the intersection
over that union, and `IntersectionBuilder` will end up returning a
`Type::Union` of intersections).

We also simplify intersections by ensuring that if a type and its
negation are both in an intersection, they simplify out. (In future this
should also respect subtyping, not just type identity, but we don't have
subtyping yet.) We do implement subtyping of `Never` as a special case
for now.

Most of this PR is unused for now until type narrowing lands; I'm just
breaking it out to reduce the review fatigue of a single massive PR.
  • Loading branch information
carljm committed Aug 12, 2024
1 parent 4b9ddc4 commit 75131c6
Show file tree
Hide file tree
Showing 3 changed files with 455 additions and 58 deletions.
76 changes: 23 additions & 53 deletions crates/red_knot_python_semantic/src/types.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,11 @@ use crate::semantic_index::symbol::{ScopeId, ScopedSymbolId};
use crate::semantic_index::{global_scope, symbol_table, use_def_map};
use crate::{Db, FxOrderSet};

mod builder;
mod display;
mod infer;

pub(crate) use self::builder::UnionBuilder;
pub(crate) use self::infer::{infer_definition_types, infer_scope_types};

/// Infer the public type of a symbol (its type as seen from outside its scope).
Expand Down Expand Up @@ -91,14 +93,14 @@ pub(crate) fn definitions_ty<'db>(
};

if let Some(second) = all_types.next() {
let mut builder = UnionTypeBuilder::new(db);
let mut builder = UnionBuilder::new(db);
builder = builder.add(first).add(second);

for variant in all_types {
builder = builder.add(variant);
}

Type::Union(builder.build())
builder.build()
} else {
first
}
Expand All @@ -117,7 +119,7 @@ pub enum Type<'db> {
/// name does not exist or is not bound to any value (this represents an error, but with some
/// leniency options it could be silently resolved to Unknown in some cases)
Unbound,
/// the None object (TODO remove this in favor of Instance(types.NoneType)
/// the None object -- TODO remove this in favor of Instance(types.NoneType)
None,
/// a specific function object
Function(FunctionType<'db>),
Expand All @@ -127,8 +129,11 @@ pub enum Type<'db> {
Class(ClassType<'db>),
/// the set of Python objects with the given class in their __class__'s method resolution order
Instance(ClassType<'db>),
/// the set of objects in any of the types in the union
Union(UnionType<'db>),
/// the set of objects in all of the types in the intersection
Intersection(IntersectionType<'db>),
/// An integer literal
IntLiteral(i64),
/// A boolean literal, either `True` or `False`.
BooleanLiteral(bool),
Expand Down Expand Up @@ -159,15 +164,13 @@ impl<'db> Type<'db> {
// TODO MRO? get_own_instance_member, get_instance_member
todo!("attribute lookup on Instance type")
}
Type::Union(union) => Type::Union(
union
.elements(db)
.iter()
.fold(UnionTypeBuilder::new(db), |builder, element_ty| {
builder.add(element_ty.member(db, name))
})
.build(),
),
Type::Union(union) => union
.elements(db)
.iter()
.fold(UnionBuilder::new(db), |builder, element_ty| {
builder.add(element_ty.member(db, name))
})
.build(),
Type::Intersection(_) => {
// TODO perform the get_member on each type in the intersection
// TODO return the intersection of those results
Expand Down Expand Up @@ -251,7 +254,7 @@ impl<'db> ClassType<'db> {

#[salsa::interned]
pub struct UnionType<'db> {
/// the union type includes values in any of these types
/// The union type includes values in any of these types.
elements: FxOrderSet<Type<'db>>,
}

Expand All @@ -261,48 +264,15 @@ impl<'db> UnionType<'db> {
}
}

struct UnionTypeBuilder<'db> {
elements: FxOrderSet<Type<'db>>,
db: &'db dyn Db,
}

impl<'db> UnionTypeBuilder<'db> {
fn new(db: &'db dyn Db) -> Self {
Self {
db,
elements: FxOrderSet::default(),
}
}

/// Adds a type to this union.
fn add(mut self, ty: Type<'db>) -> Self {
match ty {
Type::Union(union) => {
self.elements.extend(&union.elements(self.db));
}
_ => {
self.elements.insert(ty);
}
}

self
}

fn build(self) -> UnionType<'db> {
UnionType::new(self.db, self.elements)
}
}

// Negation types aren't expressible in annotations, and are most likely to arise from type
// narrowing along with intersections (e.g. `if not isinstance(...)`), so we represent them
// directly in intersections rather than as a separate type. This sacrifices some efficiency in the
// case where a Not appears outside an intersection (unclear when that could even happen, but we'd
// have to represent it as a single-element intersection if it did) in exchange for better
// efficiency in the within-intersection case.
#[salsa::interned]
pub struct IntersectionType<'db> {
// the intersection type includes only values in all of these types
/// The intersection type includes only values in all of these types.
positive: FxOrderSet<Type<'db>>,
// the intersection type does not include any value in any of these types

/// The intersection type does not include any value in any of these types.
///
/// Negation types aren't expressible in annotations, and are most likely to arise from type
/// narrowing along with intersections (e.g. `if not isinstance(...)`), so we represent them
/// directly in intersections rather than as a separate type.
negative: FxOrderSet<Type<'db>>,
}
Loading

0 comments on commit 75131c6

Please sign in to comment.