# Would it make sense for Julia to adopt refinement types?

**URL:** https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586
**Category:** Internals & Design
**Created:** [April 28, 2024, 1:38pm UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586 "2024-04-28T13:38:08Z")
**Posts on this page:** 3
**Page:** 2

<div class="post-metadata">

### Author: ![mefob](https://avatars.discourse-cdn.com/v4/letter/m/ea5d25/32.png) [@mefob](https://discourse.julialang.org/u/mefob)
#### Post date: [February 26, 2025, 6:47pm UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/21 "2025-02-26T18:47:30Z")

</div>

> [@Tamas\_Papp](#):
>
> this clearly. Generally, it is recommended not to do computations in type space.

We are on the same page, but sometimes it’s the only way. The unit example e.g. works by heavy use of generated functions to satisfy and check all unit combinations. To work around this we have DynamicQuantities.

> [@Tamas\_Papp](#):
>
> > [@mefob](#):
> >
> > Instead, the language should provide a basic type system that makes sure the right machine code gets generated with the minimum amount of dynamism.
> 
> I am under the impression that this is what Julia does now.

Yes, and it does so really well.

On the other hand, it is reasonable to ask for additional type guarantees, such as range types, full refinement types with arbitrary predicates, no-runtime cost physical units, and many more. Something as simple as a ranged integer would massively improve program correctness and speed up programs if it can prove array bounds.

---

<div class="post-metadata">

### Author: ![MilesCranmer](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/milescranmer/32/21070_2.png) [@MilesCranmer](https://discourse.julialang.org/u/MilesCranmer)
#### Post date: [February 26, 2025, 7:43pm UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/22 "2025-02-26T19:43:45Z")

</div>

> [@mefob](#):
>
> We are on the same page, but sometimes it’s the only way. The unit example e.g. works by heavy use of generated functions to satisfy and check all unit combinations. To work around this we have DynamicQuantities.

Completely random thought but I wonder if it would be technically possible to have Unitful.jl automatically switch to DynamicQuantities.jl when type inference fails?

Kinda like a DispatchDoctor.jl approach that has a function check its own type stability, and branch based on that

```julia
function _f_body(x)
    x == abs(x) ? (x / auto_u"s") : x
end
function f(x)
    T = Base.promote_op(_f_body, typeof(x))
    if Base.isconcretetype(T)
        # all stable, so continue normally
        return _f_body(x)
    else
        # instability! switch to runtime units
        return _f_body(convert(DQ.Quantity, x))
    end
end

```

So that `f` itself is always type stable.

But might be a low return-on-investment (and a bit spooky-action-at-a-distance)… But cool to think about.

---

<div class="post-metadata">

### Author: ![nsajko](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/nsajko/32/221187_2.png) [@nsajko](https://discourse.julialang.org/u/nsajko)
#### Post date: [August 12, 2025, 4:55pm UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/23 "2025-08-12T16:55:47Z")

</div>

> [@vchuravy](#):
>
> The core issue here is that our lattice only has Const and PartialConst, but not “Set of Values” or “Range of Values” representation.

Some cross-references for posterity:

- unmerged PR regarding “Range of Values” representation: [wip: inference: implement numeric interval analysis by aviatesk · Pull Request #48007 · JuliaLang/julia · GitHub](https://github.com/JuliaLang/julia/pull/48007)

- unmerged PR regarding “Set of Values” representation: [Implement support for set of constants in absint by vchuravy · Pull Request #56067 · JuliaLang/julia · GitHub](https://github.com/JuliaLang/julia/pull/56067)

Tangentially related work in other languages:

- eBPF: [[2105.05398] Sound, Precise, and Fast Abstract Interpretation with Tristate Numbers](https://arxiv.org/abs/2105.05398)

- PyPy: [A Knownbits Abstract Domain for the Toy Optimizer, Correctly | PyPy](https://pypy.org/posts/2024/08/toy-knownbits.html)

[Previous page](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586.md?page=1)
