Discussion: Anticipate a wider set of types for future static typecheckers

[dpchamps]

First off, thanks all for putting this proposal together, very exciting!

Introducing a specification for type annotations into ECMA is a super interesting idea. I think I'm most selfishly interested in the notion that future static typecheckers might target a single specification, or implement a typesystem against ecmascript without needing to compile.

Having looked through the issues, I might coin an unofficial mantra:

The specification is type-system agnostic.

With that in mind, there are a couple of interesting types that this proposal may want to anticipate in the grammar itself to be permissive of future implementations to existing and new type systems.

Note: In demonstrating types I'll give some examples, but this is demonstration only. It's not my intent to propose any syntax here, instead just start the discussion for what that syntax might be should the community/champions be open to the idea

Refinement Types

• Refinement Types (pdf link)
• ADVANCED LOGICAL TYPE SYSTEMS FOR UNTYPED LANGUAGES (pdf link)

One liner summary: a type that refines a broader type T based on some predicate P, e.g.

pseudo code might be:

declare function divide<T extends number where GreaterThan<T, 0> >(n: number, x: T): number;

Dependent Types

• Dependent Types for JavaScript (pdf link)

Similar to, but different from refinement types. Hand-wavy summary: like refinement types, but with values as types.

pseudo code might look something like:

declare function concat<T extends unknown[], U extends unknown>(arr1: T, arr2: U): 
[...T, ...U] extends [...infer N]
where LengthOf<N> == LengthOf<T> + LengthOf<U>

It's not difficult to imagine that we'll see some mainstream type-system adjacent to the JS ecosystem that implements these types. There has of course been some academic exploration already. It would seem to fit into the already proposed ConditionalType production, but I think it would need a bit more syntax to be supported correctly.

Higher Kinded Types

Great discussion in TS land: https://github.com/Microsoft/TypeScript/issues/1213#issue-49436743

The grammar as is stands may be permissive enough to support implementations of HKTs, but I think it's worth including here to see if anyone feels strongly about it.

---

These are the types that I'm most interested in. I know the field of type theory is wide. There are others -- linear types stand out to me. But I haven't thought about how linear types might be useful enough to propose them for consideration here.

Thanks all!

[acutmore]

Hi @dpchamps!

The current tentative grammar (subject to change) may already be relaxed enough to allow the ideas you are envisioning.

For example, generics are defined as AngleBracketedTokens which is: < TokenBody >. So function divide<T extends number where GreaterThan<T, 0> >(): number {}; would already be a permissible type comment.

The core constraint is currently that the type comment has balanced brackets (< ... >, ( ...), { ... }, [ ... ]). So I think this might prevent a type system being able to use > as syntactic sugar for a greater than type constraint for example.

[dpchamps]

@acutmore thanks for the prompt reply!

I agree, the grammar as it stands is definitely relaxed enough to support something like GreaterThan<T, 0>.

However, it's the refinement or dependent token that concerns me. (in my examples I've used where)

Looking at the grammar, the following productions stand out to me:

TypeDeclaration :
  type BindingIdentifier TypeParametersopt = Type

Type :
  ConditionalType
  NonConditionalType

ConditionalType :
  NonConditionalType [no LineTerminator here] extends NonConditionalType ? Type : Type

I believe the grammar as it stands would not be able to support an additional refinement/dependent clause without semantically overloading the existing extends NonConditionalType .

I feel like we'd need perhaps a third type, e.g.

Type :
  ConditionalType
  NonConditionalType
  RefinementType

Or perhaps a "more rich" definition of ConditionalType -- edit: or now that I think more about it, perhaps this would need to be part of NonConditionalType 🤔

What do you think?

[acutmore]

The current 'get out of jail free card' in these cases is wrapping the whole thing in brackets. e.g:

(Array<T|U> extends [...infer N] where LengthOf<N> == LengthOf<T> + LengthOf<U>)

Do you think this is a sufficient solution to not precluding the unknown set of future possible type syntax?

[dpchamps]

Hmm interesting!

Something like that sounds promising.

Help me out: I just went back to the proposed grammar and studied it a little more closely, I don't quite see where this behavior defined. Is the general idea to elide / accept anything in place of the Type production that appears between bracketed tokens? s.t.

type T = (anything at all goes here)
declare const x: (anything at all goes here)

edit, ah I see now.. This is the proposed sln outlined here?

[simonbuchan]

I'm actually working on implementing a grammar for this proposal at the moment. It's surprisingly hard to accept completely arbitrary grammar in brackets, see #116.

In any case, I think the value for accepting a wide enough grammar that the hammer of bracketing isn't needed for the large majority of cases even of speculative type syntax is high enough that it's worth examining the option.

Here's some examples of what I would like to see be syntactically possible with my grammar, if nothing else:

// declarations
type User = frozen { own name: ?string! };
type frozen User { own name: ?string! };
type User(string);
type UserName = /^(de |mac )?[A-Z]/ - "Admininstrator";
type Id[ "A" - "Z" ("A" - "Z" | "0" - "9")* ];
type Grammar { "let" Id "=" (Id / number) ";" }
interface Foo = OtherInterface;

// annotations
let rocketEngines: number < 5 = 123; // type error: 123 is not less than 5
let distance: number.<unit = miles> = 123;
distance = getDistanceToSun(); // type error: unit = km is not compatible with unit = miles 

[dpchamps]

@acutmore

Do you think this is a sufficient solution to not precluding the unknown set of future possible type syntax?

Overall, yes-- I think it's a sufficient solution. However, I wouldn't call it ideal. What I'm trying to capture with this discussion I think is expressed a little more clearly between @ahejlsberg and myself in this exchange here: https://github.com/giltayar/proposal-types-as-comments/issues/80#issuecomment-1068480948

I think a majority of people will agree that requiring types to be wrapped in parens is inconvenient.

What I mean to say is, Should we consider a more permissive grammar that does not require a different syntax when departing from the established grammars of current type systems.

@simonbuchan

In any case, I think the value for accepting a wide enough grammar that the hammer of bracketing isn't needed for the large majority of cases even of speculative type syntax is high enough that it's worth examining the option.

For sure, 💯 agreed.

In my mind there seem to be roughly three "reasonable" approaches here:

1. Accept the current typescript-light grammar, ensure that most of other established type systems are moderately supported. Use the "escape-hatch" bracket syntax for anything else.
2. Design a grammar that is wide enough for type-systems to evolve outside of the current known set of options.
3. Design a grammar that is permissive (or anticipates) a known set of types that do not exist within status-quo javascript type systems.

To me, the ideal solution is obviously 2. If possible, it's the best of all worlds. If it's not possible, we may still want to entertain the idea that the type system has anticipated the existence of types that may require additional grammar without the need for this bracketed escape hatch.

[simonbuchan]

Here are some exciting problems to think about in this space, if you're curious:

• Automatic Semicolon Insertion in general? E.g. Should the two snippets type Foo = maybe_a_keyword function bar() be parsed differently when they have a newline between them?
• How do you support introducing new type keywords as either unary modifiers or binary operations, which is a popular type system addition? E.g. infer, readonly, opaque? Just technically, specifying how to parse these (which the lexer currently treats like identifiers) while still being able to parse identifiers as type references is a bit tricky. How about when they are re-using existing keywords? extends and function are very plausible for use in type syntax, afterall.
• How does a type system introduce new operators?
• How do you treat the division vs regexp lexical ambiguity in general? You essentially need to define at least enough to distinguish between "operator like" and "expression like" positions, which is especially hard when dealing with the above!

[DanielRosenwasser]

FWIW we're investigating a satisfies binary expression operator for TypeScript 4.7 as well...