Would it make sense for Julia to adopt refinement types?

Internals & Design
21

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.

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.

22

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

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.

6 Likes