Type predicate expressions and 'this' type assertions

The type system currently allows to specify basic type constraints (or 'assertions') on polymorphic types, for example:

function example<T extends Array<any>>(a: T) {};

However, currently there is no elegant syntax for types to declare constraints on themselves. Here's a real world example where I needed something like this:

I have a class containing several methods:

class MyClass {
	read(filename: string, byteCount: number): string {
		// ...
	}

	write(filename: string, text: string): void {
		// ...
	}

	delete(filename: string): void {
		// ...
	}
}

and I want to write a known (i.e. monomorphic) type that is constrained to exactly match the keys of MyClass (the property types don't matter for this example, so I annotated them with { ... }, for simplicity, also note that MyType is intended to be user-customizable and cannot be deterministically generated using a mapped type):

type MyType = {
	read: { ... };
	write: { ... };
	delete: { ... };
}

The best hack/workaround I found so far was to declare additional dummy types, that would fail if MyType doesn't satisfy the expected constraint:

type Extends<T1 extends T2, T2> = boolean; // The 'boolean' doesn't really have any meaning here.
					// It can technically be any type.
					// I only used it because I needed to fill out some sort of
					// type association to satisfy the compiler.

// These types are never actually used. They are only here to force the program not to type-check 
// if their supplied arguments don't satisfy the constraints for the Extends<..> type parameters:
type DummyAssertionType1 = Extends<keyof MyType, keyof MyClass>;
type DummyAssertionType2 = Extends<keyof MyClass, keyof MyType>;

The hack does seems to work so far, and has proven useful in practice, so by itself that's a significant improvement over having nothing at all. However, it is not very elegant or readable and violates type 'encapsulation'. It would be cool if I could instead write something like:

type SameKeys<T1, T2> = (keyof T1 extends keyof T2) && (keyof T2 extends keyof T1);

type MyType where SameKeys<this, MyClass> = {
	read: { ... };
	write: { ... };
	delete: { ... };
}

I'll try to break down what is happening here:

The SameKeys type contains a type expression that evaluates to either the true or false boolean literal types. Given P1, P2 are valid type predicate expressions (e.g. T extends U) then P1 && P2, P1 || P2 !P1 are also type predicate expressions etc.
The where keyword simply implies that the following type or type expression must evaluate to a boolean literal type and in particular to true for the constrained type to be valid.

[Edit: removed some confusing examples, see the next comment]

The concept can also be used with interfaces, or even classes:

interface MyInterface<T, U> where SomeComplexPredicate<this, T, U> { 
  // ...
}

class MyClass<T, U> where SomeComplexPredicate<this, T, U> { 
  //...
}

Edit: changed the suggested satisfies keyword to where as I believe it gives slightly better readability.

I think some of my examples were a little bit misleading (edit: they have now been removed from the original comment) and I need to try to clarify what exactly is and is not in the scope of this idea (perhaps for myself as well):

This concept is about:

Providing a way for type, interface or class declarations to provide a set of assertions on themselves, in the same sense that contracts assert over values. This is very similar in spirit to implements but allows for more expressive grammar in the form of propositional logic statements and clauses over relations between types. In a rough sense, it allows interfaces, types, or classes to "implement" other interfaces, types, or class "shapes", or more complex mappings of them, and test for multiple combinations of these propositions, joined by logical connectives.

This concept is not about:

Providing an alternative way to declare constraints on type parameters: I have considered what would be the implications of trying to achieve that using this powerful grammar and came to the conclusion that the level of potential complexity would not justify the value it gives.

I'll try to create a set of limiting rules to try to "reduce" the power (and also the potential traps) of these clauses.

One thing that can be done is introduce rules that limit what can participate in individual propositions. The first rule might be that every proposition must include the this type (or a name that corresponds the current type) at some form:

These are ok:

interface MyInterface<T, U> 
    where (this extends { [key: string]: [T, U] }) || 
          ({ [key: string]: { a: T, b: U } } extends this) {
   // ...
}

interface MyInterface<T, U>
    where keyof this extends "a" | "b" | "c" {
   // ...
}

interface MyInterface<T, U>
    where this["a"] extends T[] && this["b"] extends { x: U } {
   // ...
}

These are not:

interface MyInterface<T, U>
    where T extends Array<any> {
    // ....
}

interface MyInterface<T, U> 
    where Array<T> extends Array<number> {
    // ....
}

interface MyInterface<T, U> 
    where T extends Array<U> {
    // ....
}

The reason I'm trying to disallow these patterns is because I'm considering what would happen if the type arguments given to T and U are themselves polymorphic:

interface AnotherInterface<A, B> where (...) {
    a: MyInterface<A, B>;
}

If the where assertion was allowed to constrain its type parameters directly with this powerful grammar, it would mean that the compiler would need to "prove" that the type parameters A and B satisfy a set of complicated constraints based on a whole different set of complicated constraints as premises, and that may be very difficult to do, or even eventually require the equivalent of a theorem prover.

Instead, I'm trying to figure out a way to limit the power of these propositions to avoid trying to directly or indirectly enforce particular types over their parameters.

So the following where assertion should probably fail as well:

interface MyInterface<T> 
    where this extends { a: number } {
    a: T;
}

Because it indirectly "forces" a type over an unknown polymorphic type.

But this would pass:

interface MyInterface<T extends number> 
    where this extends { a: number } {
    a: T;
}

I think the aim and direction here should become clearer now. I hope this helps..

Another way to express this is that the where assertion I'm describing here "validates" the final, resulting type, but does not participate in or influence its definition. It is not the same semantics as where in C# , which is used for type parameter constraints.

Maybe the keyword could be improved. Initially I considered satisfies, which I thought didn't read very well, then where. I'm considering assert but it could be a bit confusing as most people associate it with assertions over values, not types. I don't want to use keywords that may be useful for future features like code contracts (ensure, validate, expect etc.).

Edit: How about check?

interface MyInterface<T, U> 
    check (this extends { [key: string]: [T, U] }) || 
          ({ [key: string]: { a: T, b: U } } extends this) {
   // ...
}

type MyType<T, U> check SomePredicate<this, T, U> = {
   // ...
}

I have intentionally generalized the ideas here as I felt doing that would be interesting and academically important. I wasn't necessary suggesting for it to be implemented the way it is presented here.

I'm closing this for now to prevent it from getting "tanked" forever by the TS team. Maybe I'll try to suggest something similar in the future in a more limited form.

Navigation Menu

Repository navigation

Type predicate expressions and 'this' type assertions #12942

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Type predicate expressions and 'this' type assertions #12942

Description

Activity

rotemdan commented on Dec 16, 2016

rotemdan commented on Dec 16, 2016

rotemdan commented on Jan 13, 2017

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions