Type merging improvement => x & void = x since y & never = never, instead of u & void = illogical constraint

[wesleyolis]

Hi Guys,

I would just like to challenge some of the types engine logic here for the greater good of patterns.
I would like to recommend a change to the logic of how intersections are resolved with regards to void and never, which I see as reciprocal operations.
I would like to suggest think of/working with sets theory, then the type keywords void and never have specially meaning. cumulative, associative, distributive laws come to mind from probability and stats.

This would improve build up of types with recursion, were a default initial condition can be supplied.
Similar to SQL tricks of "1 == 1" + $WereConditional

The following similar explanation I have offered for SQL language comes to mind that I have previously given. Extract

Select rowid From BackColors where col1 not in (Select col_in From table_in where col_in is not null)

Very import in the sub-query the SQL statement in bold, italics, red is the part where the column on which the lookup is to be done, must exclude nulls. Reason a NULL will match anything, thus it will return no records to highlight. 

If you imagine null as a set and null means the set is empty (nothing) then what is the not or opposite NULL then? Not of empty is full and the not of nothing is everything. This is the reason why you have to exclude nulls from the subquery as you noting the result which in tern then is everything.

Current Typescript Behavior:

void type identifier

type inter = (number | string) & void;

// impossible logical condition to meet.
const example : inter = ... ;// type must be of form number & void | (string & void), which is an impossible condition to meet.

never type identifier

type nothingEmpty = (number | string ) & never; // = never

const example : nothingEmpty = ...; //type must be of form never, removes item or type.

Suggested Behaviour, perceived improved behaviour

void type identifier

type inter = (number | string) & void;

const example : inter= 34; // Ok, type must be of form number | string
const example : inter= "testst"; // OK, type must be of form number | string

never type identifier

type nothingEmpty = (number | string ) & never; // = never

const example : nothingEmpty = ...; //type must be of form never, removes item or type.

One may also want to introduce boundaries for type simplification/resolution such as intersections and unions,
which will communicate to the compiler, were it should no longer simplify void and never conditions.
Think of using some form of brackets []. This cases below are not practical, however, example of the pattens.

[number & void] & string = number & string

or

 [number & never] & string = string

Looking forward to your feedback.

[crdrost]

Hi, WesleyOlis!

I can tell you that you need to update your docs ;-)

Your example is that this will implicitly accidentally select nothing:

select * from myTable where val not in (select 1 union select null)

That is true. But your explanation of why this implicitly selects nothing is problematic.

By describing this as the problem of "a null will match anything" you are implicitly suggesting that this will implicitly select everything:

select * from myTable where val in (select 1 union select null)

...and that is not actually true. (This is equivalent to where val = 1, not where 1 = 1.)

Roughly speaking, never is meant to be a "bottom type" that contains no subtypes and no values, and is a subtype of all other types. It is dual to the "top type" of any which has no supertypes and all values, and is a supertype of all other types. The exact problem of how to mentally model never is more or less being tracked at #13803, and note that your problem directly runs into some of those issues. (The problem in rough outline is that there is usually a bottom value corresponding to infinite loops and exceptions, but here we are talking about a bottom type corresponding to infinite loops and exceptions, and shouldn't that type only contain bottom values? See also the comments to my issue #23971 which were at least enlightening for me.)

Using void to mean any is problematic because in JavaScript void functions actually return undefined, which is the unit type in JavaScript (it has exactly one inhabitant). So if you were to intersect void = {undefined} with the set int = {0, 1, -1, 2, -2, 3, -3, ...} the proper set-intersection is never = {} because undefined is a first-class JavaScript value which happens to not be in that set.

With that said I think there is a bug we could open here, which is that x & any should presumably be x (right now it appears to resolve to any) to properly resolve along subtype lines, just like how x & never correctly resolves to never.

[RyanCavanaugh]

I don't understand what problem the OP solves. Some motivating scenarios would be really useful.

in JavaScript void functions actually return undefined

I just have to correct this wherever I see it - a void-returning function in TypeScript can return anything because it might be an alias to another function:

const f: () => void = () => 42; // Legal
console.log(f() === undefined); // False

