Intransitivities in subtyping

Internals & Design
1

I think the WAT on subtyping is

julia> Direct = Tuple{String,String}
Tuple{String, String}

julia> SubStr = Tuple{T,T} where T<:String
Tuple{T, T} where T<:String

julia> SupStr = Tuple{T,T} where T>:String
Tuple{T, T} where T>:String

julia> SubStr <: Direct
true

julia> Direct <: SupStr
true

julia> SubStr <: SupStr
false

i.e. the failure of transitivity of subtyping.

11 Likes
2

Is there a bug report already?

Also, I think this case wasn’t discussed as breaking transitivity in the Julia subtyping paper, so I guess it’s a regression since the v0.6.2 days?

3

Not that I know, but I admit that I haven’t looked too hard. I just ran it on 1.9.2.

My takeaway from all the julia type system stuff was: It works amazingly well in real life, but looking at how the sausage is made is not for the faint of heart and may spoil your enjoyment of julia.

It is unfortunately a never-ending source of zombie-bugs that come back and back, mixed in with “CANTFIX, subtyping is undecidable anyway”.

(big wish for 2.0: sacrifice some convenience and expressivity in order to make the type system simpler and sounder, i.e. make it feasible to have a small and understandable toy implementation of the type system)

6 Likes
4

This is even worse than it looks at first, because SubStr == Direct. So it’s not so much a counterexample for transitivity, as it is a basic logical error:

julia> struct S end

julia> const A = Tuple{S,S}
Tuple{S, S}

julia> const B = Tuple{T,T} where {T<:S}
Tuple{T, T} where T<:S

julia> const C = Tuple{T,T} where {T>:S}
Tuple{T, T} where T>:S

julia> (A == B) & isequal(A, B) & (A <: B <: A <: B)
true

julia> A <: C
true

julia> B <: C
false

Bug report: inconsistent subtyping: `A == B`, but `(A <: C) & !(B <: C)` · Issue #53019 · JuliaLang/julia · GitHub

1 Like
5

A == B between types is implemented as A <: B && B <: A, and I don’t think that Direct <: SubStr makes it worse? We’d like subtyping to be transitive, or objects with A==B to be exchangeable when tested with <:, but failure of that is not a logical error.

But it would be a quite catastrophic logical error if we had a practical distinction between some A and B with A === B.

:+1: but maybe split off the parts of discussion that are still ongoing? I don’t feel like the ongoing discussion has gone bad yet.

That is only very slightly related to the 2 year old parts and should have been a new thread instead of necroing the old one.

2 Likes
6

I generated a considerable number of intransitive subtyping examples automatically, here are the Julia bug report and my repo:

4 Likes
8

No, this is not a regression, and, in fact, the code by the authors of the paper exhibits the same intransitivity (lj_subtype_revised behaves the same as lj_subtype):

julia> include("/home/nsajko/tmp/jl/julia_subtyping/juliasubtyping-distro/lj.jl")
--- LJ-INFO: LJ init
--- LJ-INFO: include LJ files
--- LJ-INFO: LJ loaded
--- LJ-INFO: Install LJ dependencies
--- LJ-INFO: Dump decls (if needed)
Loading type declarations... Done

julia> const Direct = "Tuple{String,String}"
"Tuple{String,String}"

julia> const SubStr = "Tuple{T,T} where T<:String"
"Tuple{T,T} where T<:String"

julia> const SupStr = "Tuple{T,T} where T>:String"
"Tuple{T,T} where T>:String"

julia> lj_subtype(SubStr, Direct)
= true
= [T ^String _Union{} L [false|0|0] false]  ||| 
                   === stats ===
Rule Name                         # occs  success
L_Left                      =>         2     100%
Refl(Name)                  =>         2     100%
Tuple                       =>         1     100%
L_Intro                     =>         1     100%


julia> lj_subtype(Direct, SupStr)
= true
= [T ^Any _String R [false|2|0] false]  ||| 
                   === stats ===
Rule Name                         # occs  success
Top                         =>         4     100%
R_Right                     =>         2     100%
R_Intro                     =>         1     100%
Tuple                       =>         1     100%


julia> lj_subtype(SubStr, SupStr)
= false
= [T1 ^Any _Union{Union{String, T}, T} R [false|2|0] false] [T ^String _Union{} L [false|0|0] false]  ||| 
                   === stats ===
Rule Name                         # occs  success
Top                         =>         3     100%
R_Right                     =>         2     100%
R_Intro                     =>         1       0%
Tuple                       =>         1       0%
L_Intro                     =>         1       0%

I didn’t see examples like this one discussed in the paper, I think? I guess their fuzzer just didn’t catch this particular issue? Too bad, this might be much harder to fix now that Julia has stabilized :pensive:. @ckfinite I see you’re active now, perhaps you’re interested, care to comment?

2 Likes
9

From what I recall, we tried but weren’t able to prove transitivity though I do not remember where we got stuck. Moreover, our exploration of lower bounds (a la SupStr) was limited, as we found out in later work. It’s not at all surprising to me that the fuzzer missed transitivity issues, as a result; the space is huge and I expect that there’s many more examples. I’d only trust a proof to guarantee transitivity and those are both very hard to do and tend to operate on subsets of actual type systems.

In later work (under submission now), we do prove transitivity for a weaker version of the type system that restricts how you use lower bounds. In particular, the Tuple{T,T} where T >: String would be forbidden and you’d need to write Tuple{>:String,>:String} instead. This restriction avoids the very problematic secondary equality check that we also used to prove undecidability.

4 Likes
10

@N5N3 managed to fix this already! Thanks so much! PR: Subtype: Fix some diagonal rule related false alarm by N5N3 · Pull Request #53034 · JuliaLang/julia · GitHub

7 Likes