[feature request] switch and pattern match in type position

[HerringtonDarkholme]

Hi, thanks for building Civet. The if/else addition to the conditional type greatly increases the language expressiveness.
Since Civet also supports runtime switch and pattern matching, here is a suggestion for adding them to type level. The inspiration also comes from Scala's match type.
This is a fan post so feel free to close.

Motivating Example

It is common to check the type of one type parameter several times in a type alias. While Civet's if/else extension helps reduce long ternary type's verbosity, it can be further simplified by switch.

Consider this type, from Civet's playground

type RSliceReturn<T> = T extends string
  ? string
  : T extends RSliceable<infer R>
    ? R
    : never 

can be simplified using switch with pattern matching

type RSliceReturn<T> = switch T 
  string then string
  RSliceable<infer R> then R

More Examples and Behaviors

Basic Behavior

Runtime switch expression can be compiled down to a series of if conditionals, so is type level switch.

type isFalsy<T> = switch T
  "" 
     true
  0 
     true
  false
     true
  else 
    false

is equivalent to this Civet

type isFalsy<T> = 
  if T < ""
    true
  else if T < 0
    true
  else if T < false
    true
  else 
    false

Using literal, tuple, object

The example above has already shown switching on literal. We can also support other types.

type Example = switch T
  "true", "false" then boolean
  123, 456 then number
  []  then 'empty array'
  {a: number, b: string} then 'object'
  [a, b, ...c] then Array<T>

Note the last type [a, b, ...c] is equivalent to TypeScript's [a, b, ...c]. Type position pattern match is different from value position pattern match.

Using type name and bind

Since using existing type name is more common in conditional type, it is better to reference outer scope variable as default. (this is different from switch expression in value position)

Example ::= switch A
  Ref<T> then T
  Ref<T>[] then T[]

is equivalent to

type Example = 
  A extends Ref<T>
    ? T
    : A extends Ref<T>[]
       ? T[]
      : never

It is possible to create a new binding in type level pattern matching using ^

Example2<T> ::= switch T
  Ref<R^> then R

is equivalent to

type Example2<T> = T extends Ref<infer R> ? R : never

This is similar to the runtime value switch pattern matching.

Binding can also be used with object restructuring and name^bound can also be used as infer name extends bound syntax in TypeScript.

type Example3 = switch T
  { a: A^, b: B^} then [A, B]
  {  foo^, bar^ } then [foo, bar] 
  { bound^number} then bound

compiles to

type Example3 = 
  T extends {a: infer A, b: infer B} ? [A, B] : 
  T extends {foo: infer foo, bar: infer bar}  ? [foo, bar] :
  T extends {bound: infer B extends number } ? B : never

Using template literal type

type Literal = switch T
  `0x${string}` then 'address'
  `hash_${Hex^}` then Hex

Real World Example

Take React-Query as an example.

DeepUnwrapRef<T> ::= switch T 
  UnwrapLeaf then T
  Ref<U^> then DeepUnwrapRef<U>
  {} then { [Property in keyof T]: DeepUnwrapRef<T[Property]> }
  else UnwrapRef<T>

can be compile down to

type DeepUnwrapRef<T> = T extends UnwrapLeaf
  ? T
  : T extends Ref<infer U>
    ? DeepUnwrapRef<U>
    : T extends {}
      ? {
          [Property in keyof T]: DeepUnwrapRef<T[Property]>
        }
      : UnwrapRef<T>

It is arguably more readable than the original type

Alignment with Civet Design Philosopy

• Less syntax: type level switch is less verbose IMHO
• Context matters: type level switch depends on the switch keyword appearing in type position
• Pragmatic: See the React Query as an example
• Configurable: This feature is separate from other features and can be turned off
• Evolve: If TypeScript supports regex literal type, pattern match can also evolve to use it.

[edemaine]

This looks like a great idea for addition! There are a few details that I'm not quite sure of, though your approach might be best:

• Should a pattern just be a type T or of the form < T / extends T? The latter fits our "condition fragments" in current switch (such as < 5). But given that all conditions in types involve extends, maybe it's redundant to include it? Also, we've generally thought of patterns as being types, so given that we're working with actual types here, I think it's reasonable for T to mean extends T... A possible "best of both" solution is that we could allow for both T and < T (and extends T), the former being shorthand for the latter.

• Related, it would be nice to allow for the negated form of extends. With patterns of the form < T / extends T, it's clear how to do so: !< T / !extends T / not extends T. With patterns of the form T, maybe we could allow for !T and not T.

• We have to choose whether

  • referenced types T are infer T by default and you need to use pins ^T to get the T in the outer scope (which seems more consistent with current switch), or
  • referenced types T reference the outer T by default and you need to use reverse pins T^ to bind T and get infer T (which is what you propose, with the argument that this prioritizes the more common case; it also makes the code closer to the corresponding to TypeScript, with the simple idea that T^ is shorthand for infer T).

  I'm not totally sure which is best here, and it would be good to hear from others.