[crdrost]

Oh, that's interesting and I definitely did not realize that.

I would love if at some point we could publish a sort of formal semantics for this thing, as I would not have expected something like "void is secretly an any which does not like return statements."

[wesleyolis]

Well if I stick to the topic!

There are three perspectives(Dimensions) of analysis when dealing with types, one is based on looking at things from the perspective of sets and what they can represent; the other is from their implicit compound operator function that is perform when resolving types, with an intersections and unions when used in conjunction with a type; and type assignment

A, Type assignment, which types in the type set of identifies in B can be assigned to one another.

Each type indentifies, defines for each of the following, which types can be assigned to it.
void*, boolean, number, string, object, array, undefined, null, any*, never*

• never, doesn't allow anything to be assigned to it.
• void, allows anything to be assigned to it, but morphs into the first assigned type. ( not 100% sure here..)
• any, allows anything from the above set to be assigned to it, and will never morf.

B, Sets perspective:

If we look at types that can be used in a set then I see the following set of types being used, were void and any are special
TypeIdentifiers=void*, boolean, number, string, object, array, undefined, null, any*, never*
Types = boolean, number, string, object, array, undefined, null, (never)**

• void, is a key word that donates empty set of Types,
• any is a key word that donates a full set of Types, it is all so special as single key word that say it will accept any other type, always and will never mutate into that type.
• never is kind of special and compound operator with union, intersection of any and a presidency of operators would need to be determined.

  type AnyType = any & string; // becomes, any

C, Compound Operator perspective, when encounter with an intersected or union in type definition.

• never can be used as if it were a type, but it functions as an operator in type resolution with intersection, union.
• void, proposal, can be used as a type, but it would also now function as an operator such as in type resolution, when encountered with intersection and union.
• any, can be used as if it were a type, but it functions as an operator in type resolution with intersection, union.

any, improvement for autosuggestion, auto complete with typings

The AST Backing data structure for any, should have a field, that contains an AST of the types it consumes as an operator, should preserve the relationships. This will allow autosuggest and complete, to interrogate and any data structure and provide more comprehensive types and structure as suggestions prefix with a *{a:number, b: string} | *number | *SomeInterface as as apposed to nothing.
The prefixed start would indicate this is a hinted possibility and can actually be anything its not a concert constraint.
Autosuggest and complete, should also attempt to try pass an in complete context based AST, were their is a hard type available for assignment, and then attempt to find the closest union matching the partially passed assignment context, so that the list can be narrowed, to the relevant properties. Think of kind, when using algebraic stuff, once [kind]:"identifiier" is matched. Joi.Alternatives.try semantics, is what one would be looking for here. Other Alternatives can be on the end of the list, and prefixed with a #.

From operator perspective, void and never do the opersite things.

• Never, basically aggressively nukes types, that are intersected or union with it.
• void, basically would gracefully morph and become the type that it is union ed or intersected with it
  any, basically aggressively consumes types and replace them with its self, its definition is never morphed.

With void and never defined with these augmented operator resolution properties for type resolution and merging. On can very easily now achieve most patterns with sets, unions, intersections, when doing recursive type processing.

never, void are consider operators, when used with union and intersection as they modify the behaviours of union and intersection, when encounter with a non-operator type set.
boolean, undefined, null, string, number, object, array, interface..

The best is when you are required to seed any problem, then you seed it with void, when void is intersected with or union with another type it nukes(morphs) it self, leaving just the type is was merged with.
Their is no breaking behaviour to existing void, it still can return undefined, if void has not' been merge
via union or intersection operator, something else, in which just nuke its self from the type definition.

Example, programming with a type system veneer layer, to generate type definitions..

This is really just the basic idea..

interface base
{
 type: void; // Seed value...., which will morph into the first type that is unioned with it.
 tackOnTypes() : type : string
}

interface specialisation extends base
{
tackOnArray(value : T) : type : T[]
}

type extractRecusive<T> = ifHasKey<T,'type',extractRecusive<T['type']>, T>

const instance = {....} // which is composed from many specialised instance above.

type myType = extractRecusive<typeof instance>();

