How about allowing an abstract type to be frozen (or, perhaps, closed) at some point? After the abstract type is frozen, any attempt at adding a new subtype to it would throw. Example:
abstract type A end
struct S <: A end
freeze_abstract_type(A)
struct T <: A end # throws!
The motivation is that subtyping could then use the fact that the set of subtypes is closed. For example, the subtyping query here should be able to return true
if we were to freeze A
before doing A <: Union{S,T}
:
julia> abstract type A end
julia> struct S <: A end
julia> struct T <: A end
julia> A <: Union{S,T}
false
FTR this proposal is basically an alternative to the following feature request:
Motivating example 1: Peano natural numbers in the type domain
Suppose we’re implementing natural numbers in the type domain recursively, like in Peano’s construction. Ref Haskell Wiki, Wikipedia.
First try
An initial attempt might look like so:
"""
Nat(predecessor)
The `predecessor` must be either:
* `nothing`, we have `iszero(Nat(nothing))`
* a `Nat`
"""
struct Nat{Predecessor} <: Integer
predecessor::Predecessor
end
The obvious problem with the above is the absence of type safety, also resulting in bad abstract type inference. E.g., Nat{Float32}
or Nat{:some_symbol}
don’t throw.
Second try
We could make the design stricter by adding some abstract types:
recursive_step(t) = Union{Nothing,t}
abstract type UpperBound0{P <: recursive_step(Integer)} <: Integer end
abstract type UpperBound1{P <: recursive_step(UpperBound0)} <: UpperBound0{P} end
"""
Nat(predecessor)
The `predecessor` must be either:
* `nothing`, we have `iszero(Nat(nothing))`
* a `Nat`
"""
struct Nat{
Predecessor <: recursive_step(UpperBound1),
} <: UpperBound1{Predecessor}
predecessor::Predecessor
end
Now we have a design that’s type safe as long as no new subtypes are added to the abstract types:
julia> Nat{Float32}
ERROR: TypeError: in Nat, in Predecessor, expected Predecessor<:Union{Nothing, UpperBound1}, got Type{Float32}
Stacktrace:
[1] top-level scope
@ REPL[5]:1
However, the type inference is still not perfect, not without adding some type assertions:
julia> Base.infer_return_type((n -> n.predecessor), Tuple{Nat})
Union{Nothing, UpperBound1}
julia> Base.infer_return_type((n -> n.predecessor.predecessor), Tuple{Nat})
Any
Ideally, both results would be Union{Nothing,Nat}
, but this isn’t possible because Julia’s subtyping assumes further subtypes may be added to the abstract types. Thus my feature request.
Motivating example 2: recursive data structure
Suppose we’re implementing a recursive homogeneous nonempty ordered collection of compile-time constant length. Basically a recursive equivalent to Tuple{X, Vararg{X}} where {X}
. Homogeneous trees, etc., might instead be constructed using a similar approach.
First try
A design lacking type safety:
"""
List(elem, tail)
Construct a single-element list like so: `List(elem, nothing)`.
Prepend an element to an existing list like so: `List(elem, existing_list)`.
"""
struct List{Element, Tail}
first_element::Element
tail::Tail
end
The type system doesn’t help enforce the homogeneity of List
:
julia> L1 = List{Int, Nothing}
List{Int64, Nothing}
julia> List{Float32, L1} # want this to throw
List{Float32, List{Int64, Nothing}}
Second try
recursive_step(t) = Union{Nothing,t}
abstract type UpperBound0{E, T <: recursive_step(AbstractVector{E})} <: AbstractVector{E} end
abstract type UpperBound1{E, T <: recursive_step(UpperBound0{E})} <: UpperBound0{E,T} end
struct List{
Element,
Tail <: recursive_step(UpperBound1{Element}),
} <: UpperBound1{Element, Tail}
first_element::Element
tail::Tail
end
Again, we achieved type safety, as long as the abstract types don’t get any new subtypes:
julia> L1 = List{Int, Nothing}
List{Int64, Nothing}
julia> List{Int, L1}
List{Int64, List{Int64, Nothing}}
julia> List{Float32, L1}
ERROR: TypeError: in List, in Tail, expected Tail<:Union{Nothing, UpperBound1{Float32, T} where T<:Union{Nothing, UpperBound0{Float32, T} where T<:Union{Nothing, AbstractVector{Float32}}}}, got Type{List{Int64, Nothing}}
Stacktrace:
[1] top-level scope
@ REPL[7]:1
julia> List{Int, Int}
ERROR: TypeError: in List, in Tail, expected Tail<:Union{Nothing, UpperBound1{Int64, T} where T<:Union{Nothing, UpperBound0{Int64, T} where T<:Union{Nothing, AbstractVector{Int64}}}}, got Type{Int64}
Stacktrace:
[1] top-level scope
@ REPL[8]:1
Again, the type inference fails:
julia> Base.infer_return_type((n -> n.tail), Tuple{List{Bool}})
Union{Nothing, UpperBound1{Bool, T} where T<:Union{Nothing, UpperBound0{Bool, T} where T<:Union{Nothing, AbstractVector{Bool}}}}
julia> Base.infer_return_type((n -> n.tail.tail), Tuple{List{Bool}})
Any