[Pitch] Dependent Integer Expressions in Generic Arguments

Evolution Pitches
,
1

Hey all,

I've been working on several small prototypes of this ever since SE-0452 originally introduced integer generic parameters and mentioned arithmetic generics in the "Future directions" section. Since SE-0531 (literal expressions in integer generic argument positions) got accepted recently too, I decided to make another prototype and got far enough this time that I wanted to pitch it for real.

Basically, Swift still cannot use arithmetic with integer generic parameters in generic argument positions to do things like this:

struct Vector<let count: Int, Element> {}

func concatenated<let lhsCount: Int, let rhsCount: Int, Element>(
    _ lhs: Vector<lhsCount, Element>,
    _ rhs: Vector<rhsCount, Element>
) -> Vector<(lhsCount + rhsCount), Element>

The pitch keeps SE-0531's required parentheses, but extends the expressions inside them to include integer generic parameters and a bounded set of Int operations. In my prototype, the signature above is accepted, allowing the result type to retain the relationship between its input sizes.

Literal subexpressions continue to use SE-0531's existing folding rules. For example, Vector<(count + (2 + 3)), Element> still becomes Vector<(count + 5), Element>. The dependent generic part of an expression retains its ordered tree though: Vector<(n + m), Element> and Vector<(m + n), Element> are distinct. I initially tried to add a more general algebraic-equivalence system, but obviously the complexity of that really ballooned, even when my prototype was just working with + and * operators. I think keeping the whole expression tree structure ended up making the most sense for many reasons.

I've currently got support for all of the Int arithmetic, bitwise, shift, and unary operators supported by the literal expressions from SE-0531. For now, division and remainder require a divisor that SE-0531 can fold to a nonzero integer. Supporting a dependent divisor would require a way to state a divisor != 0 constraint in a generic signature, which this pitch deliberately leaves out of scope.

This is my first pitch (and first post!) even though I've followed the Swift Evolution forums for several years now. I'm really looking forward to hearing your feedback and thoughts!

The current proposal draft is here:

https://github.com/Brennanium/swift-evolution/blob/dependent-integer-generic-expressions/proposals/NNNN-dependent-integer-expressions.md

The compiler prototype and tests are here:

https://github.com/Brennanium/swift/tree/dependent-integer-generic-expressions

20 Likes
2

I'm mostly going to stay out of this, but please make sure the compiler doesn't assume Foo<(n + m)> and Foo<(m + n)> (and Foo<n> and Foo<7> and Foo<(a + b + c)>) are not the same type. That should be fine since Foo<T> and Foo<U> are already a well-tested version of this, but it'd be really bad to get it wrong. :sweat_smile:

2 Likes
3

Yeah for sure! The compiler does not assume they are unequal once the generic arguments become concrete. Foo<(n + m)>and Foo<(m + n)> are distinct symbolic forms in a generic context, just like Foo<n> and Foo<7>. Once the generic arguments are concrete, the expressions evaluate normally, so both Foo<(3 + 4)> and Foo<(4 + 3)> are Foo<7>.

5 Likes
4

This looks good. Just want to drop in with two edge-case nits:

