Uh oh!
There was an error while loading. Please reload this page.
Uniform Generics for Conditional Type Inference and Type Parameter Narrowing [Experiment] - #30284
Uniform Generics for Conditional Type Inference and Type Parameter Narrowing [Experiment]#30284jack-williams wants to merge 26 commits into
Conversation
Could you expand a bit on how the following example works with your implementation? functiontest1<T!extendsnumber|boolean>(b: T): T{if(typeofb==="boolean"){// unsafe, since T could be falsereturntrue;}returnb;}Does it reject this program? It should be rejected, since if it is accepted it results in unsoundness if constb=test1<false>(false);// b === true while it has the type false |
jack-williams
commented
Jun 7, 2019
The The callsite |
rubenpieters
commented
Jun 7, 2019
Yes, that makes sense. I was just curious to see how it worked.
Do you have an example in mind where it would be unsound? |
jack-williams
commented
Jun 7, 2019
It depends on your definition of unsound - it's unlikely that code today would go observably wrong. The technical issue is that it violates parametricity, and various nice things you could learn from reading a type no longer apply. For instance. declarefunctionswap<Textendstrue>(t: readonly[true,T]): readonly[T,true];One assertion that holds today might be that functionswap<Textendstrue>(t: readonly[true,T]): readonly[T,true]{if(t[1]===true){returnt;// as true <: T, and T <: true, therefore [true, T] <: [T, true]}return[t[1],t[0]];}I also generates issues if you ever add name subtyping, where you could have a named subtype like flow. opaquetype valid: true;// valid is a subtype of true, but true is not a subtype of validThe claim then that narrowing a generic |
sandersn
commented
May 24, 2022
This experiment is pretty old, so I'm going to close it to reduce the number of open PRs. |
typescript-bot
commented
May 24, 2022
This PR doesn't have any linked issues. Please open an issue that references this PR. From there we can discuss and prioritise. |
This PR is an experimental implementation of uniform generics: Generic types that can only be instantiated with types that behave uniformly under
typeof. This additional constraint makes it possible to apply new reasoning: something abit closer to dependent types.typeofapplies to all values of a uniform type. SeeequalityTransUniform.fn.The notation for uniform generic types is:
Type parameter
Tmust be instantiated with a type that behaves uniformly undertypeof, such asnumber,boolean,1 | 2 | 3, but notnumber | boolean,any, orunknown.This feature significantly benefits from #29317 and #29437.
The feature can also be extended to further uniformity constraints such as equality for enum members.
Examples (including ones from #22735 and #24929):