Here is a whole bunch hacking around with types and other attempts, before we found very simple way, that can be simplified every more if void, is given operator capabilities when operated on by intersection and unions, when resolving types and merging types.

https://github.com/wesleyolis/tsTypesFromASchemaImplemention

https://github.com/wesleyolis/tsTypesFromASchemaImplemention/blob/master/src/schema-validation/internal/type-helpers.ts

You probably now, mabye get a bit more understanding for the context for were we were going with the following:
#24517

I can say that our new approach to extracting types by programming in the type system veneer layer with types, is work out reasonable well for us. Our simple Joi Superset Extension framework as we flesh and resolve issues as we build it out, gives us primitive and structured typescript types, from a single simple joi schema instance implementation.. No pre-processors or generators needed.. :-) All we required to do.

type myType = extractRecusive<typeof schemaInstance>()
const settings : myType = {} // bobs your uncle.

@RyanCavanaugh 
The behaviour you define, with regards to function return type, is the behaviour you like to have happen everywhere, with void, as I original describe in my examples.

[crdrost]

I think this proposal is basically that the set operations of TypeScript should form two monoids:

Type union is already a monoid with never as the identity element. The idea right now is that "x is a valid element of A | B if x is a valid element of A or x is a valid element of B (or both)", and never does not contain any valid elements so never | A always reduces to A. The proposal is that this identity element should instead be void and never should be a zero element, so that never | A = never. I personally think this part is indefensible.

Type intersection is a semigroup with never as a zero element. In the most common case, where one is intersecting objects, object is an identity element, but this is not fully general. The idea is "x is a valid element of A & B if x is both a valid element of A and x is a valid element of B". The proposal is that this should admit an identity element void and never should continue being its zero element.

I think the latter is weakly defensible on mathematical grounds, now that I know that void is secretly an any type that only enforces special semantics around return statements. I think a stronger statement is that any should be the fully general identity element. This requires that any & x which right now in my VS code (TS 2.9.1) usually reduces to any should instead reduce to x. (Right now any is a pseudo-zero, only distinguishable from the real zero element by seeing that any & never = never & any = never. This does not seem very useful.)

With that modification to any under &, the TypeScript type system has a strong basis in set theory (types can be viewed as sets of members where union and intersection are set operations on them) and in fact forms an idempotent commutative semiring, with addition equal to | and multiplication equal to & and zero equal to never and one equal to any. (This probably comes from the fact that the above is defining a distributive lattice?)

[wesleyolis]

The have one other reason, that void should have morphing behaviour like in the return statement indicated above would be for type checking reasons.

