Would it make sense for Julia to adopt refinement types?

Internals & Design
10

Stumbled on an example where it seems like refinement types would be useful to improve Julia’s type inference:

f(t::Tuple, n::Bool) = t[10 + n]

Julia would ideally be able to prove that the below abstract call is type stable, but it currently fails:

julia> Core.Compiler.return_type(f, Tuple{Tuple{Bool,String,Vararg{Int}},Bool})
Union{Bool, Int64, String}

The call will always return Int (if it returns), because the index 10 + n is always either 10 or 11, thus the index is always greater than two.

I guess Julia isn’t able to prove this because, after n gets converted to Int, Julia has forgotten about the fact that n can only take two values: zero or one. Some kind of refinement types (perhaps purely for internal use in the compiler) could presumably help Julia remember that the result of convert(::Type{Int}, ::Bool) is always nonnegative, and thus that 10 + n is always greater than two.

EDIT: issue on Github:

3 Likes