It is also currently possible (probably shouldn't be, but alas) for end users to alter the precedence group (and hence associativity and precedence) of stdlib operators locally within their own code. It would probably be right to (and also sufficient to) reject attempts to use stdlib operators in generic contexts when their precedence group has been altered, so as to avoid 2 * 2 + 3 evaluating to different results inside versus outside angle brackets.

It's sort of implied by your text, but the implementation must be sure that whether this is accepted and evaluates to count >> 1 depends on whether << resolves to the expected stdlib function, not >>.

4 Likes
5

Holy good catch! Allowing local precedence override like that is crazy tbh :sweat_smile: I just checked and it appears to not be properly handled by both this prototype and the already accepted SE-0531 literal expressions as well actually. I've got a quick fix for both now.

Also adding a small wording change to not imply that << gets resolved as >> for real, just that the result is the same based on normal << smart shift behavior.

1 Like
6

I've fixed several small bugs and all the tests are passing, also rebased with @ArtemC's recent literal expression fixes in main. Anyone gotten a chance to try out my branch yet?

7

I think the use-cases here are compelling, it would be nice to be able to write:

extension InlineArray {
  func appended<let k: Int>(_ o: InlineArray<k, Element>)
    -> InlineArray<(count + k), Element>
}

A few notes in no particular order:

The various examples in the pitch put the dependent type in the return position, e.g.

func concatenated<let lhsCount: Int, let rhsCount: Int, Element>(
  _ lhs: Vector<lhsCount, Element>,
  _ rhs: Vector<rhsCount, Element>
) -> Vector<(lhsCount + rhsCount), Element>

Can you expand on what happens when putting a dependent generic value expression in parameter position? e.g.

let v5 = [5 of Int](repeating: 1)
func f<let n: Int>(_ :[(n + 1) of Int]) {}
f(v5) // error: cannot convert value of type '[5 of Int]' to expected argument type '[n + 1 of Int]'
      // error: generic parameter 'n' could not be inferred

A dependent divisor would require a value constraint such as divisor != 0 to make that property part of a generic signature; this proposal intentionally does not add value constraints.

For example, evaluating Vector<(count + 1), Element> with count == Int.max traps.

Why does division by zero get a different treatment from overflow? It seems that the proposal would be simplified a bit if division by zero got treated the same way as overflow, which gets treated the same way as any other runtime arithmetic fault.

An API using the same structural expression can consume the result directly; the proposal does not infer an equivalent differently spelled expression.

Structural identity makes these distinct types:

func makeSum<let n: Int, let m: Int, Element>(...) -> Vector<(n + m), Element>
func takeSum<let n: Int, let m: Int, Element>(_ v: Vector<(m + n), Element>)

takeSum(makeSum(a, b))   // ?

If I understand this correctly, then according to this proposal there isn't a way to do this, which means that two libraries that pick different spellings for the same relationship then can't interoperate.

In the | Expression | Behavior | table:

| `Vector<(count << -1), Element>` | Has the same result as `count >> 1` (smart shift). |

I found this confusing because it conflates identity and evaluation, since this is true for the latter and false for the former.

1 Like
8

The second n would evaluate to the first m and vice versa, right? The issue would only arise if this were in some context where they must be the same thing, e.g:

struct Foo<let n: Int, let m: Int, Element> {
  func makeSum(...) -> Vector<(n + m), Element> { ... }
  func takeSum(_ v: Vector<(m + n), Element>) { ... }

  func frobnicate() {
    self.takeSum(self.makeSum(...))
  }
}
3 Likes
9

@bbrk24 is right in this case; @ArtemC's specific example of structural identity mismatch actually compiles just fine since the generic parameters of both functions are independent from each other:

func makeSum<let n: Int, let m: Int, Element>() -> Vector<(n + m), Element>
func takeSum<let x: Int, let y: Int, Element>(_ v: Vector<(x + y), Element>)

takeSum(makeSum(a, b)) // compiles just fine n->x and m->y

When the generic parameters are already bound like in @bbrk24's struct example, that's when it does pose a problem where (n + m) is structurally not equivalent to (m + n)

1 Like
10

Thanks @ArtemC these are all great points! I'll go through and try to address these one by one.

Including more examples in parameter positions is definitely something I need to expand on in the pitch document and tests. This particular function has no source to infer n from since there's no way (yet) for the compiler to solve the equation n + 1 == 5 to infer n == 4. In other examples where we expect to get a generic parameter X could not be inferred error:

func consume<T>(_ value: [T]) {}
consume([]) // error: generic parameter 'T' could not be inferred

We can easily fix this by just specifying the type another way like:

func consume<T>(_ value: [T]) {}
consume([] as [Int]) // no error

The problem with your func f<let n: Int>(_ : [(n + 1) of Int]) {} example is that in a concrete call with only v5, there is no way for the compiler to ever infer n without solving n + 1 == 5; there's no equivalent of the as [Int] example since it's always dependent, and there are no other clues in the function signature to disambiguate. I did initially think that your function signature was actually impossible to resolve concretely, but with some experimenting I did find a situation that does actually compile just fine:

func f<let n: Int>(_ value: [(n + 1) of Int]) {}

func g<let n: Int>(
  _ first: [n of Int],
  _ second: [(n + 1) of Int]
) {
  f(second)
}

g([4 of Int](repeating: 0), [5 of Int](repeating: 0)) // compiles

I didn't expect the compiler to be able to figure out f.n like that honestly! The compiler is not solving f.n + 1 == 5 backward here of course, but it does seem to be able to match f’s (n + 1) parameter against g’s already-known (n + 1) parameter and instantiate f’s independent n with g’s symbolic n somehow.
While it does seem a bit strange to have a function signature like f be allowed when its use is limited to a very specific context like this, I don't really see a way to cleanly diagnose this as an issue either. Documenting this behavior is important though and I'll definitely be adding some cases to the pitch document to clarify this.

I think you're right here actually. I'm not sure why the trapping for overflow seemed more natural than trapping for divide by 0, but fundamentally there isn't really a reason why divide by 0 is any more scary than an overflow or anything :sweat_smile: looking back it was pretty arbitrary on my part. I already have a branch that allows the full division / remainder functionality; I'll try and get that pulled into the main prototype branch and I'll update the pitch to reflect that too.

This was partially answered above by @bbrk24's example. In your specific small example, the two free functions can compose since their generic parameters are inferred independently. The limitation only arises when the parameters are already bound in a shared generic context:

struct Foo<let n: Int, let m: Int, Element> {
  func makeSum(...) -> Vector<(n + m), Element> { ... }
  func takeSum(_ value: Vector<(m + n), Element>) { ... }

  func frobnicate() {
    takeSum(makeSum(...)) // rejected
  }
}

There is no current way to prove n + m and m + n are equivalent here. It was initially very tempting to try to implement some basic algebraic equivalence checking by like canonicalizing the order in subexpressions with commutative operators or grouping constants, but the complexity really exploded and I ran into some serious ABI stability issues. If we start adding some basic algebraic equivalence checking, any tiny change to that algebraic equivalence model later on could retroactively change generic type identity and potentially break ABI.

Yeah... @xwu had similar issues with my explanation before and my attempt to clarify things is still quite confusing I guess. The expression is accepted and retains the structural identity count << -1; when evaluated, Swift's smart shift semantics produce the same value as count >> 1 though.

1 Like
11

Updated code and pitch document based on @ArtemC and @bbrk24's comments available now

1 Like