JuliaLang / julia

The Julia Programming Language
https://julialang.org/
MIT License
44.95k stars 5.42k forks source link

recursive type parameter constraints #54838

Open nsajko opened 2 weeks ago

nsajko commented 2 weeks ago

I don't think describing this type is currently possible in Julia:

julia> struct S{A,B<:Union{Nothing,S{A}}}
           a::A
           b::B
       end
ERROR: UndefVarError: `S` not defined in local scope
Suggestion: check for an assignment to a local variable that shadows a global of the same name.
Stacktrace:
 [1] top-level scope
   @ REPL[1]:1

julia> versioninfo()
Julia Version 1.12.0-DEV.740
Commit 319d8900dbb (2024-06-15 22:59 UTC)
Build Info:
  Official https://julialang.org/ release
Platform Info:
  OS: Linux (x86_64-linux-gnu)
  CPU: 8 × AMD Ryzen 3 5300U with Radeon Graphics
  WORD_SIZE: 64
  LLVM: libLLVM-17.0.6 (ORCJIT, znver2)

The intention is for S to be a homogeneous list type with statically-known length, so S{A} should be roughly equivalent to Tuple{Vararg{A}}.

EDIT: @kimikage gives a partial workaround for my usecase (describing the homogeneity of S in the type system) below, by introducing a supertype parameterized by the element type.

nsajko commented 2 weeks ago

Perhaps an OK way to get better type inference is to make the instance properties private, and define a getter with appropriate type assertions. Something like:

function list_tail(l::S)
    r = l.b
    r::Union{Nothing,S{typeof(l.a)}}
end

After applying @kimikage's workaround below, the getter could be simplified to:

function list_tail(l::S)
    r = l.b
    r::Union{Nothing,S}
end
kimikage commented 2 weeks ago

BTW, I think the typical and practical workaround for this is to use abstract types.

abstract type AbstractS{A} end

struct S{A,B<:Union{Nothing,AbstractS{A}}} <: AbstractS{A}
    a::A
    b::B
end

I think it is somewhat misleading to bring up the S{A,B} without constraints.

nsajko commented 1 week ago

This is pretty nice, thank you very much, though not perfect on its own. The subtyping in your solution guarantees that, for any s isa S, the element type of s.b is the same as the element type of s if s.b isa S.

When combined with my getter-with-type-assertions solution above, I suppose this should be able to convince type inference of the homogeneity, though.