[FR] allow "freezing" an abstract type, making future attempts of adding a subtype throw

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
1 Like

Julia is designed to be flexible. “Freezing” the abstract type would likely not get you a safe system, but rather yet another promise that can subtly be broken or something along the line. Even if that’s not the case, the type “safe” example may be kinda “safe”, but actually produces really hard-to-read message.

The magic of Julia is that things just work. Maybe adding some restrictions here and there won’t be problems today, but who knows what happens tomorrow? It’s another reason I think interfaces shouldn’t be added to Julia either. In my experiences, interfaces are nightmarish systems to wrangle with for the benefit of saving a few seconds of looking at the stack trace and correcting the type of the argument.

Let Julia be the performant generic language.