Currently the Any compound operator, consumes all types and basically results in typing any further with any pointless!! As Any represents a fullset of possible type assignments, which means anything can happen. Basically is better to use @ts-ignore than an Any type. [A // @ts-ignore comment suppresses all errors that originate on the following line. It is recommended practice to have the remainder of the comment following @ts-ignore explain which error is being suppressed.]

If the Void Compound operator, morphs into the first type is consumes(Basically what current happens for return type function statement assignment), then the type checking engine will still be able to perform type checking downstream, which will results in more of the program being being type checked.

I like the idea that by upgrading void, instead changing the behaviour of any, provides a complete set or all possibilities of compound operator behaviour with their reciprocals (void/any), were never is really just their for compound operator behaviour.
The one thing for me is that the alias, void donates and empty set of types, and any donates a full set of types, if this was looked at from sets perspective.

That or we have 3 type key words here, were only two of them are required.

I am now starting to consider, what would be lost if Any definition is changed, to be the void behaviour I describe, as well as should never and void not be the same thing?? In the bigger picture of existing code and backwards compatibility what do we end up breaking and improving then... Because currently for void Compound operator results in illogical constraint which can't meet piratically, so we wouldn't be breaking anything existing.

[wesleyolis]

One advantage of Any type have this compound operator behavior of morphing, is that it would allow
the typing engine, to be able to do further type checking, were a function or assignment is many to and any type, which can then further restrict it for more specialized evaluation... Trying to determine the cons to the two main competing narratives presented here at the moment

This is probably not a bad thing to work against: https://github.com/Microsoft/TypeScript/blob/master/doc/spec.md#3

[wesleyolis]

Ran into a couple of other issues over past couple days and weekend, Sent me round in couple circles, reporting couple more non-bugs, then also then vetted a couple other things with my colleague in this area were I was wrong, but subtitle improvement can be made why went down that rabbit hole, with what I was wanting. To nights feature request and example, to clear that misconception up.

We have also been debating or opposing interpretation of Any, were it should be morphing or not.
Were I am for void morphing, from the start.

All of this has lead me to have the following understanding of the Any type, which hopefully should help in shorting out why, void should morph and any can't and should never morph.

Any, means we are not prepared to make an assumption about the type, we not for any reasons, prepared to further constrain the type. We can only know the constrained type for absolute certainty after an Any type has been validated at run time to be of a certain type form against which, we were validating, it can then after validation be assumed the type against which we have validated.

If you reading a file from disk, you are assuming it has a certain type and structure, until its has been validate to have that type, form or structure, one is making an assumption. If you wrote the file and read it again, with out validating it, you are making the assumption it is of certain form and are hoping it has been tampered with in between.

Everything that is not compiled in the same compiler instance, can have the potentially to be an assumption of the type you are making. any 3 party, could have cast the type. Any internal cast also mean you making an educated guess and assumption.

Therefore, it is with this enlightenment that Any must always consume, nuke other types, when acting as an operator with Union or Intersection, because an assumption plus anything concrete, is still yet just that an assumption, with a shadow, probability of being right.

The type checking engine, internally, could potentially softly attempt to narrow the AnyType, with a shadow type, to provide higher level of type checking probability for any usage internally, and emit helpfull soft warnings, but still must have back off, that were narrowing has happen, can become AnyType again, if it was wrong up till that point. Think creating a new context environment for compiling that block of code, were AnyType has been narrow, if wrong, emits warning, and changes the type back to an AnyType and then re-compiles that section with reverted context of AnyType, as an example.

[crdrost]

You are overthinking this. (x: any) => Foo is a statement that I will take any sort of x and give you a Foo. (x: Bar & Baz) => Foo is a statement that I will take any x which can be described both as a Bar and as a Baz and I will return to you a Foo. It gives you an intersection of two types. From those two statements it follows that if Baz = any then we will find Bar & Baz = Bar: "anything which can be described both as a Bar and as anything" reduces directly to "anything which can be described as a Bar."

So for example if Bar is {toJSON: () => string) then every other instance of Bar & Baz for every other Baz has a toJSON property which takes nothing and returns a string. It makes no sense (more precisely, & becomes highly cognitively complex where it could have been much simpler) if one's ability to infer the existence of this property suddenly fails in the special case where Baz = any.

[wesleyolis]

I hope this gives you some context on the bigger picture that we are looking at, were we current see things are going.
explicit type assignment modifier keyword for function/constructor parameters typically

[wesleyolis]

Here are a couple more reason and examples of the patterns that can be formed, which now having problems with, when it comes to extends and structural typing, in which having a seed void morphing operator, would definitely simplify things as a result in perfectly recursive and simplified extraction methods, with less exceptions, because one can't initialization a property in an interface with any or void, right now, as pattern nukes all recursive intersection.

Typically we are mainly targeting methods and not properties, which means
of class interfaces, are all identical. typically it would be good to have a nominal extends, with introduction of nominal typing.

interface InterA
{
    MethodA() : this & {someTypeMinipulations};
    MethodB() : void;
}


interface InterB
{
    MethodA() : someCastingMinipulation;
    MethodB() : void;
}


interface InterC
{
    MethodA() : void;
    MethodB() : void;
}

type Structure = 
{
    [index: string] : InterA | InterB | InterC
}

Basically the extract method which uses the extends key word, is absolutely pointless here,
because it is structural typing and each class is required to have a dummy member.
Typically we have had actually members, which used for recursion, however, they are then required to be seeded, if you want to use it, and seeding with any, means it will always be any.
Here as per this posts request to allow void to be a value, that can morph into the first type it is intersected with or union, would clearly have a benefit, as one would only need a single variable to be added, which also be used in type manipulation. It also simplifies things alot more, because after an extends question then type if true is constrained to that type, which means one knows the member exists.

type Extract<T extends Structure> =
{
    [K in keyof T] : 
    T[K] extends InterA ? number :
    T[K] extends InterB ? boolean :
    T[K] extends InterB ? string :
    'Mistake' & T[K]
}

void as a type that can morph, which then also allows, guaranteed perfectly recursive methods to be written with out having to worry about the default initialised cases of the member variables of having to check were this class is of a certain type.
CommonKind identifier, will also not work, because the key doesn't make it structurally unique, so that is out of the question.

interface InterA
{
    MethodA() : void;
    MethodB() : void;

    commonKind : 'InterA'
}


interface InterB
{
    MethodA() : void;
    MethodB() : void;

    commonKind : 'InterB'
}


interface InterC
{
    MethodA() : void;
    MethodB() : void;

    commonKind : 'InterC'
}

At the moment we really on the fact that a method must be called, to assign the first type to __interA.
which means, alot more complicated processing is required for extraction, as the pattern is not perfectly recursive.

interface InterA
{
    MethodA() : void;
    MethodB() : void;

    __interA : void
}


interface InterB
{
    MethodA() : void;
    MethodB() : void;

    __interB : void
}


interface InterC
{
    MethodA() : void;
    MethodB() : void;

    __interC : void
}

type Structure = 
{
    [index: string] : InterA | InterB | InterC
}


// Both are now equivalent.
type Extract<T extends Structure> =
{
    [K in keyof T] : 
    T[K] extends InterA ? number :
    T[K] extends InterB ? boolean :
    T[K] extends InterB ? string :
    'Mistake' & T[K]
}

type Extract<T extends Structure> =
{
    [K in keyof T] : 
    T[K] extends { __interA : any } ? number :
    T[K] extends { __interB : any } ? boolean :
    T[K] extends { __interC : any } ? string :
    'Mistake' & T[K]
}

However this way below more explicitly in communicating what asking, that a certain property existing,
because interface are structural, it looks advertising use interface name, doesn't mean much here.
May it would be good to read for those coming from nominal typing back ground to read, 'structural extends' or 'nominal extends', say as to not make a few times.. when working mainly with interfaces were their typically no members or properties and wanting to do type extraction. It may actually be of benefit here to differentiate the two because unless one is prepare to wrap every single class in a wrapper, one is not able to use decission logic to enhance other models classes simple.
Think of wanting to write a method to extra the AttributesValues = Value1 | Value2 | Value3 | Value4
from amazon type definitions. so that they can be suggested as keys.
RecordOptional<Attributes, string>, but to do this at a global level one wants to write a method along the lines of this, relative give take extends keyword.

type EnhanceAmazonType<T> = {
    [K in keyof T] : T[K] extends {AttributesValues: any, Value: string}
    ? RecordOptional<T[K]['AttributesValues'], string> : extends {} ? 
    EnhanceAmazonType<T[K]> : T[K]

}

Target specific class interface name with a nominal type guarantee, that their be no conflict, in structurally writing an incorrect classes type for 3rd party modules, that one would like to recursively re-write definitions for.

type EnhanceAmazonType<T> = {
    [K in keyof T] : T[K] nominally extends ServerType
    ? RecordOptional<T[K]['AttributesValues'], string> : extends {} ?
    EnhanceAmazonType<T{K} : T[K]
}

[wesleyolis]

this could be quite similar to unknown propsal. Mabye need to compare differences pros and cons.
#24439

[wesleyolis]

It has also come to light that any from a set perspectives, should NOT include null and undefined, because those keywords are special and used to differential lack key of presents (undefined) and uninitialise contents nulls state. Especially from a patterns perspective when programming with and Any (undefined, null, Any), to be backwards compatible, explicit keyword may need to be used.

#25053

[RyanCavanaugh]

There's a lot of text here and even more confusion about what void means. I don't see any actionable change to be made; the intersection and union rules are well-established based on properties we want them to have.