[codex] Add pack count constraint proposal

[csyonghe]

Summary

Adds SP #41, a language proposal for variadic pack count constraints:

where countof(Pack) == IntExpr

The proposal documents the feature as an oriented pack-shape proof rather than a general integer equality system.

Design Points Covered

• Type-pack and value-pack support.
• Exact declared-witness forwarding for nested generic bodies.
• Validation-only behavior: no inference of N from countof(T).
• Oriented syntax only: countof(Pack) must be on the left side.
• Rejection of !=, >=, and RHS countof(...) spellings.
• The non-goal of algebraic proofing for cases such as countof(T) + 1 == N.
• The non-goal of symmetric witness use for countof(T) == countof(U).
• AST, witness solving, signature matching, lowering, diagnostics, alternatives, and future directions.

Validation

• git.exe diff --cached --check before commit.
• Proposal-only change; no compiler tests required in this repo.

[skiminki-nv]

Just a note. This probably refers to the sizeof... operator.

Something like the below is probably the model example:

#include <cstddef>
#include <initializer_list>
#include <iostream>
#include <type_traits>

template <typename FirstArgType, typename SecondArgType, typename... RestArgTypes>
constexpr bool areSameTypes() noexcept
{
    if constexpr(sizeof...(RestArgTypes) == 0U)
        return std::is_same_v<FirstArgType, SecondArgType>;
    else
        return
            std::is_same_v<FirstArgType, SecondArgType> &&
            areSameTypes<FirstArgType, RestArgTypes...>();
}

template <size_t N, typename FirstArgType, typename... RestArgTypes>
requires (sizeof...(RestArgTypes) + 1U == N &&
          areSameTypes<FirstArgType, RestArgTypes...>())
auto sumArgs(FirstArgType arg, RestArgTypes... args) -> FirstArgType
{
    FirstArgType ret { };
    for (auto i : std::initializer_list<FirstArgType> { arg, args... })
        ret += i;

    return ret;
}

int main()
{
    // Declared argument count must match the number of arguments.
    // Argument types must be the same.
    std::cout << "Sum: " << sumArgs<3>(1.0, 2.5, 3.0) << std::endl;
}

[skiminki-nv]

I'm not particularly fond of adding new where-clause syntax here. For the long run, better would be to allow boolean-typed constraint expressions, and if necessary, optimize expressions such as countof(T) == N for the equivalent overload resolution perf.

However, the current approach should be extensible to the more generic approach without breakages, if we'd ever implement one. So, this is again, more a note than anything else.

[csyonghe]

This alternative, along with the reasoning to go with the current approach is discussed in "alternative solutions" section below.

[skiminki-nv]

While this proposal is useful as a generic API constraint, I would perhaps also add the concrete motivation behind this proposal, which is the overload resolution perf (IIUC).

That is, the new where counof(...) == N constraint allows the compiler to quickly discard a bunch of overload candidates in case the application has declared a large number of those with a differing number of arguments.

[csyonghe]

Done.

[juliusikkala]

Could general value constraints be achievable the same way, by always requiring that the left side is a reference to a generic parameter?

[csyonghe]

yes, but that is kept out of this proposal to keep the scope small.

[tangent-vector]

I strongly agree with keeping this as constrained as possible to begin with, but it is probably worth noting that this proposal is syntactically compatible with the possibility of us allowing arbitrary relational expressions (or perhaps even arbitrary boolean expressions) as where clauses. The restrictions being described limit the scope of what is currently permitted, but not of what the language syntax can express.

That detail sets a general precedent for what we should aspire to going forward: new where clause cases should ideally all fit the model of where <expr>, and not introduce syntax that would make it harder to parse that general case down the line.

[juliusikkala]

I think this should be rejected altogether, not only for the initial feature. One can form fifth-degree equations to make this practically unsolvable: where countof(TIndex) == 3*N*N*N*N*N-2*N*N*N+N*N+N-432

It can also have interesting ambiguities: where countof(TIndex) == N+M or where countof(TIndex) == N*N.

[csyonghe]

Yes, I don't think we can support this any time soon, if ever.

[tangent-vector]

I would note that we should make a distinction between "may" and "must" here. We could say that an implementation of Slang may infer N == 3 from the example given, but not that it must do so.

At some point, the road we are heading down somewhat necessarily involves inference becoming best-effort in certain complex scenarios, and spelling out exactly when the inference will succeed or not would be akin to spelling out under what conditions a theorem prover is guaranteed to find a solution.

