# Intransitivities in subtyping

**URL:** <https://discourse.julialang.org/t/intransitivities-in-subtyping/109266>\
**Category:** Internals & Design\
**Created:** [January 22, 2024, 2:33pm UTC](https://discourse.julialang.org/t/intransitivities-in-subtyping/109266 "2024-01-22T14:33:42Z")\
**Posts on this page:** 9\
**Page:** 1

<div class="post-metadata">

**Author:** ![foobar\_lv2](https://avatars.discourse-cdn.com/v4/letter/f/ee59a6/32.png) [@foobar\_lv2](https://discourse.julialang.org/u/foobar_lv2)\
**Post date:** [January 22, 2024, 2:33pm UTC](https://discourse.julialang.org/t/intransitivities-in-subtyping/109266/1 "2024-01-22T14:33:42Z")

</div>

I think the WAT on subtyping is

```julia
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.

---

<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:** [January 22, 2024, 2:37pm UTC](https://discourse.julialang.org/t/intransitivities-in-subtyping/109266/2 "2024-01-22T14:37:07Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![foobar\_lv2](https://avatars.discourse-cdn.com/v4/letter/f/ee59a6/32.png) [@foobar\_lv2](https://discourse.julialang.org/u/foobar_lv2)\
**Post date:** [January 22, 2024, 2:53pm UTC](https://discourse.julialang.org/t/intransitivities-in-subtyping/109266/3 "2024-01-22T14:53:33Z")

</div>

> [@nsajko](#):
>
> Is there a bug report already?

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)

---

<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:** [January 23, 2024, 1:38pm UTC](https://discourse.julialang.org/t/intransitivities-in-subtyping/109266/4 "2024-01-23T13:38:48Z")

</div>

> [@foobar\_lv2](#):
>
> I think the WAT on subtyping is
> 
> ```julia
> 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.

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-repl
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](https://github.com/JuliaLang/julia/issues/53019)

---

<div class="post-metadata">

**Author:** ![foobar\_lv2](https://avatars.discourse-cdn.com/v4/letter/f/ee59a6/32.png) [@foobar\_lv2](https://discourse.julialang.org/u/foobar_lv2)\
**Post date:** [January 23, 2024, 2:13pm UTC](https://discourse.julialang.org/t/intransitivities-in-subtyping/109266/5 "2024-01-23T14:13:35Z")

</div>

> [@nsajko](#):
>
> 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:

`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`.

> [@A most harrowing collection of Julia WATs](https://discourse.julialang.org/t/a-most-harrowing-collection-of-julia-wats/77323/102):
>
> This thread has been going on for 2 years and has become an unorganized grab-bag of unrelated discussions. As such, it’s a prime case for [Time limits for unfocused discourse threads?](https://discourse.julialang.org/t/time-limits-for-unfocused-discourse-threads/106739).

👍 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.

---

<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:** [January 23, 2024, 2:13pm UTC](https://discourse.julialang.org/t/intransitivities-in-subtyping/109266/6 "2024-01-23T14:13:42Z")

</div>

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

> <https://github.com/JuliaLang/julia/issues/53021>
>
> Here's a Git repository containing a Julia package that generates counterexample…s to the transitivity property that \`\<:\` is supposed to satisfy:
> 
> https://gitlab.com/nsajko/SubtypingRelationExperiments.jl
> 
> So far I tested it on v1.10 and v1.11-DEV: the results between these two versions are the same and may be found under \`results/\`. I'll give just two of the counterexamples here, see the rest on my repo:
> 
> This is the first counterexample in the results:
> 
> \`\`\`
> counterexample triplet: (Tuple{X, X} where X\<:Union{}, Tuple{C, C}, Tuple{X, X, Vararg{Any}} where C\<:X\<:C)
> \`\`\`
> 
> In the REPL:
> 
> \`\`\`julia-repl
> julia\> struct C end
> 
> julia\> const T1 = Tuple{X, X} where X\<:Union{}
> Tuple{X, X} where X\<:Union{}
> 
> julia\> const T2 = Tuple{C, C}
> Tuple{C, C}
> 
> julia\> const T3 = Tuple{X, X, Vararg{Any}} where C\<:X\<:C
> Tuple{X, X, Vararg{Any}} where C\<:X\<:C
> 
> julia\> T1 \<: T2 \<: T3
> true
> 
> julia\> T1 \<: T3
> false
> \`\`\`
> 
> This is the last counterexample in the results:
> 
> \`\`\`
> counterexample triplet: (Tuple{A, X, Vararg{X}} where X\<:C, Tuple{Any, Vararg{C}}, Tuple{Any, Vararg{X}} where X\>:C)
> \`\`\`
> 
> In the REPL:
> 
> \`\`\`julia-repl
> julia\> abstract type A end
> 
> julia\> struct C \<: A end
> 
> julia\> const T1 = Tuple{A, X, Vararg{X}} where X\<:C
> Tuple{A, X, Vararg{X}} where X\<:C
> 
> julia\> const T2 = Tuple{Any, Vararg{C}}
> Tuple{Any, Vararg{C}}
> 
> julia\> const T3 = Tuple{Any, Vararg{X}} where X\>:C
> Tuple{Any, Vararg{X}} where X\>:C
> 
> julia\> T1 \<: T2 \<: T3
> true
> 
> julia\> T1 \<: T3
> false
> \`\`\`

> **[Neven Sajko / SubtypingRelationExperiments.jl · GitLab](https://gitlab.com/nsajko/SubtypingRelationExperiments.jl)**
>
> An experiment for finding counterexamples to the preorder properties that Julia's subtyping is supposed to satisfy.

---

<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:** [January 23, 2024, 11:00pm UTC](https://discourse.julialang.org/t/intransitivities-in-subtyping/109266/8 "2024-01-23T23:00:20Z")

</div>

> [@nsajko](#):
>
> 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?

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-repl
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 😔. @ckfinite I see you’re active now, perhaps you’re interested, care to comment?

---

<div class="post-metadata">

**Author:** ![ckfinite](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/ckfinite/32/8341_2.png) [@ckfinite](https://discourse.julialang.org/u/ckfinite)\
**Post date:** [January 24, 2024, 1:11am UTC](https://discourse.julialang.org/t/intransitivities-in-subtyping/109266/9 "2024-01-24T01:11:21Z")

</div>

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.

---

<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:** [January 25, 2024, 5:00pm UTC](https://discourse.julialang.org/t/intransitivities-in-subtyping/109266/10 "2024-01-25T17:00:16Z")

</div>

> [@nsajko](#):
>
> generated a considerable number of intransitive subtyping examples

@N5N3 managed to fix this already! Thanks so much! PR: [https://github.com/JuliaLang/julia/pull/53034](https://github.com/JuliaLang/julia/pull/53034)