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

**URL:** <https://discourse.julialang.org/t/fr-allow-freezing-an-abstract-type-making-future-attempts-of-adding-a-subtype-throw/119554>\
**Category:** Internals & Design\
**Tags:** type, parametric-types, feature-request\
**Created:** [September 18, 2024, 2:58pm UTC](https://discourse.julialang.org/t/fr-allow-freezing-an-abstract-type-making-future-attempts-of-adding-a-subtype-throw/119554 "2024-09-18T14:58:20Z")\
**Posts on this page:** 2\
**Page:** 1

<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:** [September 18, 2024, 2:58pm UTC](https://discourse.julialang.org/t/fr-allow-freezing-an-abstract-type-making-future-attempts-of-adding-a-subtype-throw/119554/1 "2024-09-18T14:58:20Z")

</div>

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:

```julia
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-repl
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:

> <https://github.com/JuliaLang/julia/issues/54838>
>
> I don't think describing this type is currently possible in Julia:
> 
> \`\`\`julia-r…epl
> 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.

## 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](https://wiki.haskell.org/Peano_numbers), [Wikipedia](https://en.wikipedia.org/wiki/Peano_axioms).

### First try

An initial attempt might look like so:

```julia
"""
    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:

```julia
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-repl
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-repl
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:

```julia
"""
    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-repl
julia> L1 = List{Int, Nothing}
List{Int64, Nothing}

julia> List{Float32, L1} # want this to throw
List{Float32, List{Int64, Nothing}}

```

### Second try

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

```

---

<div class="post-metadata">

**Author:** ![Tarny\_GG\_Channie](https://avatars.discourse-cdn.com/v4/letter/t/3bc359/32.png) [@Tarny\_GG\_Channie](https://discourse.julialang.org/u/Tarny_GG_Channie)\
**Post date:** [September 19, 2024, 10:50am UTC](https://discourse.julialang.org/t/fr-allow-freezing-an-abstract-type-making-future-attempts-of-adding-a-subtype-throw/119554/2 "2024-09-19T10:50:46Z")

</div>

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.