We are still in the world of spelling out cases where the compiler must be able to perform inference, but I think we will soon need to accept that there is going to be the middle ground of things that we cannot promise the compiler will or won't infer.

[juliusikkala]

So, any integer expression is OK?

• Is N+{1} going to be legal?
  • I'm asking this with parsing in mind. That's not impossible to parse by any means, but could prove annoying in the long run. Particularly so, if we ever allow the C++-style Type{initializer} syntax.
• Can parentheses be used too, like (N - 1)?
• countof(T) == countof(T)?
• countof(T) == U<countof(T)>.Member? (where U<int N> contains static const int Member = N;)

[csyonghe]

This means any expr that is already allowed in compile-time constant locations such as in foo<expr>.

[tangent-vector]

I think the proposal looks good as-is. I have one place where I made a request for more detail on alternatives, but I consider that a nice-to-have request rather than a hard requirement before we can merge this.

[tangent-vector]

Unrelated to this specific proposal, but allowing nested generics (or nested declarations in general) to include where clauses that place additional constraints on outer generic parameters is a nice-to-have feature with clear semantics ("this member/method is only usable when the client can prove that these additional constraints are satisfied"). It wouldn't express anything that couldn't be done via an extension, but might still be a convenient syntax.

[tangent-vector]

Again, not actually related to this PR, but it is worth stating as a general principle: the front-end semantic checking step is responsible for generating all of the concrete proofs as well as the code that manipulates and constructs proofs (which then gets lowered to the IR). If we end up including a more general proof assistant into Slang at some point (as a way to try and handle fully general constraint equations), it would be integrated into the front-end only, and the IR passes and compiler backend would remain deterministic and (comparatively) simple.

[tangent-vector]

I strongly agree with keeping this as constrained as possible to begin with, but it is probably worth noting that this proposal is syntactically compatible with the possibility of us allowing arbitrary relational expressions (or perhaps even arbitrary boolean expressions) as where clauses. The restrictions being described limit the scope of what is currently permitted, but not of what the language syntax can express.

That detail sets a general precedent for what we should aspire to going forward: new where clause cases should ideally all fit the model of where <expr>, and not introduce syntax that would make it harder to parse that general case down the line.

[tangent-vector]

I would note that we should make a distinction between "may" and "must" here. We could say that an implementation of Slang may infer N == 3 from the example given, but not that it must do so.

At some point, the road we are heading down somewhat necessarily involves inference becoming best-effort in certain complex scenarios, and spelling out exactly when the inference will succeed or not would be akin to spelling out under what conditions a theorem prover is guaranteed to find a solution.

We are still in the world of spelling out cases where the compiler must be able to perform inference, but I think we will soon need to accept that there is going to be the middle ground of things that we cannot promise the compiler will or won't infer.

[tangent-vector]

Having read through the material here, I think the main alternative I would have liked to see discussed that isn't covered here is the option of making other changes to the language so that instead of expressing a constraint on two separately declared things (e.g., an integer generic parameter N and a variadic type pack parameter Indices) one instead derives one part from the other, or both from a single source of truth.

As an example, a simplistic idea might be a way to represent a type pack parameter that either takes a specific arity (an integer constant). E.g.:

struct Tensor<T, let Rank : int>
{
    T load<each[Rank] Index>(Index indices)
        where Index == int
    {
        ...
    }
}

Here I'm making up the notation each[...] to represent a type parameter pack with a pre-determined arity. In practice, that would be semantically comparable to a where countof(Index) == Rank, but also more directly encodes one of the limitations that this proposal relies on: the arity constraint can only apply directly to a pack parameter (always declared with each).

The same basic feature could be used to describe cases where the arity of an each pack parameter should be exactly that of another parameter via each[countof(OtherParameter)].

Under this model, a declaration like the following, given earlier in the proposal:

void foo<let N : int, each I>()
    where countof(I) == N
{ ... }

would instead become:

void foo<let N : int, each[N] I>()
{ ... }

This perhaps even models what a pack parameter really is "under the hood" more directly, since it reflects how a pack parameter is effectively a parameter of type Type[] - that is, an array of some unknown number of types - and this notation is just allowing a parameter to be Type[N] - an array of a known number of types.

On balance, I think the proposal here is a good one to follow through on, but I would like to see the alternative at least discussed and hear the rationale for why we shouldn't do something along these lines.