[STRd6]

I'm a big fan of improving the usability of type level programming in Civet and happy to support any PR in this direction. It looks like a good overall approach with lots of compelling examples. As Erik mentions there are some nuances to work out but nothing insurmountable.

Thanks for the thoughtful and detailed request!

[HerringtonDarkholme]

Hi Civet team! Thanks for your prompt response and great consideration!

I do think most decisions here are trade-offs and more design taste than correctness. I will shed several thoughts on it but I respect all your decision.

But given that all conditions in types involve extends, maybe it's redundant to include it

Exactly, all conditions in types will need extends so it almost always needs a < if we want to keep a similar behavior with runtime pattern matching. However, there are several variants for conditional type, where we can put it in the match syntax

1. [ T ] extends [ Bound ] ? true : false is a way to avoid distributive conditional type
2. Using the exact Equal utility type [Feature request]type level equal operator microsoft/TypeScript#27024 (comment)
3. Using a sloppy equal type like [A] extends [B] ? [B] extends [A] ? true : false : false

However, I speculate most TypeScript users will need the plain A extends B syntax in most scenarios

it would be nice to allow for the negated form of extends

That sounds great. I think the compilation can be swapping the types in true/false positions. (Note users may not use infer in the matching.)

match T
  !number then 123
  string then '123'
  # !Ref<^T> then T # this does not work since we cannot use T
  
 # compiled 
 T extends number ?
   (T extends string ? '123' : never) # swapped part
     123 

referenced types T are infer T by default and you need to use pins ^T to get the T in the outer scope (which seems more consistent with current switch), or

If Civet choose this approach, the above React Query example will become

DeepUnwrapRef<T> ::= switch T 
  ^UnwrapLeaf then T
  ^Ref<U> then DeepUnwrapRef<U>
  {} then { [Property in keyof T]: DeepUnwrapRef<T[Property]> }
  else UnwrapRef<T>

I think this may be not as concise as the original example, because it is very common to use outer scope type in match.

[edemaine]

• [ T ] extends [ Bound ] ? true : false is a way to avoid distributive conditional type
• Using the exact Equal utility type [Feature request]type level equal operator microsoft/TypeScript#27024 (comment)
• Using a sloppy equal type like [A] extends [B] ? [B] extends [A] ? true : false : false

I wonder if we could allow for these with some kind of placeholder syntax. For example:

switch T
  [ & ] < [ Bound ]
    // [ T ] extends [ Bound ]
  Equal &, Foo < true
    // Equal<T, Foo> extends true
  Equal &, Foo
    // Possible shorthand for above, given that it has & so is clearly a condition
    // unless cyclic conditions like `T extends Equal<T, Foo>` are meaningful?
  [&] < [Foo] and [Foo] < [&]
    // if we want to be ambitious; alternatively, could make a helper

This is a natural extension of a previous proposal to allow functions as checkers in value pattern matching.

[vendethiel]

I have ^T vs T is especially rough here, becaus emost generally in pattern matching you want the default to be bind, and use ^ when you want to match. But here, binding is rarer.
There's one exception in pattern matching in ML: you never pin constructors. Maybe in Foo<T>, Foo could be construed to be a constructor?

[edemaine]

Agreed, Foo<T> (and its shorthand Foo T) should treat Foo as pinned.
I guess the tricky part is the standalone UnwrapLeaf in the following example:

DeepUnwrapRef<T> ::= switch T 
  UnwrapLeaf then T
  Ref U then DeepUnwrapRef U
  {} then { [Property in keyof T]: DeepUnwrapRef T[Property] }
  else UnwrapRef T

We could write ^UnwrapLeaf instead. But I'd also argue that UnwrapLeaf is a type, so maybe UnwrapLeaf should be legitimate here...?

This might be clearer if we wrote extends UnwrapLeaf or < UnwrapLeaf. Normally, condition fragments like this have a pinned expression on the right-hand side. Do we want to treat Ref<U> (pattern) and < Ref<U> (expression) differently?

[HerringtonDarkholme]

I wonder if we could allow for these with some kind of placeholder syntax.

This list a good unambiguous addition to pattern matching.

And this also reminds me that switch can take no argument. The example above will become

switch 
  [ T ] < [ Bound ]
  Equal T, Foo < true
  [T] < [Foo] and [Foo] < [T]

If we model the switch T as an extension of bare switch, the placeholder & will be natural to reference the var

switch T
& < Bound then A  # using placeholder
< Bound2  then B  # optional placeholder 
Bound3 then C      # optional extends operator

I would argue here that one single Bound variable in switch should never be a binding since the binding would always match. Similarly, value pattern match in Civet rejects bare variable binding.

What may be confusing is using bound inside object/array pattern. Consider

switch T
  [Head, ...Tails] then ???
  { project: Project } then ???

It is not clear to me if the type variable should be pinned or not.