3 ms·
> a generic function that operates on two tuples of arbitrary tuple types and returns a tuple of a third tuple type whose shape is a simple concatenation of the
by corethree 3y ago
> a generic function that operates on two tuples of arbitrary tuple types and returns a tuple of a third tuple type whose shape is a simple concatenation of the shapes of the input tuples.
This isn't definable without dependent types or a concat operator at the type level. Dependent types aren't a thing we are talking about here and languages that support this feature are waaay out of scope.
You're basically asking for stuff like this:
func concat(a: Array[int; M], b Array[int; N]) -> Array[int; N + M]
or
func concat(a: Tuple[*args1], b Tuple[*args2]) -> Array[*(args + args)]
Which is bringing those programming terms up a level into types. This doesn't exist in the realm of programming we're talking about. Idris, Lean and Coq are more you're game here and those languages are clearly off topic.
>But... I don't want that, and that's not what this works on.
You want something well out of scope of this conversation and well out of scope of most practical programming languages. You still don't get what a tuple is. Nobody defines a Product type with an arbitrary amount of properties anymore then someone defines a struct with an arbitrary amount of properties anymore then they would do it for a tuple.
This is NOT the definition of a tuple. People are confusing the Tuple for some Immutable list.
>Python is very close to allowing that, which is very different than:
Python shouldn't allow this, neither should TS. If typescript allows it, it's probably some arbitrary shortcut feature. Dependent types at the type level supported in a very generic way is very very unlikely.
Like you people are trying to explain to me what a generic is while doing all kinds of programming operations on type level entities like concatenating them and combining shapes. Is the concat the only way to do it? What about an intersection? These operators only come into play with advanced theoretical langauges like Lean or Idris and it's very off topic.
- dragonwriter 3y ago> This isn't definable without dependent types or a concat operator at the type level. It takes relaxing one overeaeger limitation in Python's type annotation syntax, a limitation which is necessary in general to avoid ambiguity, but could be relaxed in specific, enumerable cases that do not produce ambiguity. > You're basically asking for stuff like this: I'm not sure exactly what your examples mean because I'm not sure exactly what syntax that is supposed to be, but in actual Python type annotations with a relaxation of the no multiple unpacking rule for variadic generics, what would be allowed is things like the example I posted upthread for tuples: def tconcat(t1: tuple[*Ts], t2: tuple[*Us]) -> tuple[*Ts, *Us]: ... or, for Arrays: def product(a1: Array[DType1, *Shape1], a2: Array[DType2, *Shape2]) -> Array[tuple[DType1, DType2], *Shape1, *Shape2]: ... concat for arrays would take dependent types, but that's not what is being discussed. > This doesn't exist in the realm of programming we're talking about. All the concepts necessary for what the upthread poster noted TypeScript already has and was superior to Python because Python lacks, and which I pointed out Python is relaxing one limitation short of also having, already exist in Python since Python 3.11, there is just a syntactic limitation on using the necessary combination to avoid ambiguities (which occur in different circumstances). And, of course, all the necessary concepts also exist in TypeScript. And those two languages are "the realm of programming we're talking about". > You want something well out of scope of this conversation No, literally, I'm discussing the thing that is the advantage of TypeScript's type system over Python's that has been the subject of this conversation, which is not, ipso facto, well out of the scope of the conversation. > and well out of scope of most practical programming languages. It exists in TypeScript which is widely used, whether or not you thin it is "practical". > These operators only come into play with advanced theoretical languages like Lean or Idris and it's very off topic. The discussion was about a comparison between TypeScript's type system (which supports this) and Python's (which does not quite, though it has all the pieces with a syntactic restriction that prevents certain useful combinations.) These are not "advanced theoretical languages", and the discussion you jumped into is not at all off-topic (certainly not of itself, despite your jumping in to derail it, and not of the broader discussion of Python and scale because JS/TS is a similar industrially popular language ecosystem to Python with a dynamically typed base and optional statically type-checked layer.
- corethree 3y agoI see. So ts arbitrarily supports concatenation of generic parameters via unrolling. All right. I can admit TS is superior from this angle because of that arbitrary support. And I can admit that the arbitrary support follows from the way both languages use unrolling syntax.