Proposal: Variadics

proposals/p2240.md

@@ -28,6 +28,13 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
  - [Variadic types](#variadic-types)
  - [Expressions](#expressions)
  - [Patterns](#patterns)
+ - [Tuple type](#tuple-type)
+ - [Identifying potential matchings](#identifying-potential-matchings)
+ - [The type-checking algorithm](#the-type-checking-algorithm)
+ - [Parameterized class type](#parameterized-class-type)
+ - [Identifier that names a deduced parameter](#identifier-that-names-a-deduced-parameter)
+ - [Name binding pattern](#name-binding-pattern)
+ - [`[:]` pattern](#-pattern)
  - [Statements](#statements)
 - [Rationale](#rationale)
 - [Alternatives considered](#alternatives-considered)
@@ -149,12 +156,13 @@ fn StrCat[T:! [ConvertibleToString;]](..., [:]params: T) -> String {
 ```
 
 ```carbon
-// Returns the minimum of its arguments, which must all have the same type T
-fn Min[template N:! BigInt if N > 0, T:! Comparable & Value]
- (..., [:]params: [T; N]) -> T {
- // Safe since params non-empty
- var result: T = params[0];
- for (var x: T in params.Slice(1..)) {
+// Returns the minimum of its arguments, which must all have the same type T.
+//
+// Note that this implementation is not recursive. We split the parameters into
+// first and rest in order to forbid calling `Min` with no arguments.
+fn Min[T:! Comparable & Value](first: T, ..., [:]rest: [T; N]) -> T {
+ var result: T = first;
+ for (var x: T in rest) {
  if (x < result) {
  result = x;
  }
@@ -190,6 +198,14 @@ fn Zip[ElementTypes:! [Type;]]
 fn MiddleVariadic(first: i64, ..., [:]middles: [f64;], last: i64);
 ```
 
+```carbon
+// Toy example of using the result of variadic type deduction.
+fn TupleConcat[T1s: [Type;], T2s: [Type;]](
+ t1: (..., [:]T1s), t2: (..., [:]T2s)) -> (..., [:]T1s, ..., [:]T2s) {
+ return (..., [:]t1, ..., [:]t2);
+}
+```
+
 ## Details
 
 FIXME throughout the following, clarify what parts apply to patterns.
@@ -588,85 +604,198 @@ rejected), so we will focus on the semantics of phase 3 when the pattern type is
 a variadic type. Variadic types are themselves patterns, so we will break this
 down into cases based on the possible forms of a pattern.
 
-**NOTE TO READER:** You should probably ignore these examples. I used them as
-test cases when working out the typechecking rules, but they're not integrated
-into the rest of the text.
-
-A:
-
-```
-// OK
-fn F[Ts:! [Type;]](..., [:]args: Ts) -> i32;
+##### Tuple type
 
-fn G[U:! Type; Us:! [Type;]](arg: Vector(U), ..., [:]args: Vector(Us)) -> i32 {
- return F(arg, ..., args);
-}
-```
+FIXME too much nesting
 
-B:
+At type checking time, we don't necessarily know which parameters each argument
+will match with, or the other way around. For example, consider the following
+code:
 
-```
-// OK (but maybe too complex to support?)
-fn F[Ts:! [Type;], Ts:! [Type;]](arg1: (..., [:]Ts), arg2: (..., [:]Ts)) -> i32;
+```carbon
+fun F(a: i32, ..., [:]b: [i32;], c: i32);
 
-fn G[Vs:! [Type;]](..., [:]args: Vector(Vs)) -> i32 {
- return F((..., args), (..., args));
+fun G(..., [:]x: [i32;]) {
+ F(1, 2, ..., [:]x);
 }
 ```
 
-```
-fn F[Ts:! [Type;]](arg1: (..., [:]Ts), arg2: (..., [:]Ts)) -> i32;
+If `x` is empty, the `2` will match with `c`, and otherwise the `2` will match
+with an element of `b`. Similarly, if `x` is not empty, its last element will
+match `c`, and the remaining elements (if any) will match elements of `b`.
+However, at type-checking time we don't know the size of `x` yes, so we don't
+know which will occur. On the other hand, the `1` will always match `a`.
 
-fn G[Vs:! [Type;], Ws:! [Type;]](arg1: (..., [:]Vector(Vs)), arg2: (..., [:]Vector(Ws))) -> i32 {
- // Error: Vs might be different from Ws.
- return F(arg1, arg2);
-}
-```
+In general, We want type checking to fail if any possible monomorphization of
+the generic code would fail to typecheck. In this case that means we want type
+checking to fail if any of the potential argument-parameter mappings could fail
+to typecheck after monomorphization. Furthermore, for reasons of readability as
+well as efficiency, we want type checking to fail if any two potential mappings
+would deduce inconsistent values for any deduced parameter. However, in general
+this is intractable, because the number of distinct ways to map argument
+expressions to parameters is exponential in the number of variadic arguments.
 
-C:
+Introducing type deduction further complicates the situation. For example:
 
-```
-fn F[Ts:! [Type;]](arg: i32, ..., [:]args: Ts) -> i32;
+```carbon
+fun H[Ts:! [type;]](a: i32, ..., [:]b: Ts, c: String) -> (..., [:]Ts);
 
-fn G[Us:! [Type;]](..., [:]args: Us, arg: i32) -> i32 {
- // Error: first element of args might not be i32
- return F(..., args, arg);
-}
+external impl P as ImplicitAs(i32);
+external impl Q as ImplicitAs(String);
 
-fn H() {
- G(1);
+fun I(x: [i32;], y: [f32;], z: [String;]) {
+ result: auto = H(..., [:]x, {} as P, ..., [:]y, {} as Q, ..., [:]z);
 }
 ```
 
-_Variadic tuple type_
-
-A variadic tuple pattern consists of M leading elements, a variadic element
-headed by the `...,` operator, and N trailing elements. The scrutinee type may
-be an ordinary tuple type or a variadic tuple type. If the scrutinee type is an
-ordinary tuple type, it must have at least M+N elements. If the scrutinee type
-is a variadic tuple type, it must have at least M leading elements and at least
-N trailing elements.
-
-The first M elements of the scrutinee are checked against the leading elements
-of the pattern type, the last N elements are checked against the trailing
-elements of the pattern type, and the remaining scrutinee elements (if any) are
-iteratively checked against the variadic element.
-
-_Parameterized class type_
+Here, the deduced type of `result` can have one of four different forms. The
+most general case is
+`(..., [:][i32;], P, ..., [:][f32;], Q, ..., [:][String;])`, and the other three
+cases are formed by omitting the prefix ending with `P` and/or the suffix
+starting with `Q` (corresponding to the cases where `x` and/or `z` are empty).
+Extending the type system to support deduction that splits into multiple cases
+would add a fearsome amount of complexity to the type system.
+
+###### Identifying potential matchings
+
+Our solution will rely on being able to identify which parameters can
+potentially match which arguments. We can do so as follows:
+
+We will refer to the elements of the tuple pattern as "parameters", and the
+elements of the scrutinee expression as "argument expressions". We will reserve
+the term "arguments" for the elements of the scrutinee after monomorphization,
+so a single argument expression may correspond to any number of arguments,
+including zero (but only if the expression is variadic). If any variadic
+argument expressions have sizes that are known at typechecking time, we will
+treat them as a sequence of that many non-variadic argument expressions.
+
+A tuple pattern consists of N leading parameters, optionally followed by a
+variadic parameter headed by the `...,` operator, and then M trailing
+parameters. The scrutinee type must be a tuple type, and can have any number of
+variadic elements.
+
+There must be at least N+M non-variadic argument expressions, because otherwise
+if all variadic argument expressions are empty, there will not be enough
+arguments to match all the non-variadic parameters. We will refer to the Nth
+non-variadic argument expression and the argument expressions before it as
+"leading argument expressions". Similarly, we will refer to the Mth-from-last
+non-variadic argument expression and the argument expressions after it as
+"trailing argument expressions", and any remaining argument expressions as
+"central argument expressions". A "leading argument" is an argument that was
+produced by rewriting a leading argument expression, and likewise for "central
+argument" and "trailing argument".
+
+By construction, there will always be at least N leading arguments, because
+there are N non-variadic leading argument expressions. Likewise, there will
+always be at least M trailing arguments. As a result, a leading parameter can
+only match a leading argument, and so it can only match a leading argument
+expression, and likewise for trailing parameters. Consequently, a leading
+argument expression cannot match a trailing parameter, a trailing argument
+expression cannot match a leading parameter, and a central argument expression
+can only match the variadic parameter.
+
+Consider the i'th non-variadic leading argument expression E. If all the
+variadic argument expressions before it are empty, E will match the i'th leading
+parameter, so E cannot match any earlier parameter. If there are any earlier
+variadic argument expressions, E can be made to match any later leading
+parameter or the variadic parameter, by making one of those earlier variadic
+arguments large enough, but as observed above, E cannot match a trailing
+parameter. If there are no earlier variadic argument expressions, E cannot be
+made to match any later parameter, so it can only match the i'th leading
+parameter.
+
+Next, consider a variadic leading argument expression E that comes before the
+i'th non-variadic leading argument expression, but not before any earlier
+non-variadic argument expression. If E's rewritten size is sufficiently large,
+and all earlier variadic argument expressions are empty, it will simultaneously
+match the i'th leading parameter, all leading parameters after it, and the
+variadic parameter, but as before, it cannot match a trailing parameter.
+
+The same reasoning can be applied to trailing argument expressions, but with
+"before" and "after" reversed. And as noted earlier, central argument
+expressions can only match the variadic parameter. In summary, we can identify
+the possible matches for an argument expression E as follows:
+
+- If E is leading, let i be one more than the number of earlier non-variadic
+ argument expressions:
+ - If E is non-variadic, and there are no earlier variadic argument
+ expressions, then E can only match the i'th leading parameter.
+ - Otherwise, E can match the i'th leading parameter, any later leading
+ parameters, and the variadic parameter.
+- If E is trailing, let i be one more than the number of later non-variadic
+ argument expressions:
+ - If E is non-variadic, and there are no later variadic argument
+ expressions, then E can only match the i'th trailing parameter from the
+ end.
+ - Otherwise, E can match the i'th trailing parameter from the end, any
+ earlier trailing parameters, and the variadic parameter.
+- Otherwise, E can only match the variadic parameter.
+
+###### The type-checking algorithm
+
+In order to avoid type deduction that splits into multiple cases, we require
+that if the variadic parameter has a deduced type that is used in more than one
+place (as `Ts` is in the earlier example of this problem), all variadic
+arguments must have a known size (which means, as noted earlier, that we will
+expand them into a sequence of non-variadic arguments for type-checking
+purposes). This ensures that we can deduce the value of the array
+element-by-element in the cases where we will need to use that deduced value.
+
+> **Open question:** Is that restriction too strict? If so, it may be possible
+> to forbid only situations that would actually cause type deduction to split
+> into multiple cases. As well as being much less restrictive, that would avoid
+> the need to give special treatment to deduced arrays that are used only once.
+> It would still disallow cases like the call to `H` above, but that call seems
+> unnatural for reasons that seem closely related to the fact that its type
+> splits into cases.
+
+To avoid the potential for exponential blow-up, we will use a much more
+tractable conservative approximation of the ideal algorithm. We type-check each
+parameter as follows:
+
+- If the parameter is variadic, we check it against the concatenated types of
+ all argument expressions that it could potentially match. The rule stated
+ above ensures that this is safe: the concatenated type can only become
+ visible outside this local type-check if all variadic arguments have a known
+ size, in which case those concatenated types are known to be exactly
+ correct.
+- Otherwise:
+ - If there is only one argument it can match, which is also not variadic,
+ we type-check the argument against the parameter in the ordinary way.
+ - Otherwise:
+ - If the parameter has a non-deduced type, we check each potential
+ argument against that type.
+ - Otherwise, we check that all potential arguments have the same type,
+ and then check that type against the parameter.
+
+> **Open question:** When deducing a single type from a sequence of types, can
+> and should we relax the requirement that all types in the sequence are the
+> same? We can identify the common type of a pair of types using
+> `CommonTypeWith`, but it is not clear whether or how we can generalize that to
+> a sequence of types, since it might not be associative.
+
+We believe that if the code type checks successfully under this algorithm, any
+possible monomorphization can type check using the types deduced here, because
+the restrictions imposed here are a superset of the restrictions that any
+monomorphization needs to satisfy, and the information available to type
+deduction here is a subset of the information that would be available after
+monomorphization.
+
+##### Parameterized class type
 
 If the pattern and scrutinee types name the same parameterized class, the
 scrutinee type argument list is checked against the pattern type argument list.
 Otherwise, typechecking fails.
 
-_Identifier that names a deduced parameter_
+##### Identifier that names a deduced parameter
 
 FIXME
 
-_Name binding pattern:_
+##### Name binding pattern
 
 FIXME
 
-_`[:]` pattern:_
+##### `[:]` pattern
 
 FIXME