Refinement Types#7625
Closed
connortsui20 wants to merge 3 commits into
Closed
Conversation
Introduces a refinement-type mechanism for extension types. An extension vtable
declares itself a refinement of its storage dtype by returning `true` from the
new defaulted method:
fn is_refinement(&self) -> bool { false }
Semantically this asserts that every value of the extension type is also a
value of its storage dtype, with additional invariants carried by the vtable.
Plain extension types (e.g. `Uuid` over `FSL<u8, 16>`) remain `false`: their
storage is just a physical encoding, not substitutable with the logical type.
The flag is surfaced through `ExtDTypeRef::is_refinement()` via a forwarder on
the object-safe `DynExtDType` trait.
Also adds `ExtDTypeRef::as_typed<V>()` — a borrowing downcast that does not
consume the ref — which is useful for any `ExtVTable` caller, refinement or
not.
The existing `DivisibleInt` and `EvenDivisibleInt` test extensions are rewired
as plain `ExtVTable` impls that return `true` from `is_refinement`. Their
divisibility checks now run in `unpack_native` (invoked by
`validate_scalar_value`). `EvenDivisibleInt` composes with `DivisibleInt` by
drilling through its storage via `as_typed::<DivisibleInt>()` and calling the
inner vtable's `unpack_native` before applying its own evenness check.
No behavioural impact on non-refinement extension types: the new method is
defaulted to `false` and nothing consumes it yet. A follow-up commit adds the
blanket scalar-fn pushdown that uses this flag.
Signed-off-by: Connor Tsui <connor.tsui20@gmail.com>
4 tasks
connortsui20
added
the
action/benchmark
github-actions
Bot
removed
the
action/benchmark
Contributor
Polar Signals Profiling ResultsLatest Run
Previous Runs (1)
Powered by Polar Signals Cloud |
Contributor
Benchmarks: PolarSignals ProfilingVortex (geomean): 1.017x ➖ datafusion / vortex-file-compressed (1.017x ➖, 0↑ 0↓)
|
Contributor
File Sizes: PolarSignals ProfilingNo file size changes detected. |
Contributor
Benchmarks: TPC-H SF=1 on NVMEVerdict: No clear signal (low confidence) datafusion / vortex-file-compressed (1.052x ➖, 0↑ 5↓)
datafusion / vortex-compact (1.059x ➖, 0↑ 4↓)
datafusion / parquet (1.026x ➖, 1↑ 1↓)
datafusion / arrow (1.036x ➖, 0↑ 2↓)
duckdb / vortex-file-compressed (0.990x ➖, 0↑ 0↓)
duckdb / vortex-compact (0.996x ➖, 0↑ 0↓)
duckdb / parquet (0.993x ➖, 1↑ 0↓)
duckdb / duckdb (1.001x ➖, 0↑ 0↓)
Full attributed analysis
|
Contributor
Benchmarks: FineWeb NVMeVerdict: No clear signal (low confidence) datafusion / vortex-file-compressed (1.003x ➖, 0↑ 1↓)
datafusion / vortex-compact (0.999x ➖, 0↑ 0↓)
datafusion / parquet (0.999x ➖, 0↑ 0↓)
duckdb / vortex-file-compressed (0.975x ➖, 1↑ 0↓)
duckdb / vortex-compact (0.973x ➖, 0↑ 0↓)
duckdb / parquet (1.010x ➖, 0↑ 0↓)
Full attributed analysis
|
Contributor
File Sizes: TPC-H SF=1 on NVMENo file size changes detected. |
Contributor
File Sizes: FineWeb NVMeNo file size changes detected. |
Contributor
Benchmarks: TPC-DS SF=1 on NVMEVerdict: No clear signal (low confidence) datafusion / vortex-file-compressed (1.075x ➖, 4↑ 37↓)
datafusion / vortex-compact (1.060x ➖, 5↑ 27↓)
datafusion / parquet (0.999x ➖, 0↑ 2↓)
duckdb / vortex-file-compressed (0.998x ➖, 1↑ 2↓)
duckdb / vortex-compact (0.987x ➖, 2↑ 1↓)
duckdb / parquet (0.995x ➖, 1↑ 1↓)
duckdb / duckdb (0.995x ➖, 2↑ 2↓)
Full attributed analysis
|
Contributor
File Sizes: TPC-DS SF=1 on NVMENo file size changes detected. |
Comment on lines
+32
to
+49
| /// | ||
| /// A refinement asserts that every value in this extension's logical domain is also a | ||
| /// value of the storage dtype's domain, with additional invariants enforced by this | ||
| /// vtable. The canonical examples are `NormalizedVector` (refines `Vector` by | ||
| /// requiring unit L2 norm) and a hypothetical `PositiveInt` (refines `Primitive(U64)` | ||
| /// by excluding zero). | ||
| /// | ||
| /// The default is `false`: plain extension types (e.g. `Uuid` over | ||
| /// `FixedSizeList<u8, 16>`) encode a distinct logical type in their storage that is | ||
| /// not substitutable with it. | ||
| /// | ||
| /// This flag is consumed by `ScalarFnRefinementPeelRule` (in | ||
| /// `arrays::scalar_fn::rules`) to decide whether to transparently peel a refinement | ||
| /// input and retry a scalar fn on the source type. See that rule for the full | ||
| /// semantics; the `TODO(connor)` there also tracks refinement-closure preservation. | ||
| fn is_refinement(&self) -> bool { | ||
| false | ||
| } |
Contributor
There was a problem hiding this comment.
lets make this an enum
General | Refinement
Contributor
Author
There was a problem hiding this comment.
Not sure what that gives us? Also not even sure what this method would be called.
Contributor
There was a problem hiding this comment.
Extensibility. Properties or Specialisation, ..?
Contributor
Author
There was a problem hiding this comment.
Those things would need to compose, right? In which case we probably either need more than a single method or return a struct of things. For now, I think a boolean is sufficient until we actually figure out the semantics of pushing things down to refinement/extension types (see the comment in vortex-array/src/arrays/scalar_fn/array.rs).
Contributor
There was a problem hiding this comment.
I guess you might expect them to be compositional, I was not
connortsui20
force-pushed
the
ct/refinement-types
branch
from
0789568 to
b385e7e
Compare
Contributor
Benchmarks: FineWeb S3Verdict: No clear signal (environment too noisy confidence) datafusion / vortex-file-compressed (1.098x ➖, 0↑ 1↓)
datafusion / vortex-compact (1.050x ➖, 0↑ 1↓)
datafusion / parquet (0.980x ➖, 0↑ 0↓)
duckdb / vortex-file-compressed (1.031x ➖, 0↑ 0↓)
duckdb / vortex-compact (1.038x ➖, 0↑ 0↓)
duckdb / parquet (0.982x ➖, 0↑ 0↓)
Full attributed analysis
|
Contributor
Benchmarks: Statistical and Population GeneticsVerdict: No clear signal (low confidence) duckdb / vortex-file-compressed (0.941x ➖, 1↑ 0↓)
duckdb / vortex-compact (0.964x ➖, 0↑ 0↓)
duckdb / parquet (0.969x ➖, 0↑ 0↓)
Full attributed analysis
|
Contributor
Benchmarks: TPC-H SF=10 on NVMEVerdict: No clear signal (low confidence) datafusion / vortex-file-compressed (1.034x ➖, 0↑ 1↓)
datafusion / vortex-compact (1.033x ➖, 0↑ 1↓)
datafusion / parquet (1.016x ➖, 0↑ 0↓)
datafusion / arrow (1.024x ➖, 0↑ 1↓)
duckdb / vortex-file-compressed (1.017x ➖, 0↑ 0↓)
duckdb / vortex-compact (1.015x ➖, 0↑ 0↓)
duckdb / parquet (1.004x ➖, 0↑ 0↓)
duckdb / duckdb (1.004x ➖, 0↑ 0↓)
Full attributed analysis
|
Contributor
File Sizes: Statistical and Population GeneticsNo file size changes detected. |
Contributor
File Sizes: TPC-H SF=10 on NVMENo file size changes detected. |
Contributor
Benchmarks: Random AccessVortex (geomean): 1.087x ➖ unknown / unknown (1.081x ➖, 0↑ 20↓)
|
Contributor
Benchmarks: Clickbench on NVMEVerdict: No clear signal (low confidence) datafusion / vortex-file-compressed (1.026x ➖, 0↑ 2↓)
datafusion / parquet (1.030x ➖, 0↑ 5↓)
duckdb / vortex-file-compressed (1.023x ➖, 0↑ 5↓)
duckdb / parquet (1.005x ➖, 0↑ 1↓)
duckdb / duckdb (0.967x ➖, 3↑ 0↓)
Full attributed analysis
|
Contributor
File Sizes: Clickbench on NVMEFile Size Changes (1 files changed, -0.0% overall, 0↑ 1↓)
Totals:
|
Contributor
Benchmarks: TPC-H SF=1 on S3Verdict: No clear signal (environment too noisy confidence) datafusion / vortex-file-compressed (0.952x ➖, 1↑ 1↓)
datafusion / vortex-compact (0.939x ➖, 1↑ 2↓)
datafusion / parquet (1.041x ➖, 0↑ 3↓)
duckdb / vortex-file-compressed (0.997x ➖, 0↑ 0↓)
duckdb / vortex-compact (1.005x ➖, 0↑ 0↓)
duckdb / parquet (0.991x ➖, 0↑ 0↓)
Full attributed analysis
|
Contributor
Benchmarks: CompressionVortex (geomean): 0.998x ➖ unknown / unknown (0.994x ➖, 0↑ 1↓)
|
Contributor
Benchmarks: TPC-H SF=10 on S3Verdict: No clear signal (environment too noisy confidence) datafusion / vortex-file-compressed (1.062x ➖, 0↑ 2↓)
datafusion / vortex-compact (0.993x ➖, 1↑ 2↓)
datafusion / parquet (1.022x ➖, 0↑ 1↓)
duckdb / vortex-file-compressed (0.954x ➖, 0↑ 0↓)
duckdb / vortex-compact (1.045x ➖, 0↑ 0↓)
duckdb / parquet (1.001x ➖, 0↑ 1↓)
Full attributed analysis
|
connortsui20
force-pushed
the
ct/refinement-types
branch
3 times, most recently
from
b6c3e91 to
993ee11
Compare
Merging this PR will degrade performance by 29.8%
Performance Changes
Comparing 
|
connortsui20
force-pushed
the
ct/refinement-types
branch
from
993ee11 to
414a56c
Compare
connortsui20
added
the
action/benchmark
github-actions
Bot
removed
the
action/benchmark
…truction
When a scalar fn is given a refinement-typed input that its `return_dtype`
rejects, the framework now transparently peels the refinement one level at a
time until the fn accepts the shape. This lands in `ScalarFnArray::try_new`
rather than as a reduce rule because `try_new` already calls `return_dtype`
and aborts on error — no ScalarFnArray tree is ever constructed to reduce
when a refinement input is rejected.
Algorithm (see `peel_refinements_and_resolve_dtype` for details):
1. Compute `scalar_fn.return_dtype(arg_dtypes)` on the current children.
2. If it succeeds, done. This covers both non-refinement inputs and fns
that explicitly accept the refinement (category B / C / D from the plan
— specialization path).
3. If it errors, peel one level from every child whose dtype is an
extension dtype with `is_refinement() == true`. Replace each with its
storage array.
4. If no children were peeled, return the original error.
5. Otherwise, loop back to step 1 with the peeled children. Multi-level
refinement chains (e.g. EvenDivisibleInt → DivisibleInt → U64) unwind
one level per iteration.
Implements category A (refinement-transparent scalar fns): when a generic fn
doesn't know about a refinement, the refinement is lost and the fn operates
on the source storage. Refinement-preserving semantics (categories C and D)
are deferred; the TODO(connor) in `peel_refinements_and_resolve_dtype`
documents the intended direction — an inverted-control hook on the refinement
vtable itself, rather than per-fn specialization, which is blocked by the
vortex-array → downstream crate dependency direction.
Exposes `crate::extension::tests::{divisible_int, even_divisible_int}` as
`pub(crate)` so the scalar-fn tests can reuse them. No user-facing public
API changes beyond what the prior commit landed.
Four unit tests:
- peels_single_level_refinement_through_strict_add: `Binary(Add)` over
`DivisibleInt(U64)` succeeds and returns `U64`.
- peels_two_level_refinement_chain_through_strict_add:
`EvenDivisibleInt(DivisibleInt(U64))` unwinds both layers.
- does_not_peel_non_refinement_extension: `Uuid` is not peeled; the fn's
original error surfaces.
- does_not_peel_when_scalar_fn_accepts_refinement: `Binary(Eq)` accepts
extension inputs directly, so children retain their refinement dtypes.
Signed-off-by: Connor Tsui <connor.tsui20@gmail.com>
connortsui20
force-pushed
the
ct/refinement-types
branch
from
414a56c to
33571c2
Compare
Contributor
Author
|
this is proving to be harder than expected to get right |
Signed-off-by: Connor Tsui <connor.tsui20@gmail.com>
Contributor
Author
|
This is more complicated than I initially thought, so I'm going to punt this to later |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Tracking issue: #6872
Adds refinement types as extension types by adding an
is_refinementmethod to theExtVTable.The main benefit of declaring an extension type as a refinement type is that many scalar functions can push down operations directly onto the storage array since the domain of values of the refinement type is a$\subseteq$ of the domain of the storage type.
This additionally adds a "reduction rule" (it's not actually a rule here, this is checked on construction and in expressions, I don't really know if this fits into our current reduction rule system?) that will "peel back" the refinement layers of extension types if the scalar function cannot handle / has no knowledge of the refinement type, but does know about the storage type.
I think we can also do this for non-scalar array parents? Not sure.
I've also left a TODO where it would be nice if there was a way to express that a refinement type is closed under some operation. For example, if we had a
PositiveIntegerrefinement type overPrimitive, we know that it is closed under addition (ignoring overflow), soadd: PositiveInteger x PositiveInteger -> PositiveInteger, but with this change alone we can only getadd: PositiveInteger x PositiveInteger -> Primitive. It is unclear if this is even possible to express.API Changes
Adds
is_refinementto theExtVTable.Testing
Some basic refinement type unit tests.