TS: Disallow cycles in types describing a state machine

Question

There's a multi-step process that I've implemented in my app as a state machine, and created types that express the possible state transitions:

enum ProcessStep {
  STEP_1,
  STEP_2a,
  STEP_2b,
  STEP_3
}
type ValidNextStep<Step extends ProcessStep> = {
  [ProcessStep.STEP_1]:
    | ProcessStep.STEP_2a
    | ProcessStep.STEP_2b;
  [ProcessStep.STEP_2a]: ProcessStep.STEP_3;
  [ProcessStep.STEP_2b]: ProcessStep.STEP_3;
  [ProcessStep.STEP_3]: never;
}[Step]

But I'd like to be able to tell if I've created a cycle in this graph, i.e. if ProcessStep.STEP_3 could transition back to ProcessStep.STEP_2a.

How might one go about establishing that kind of invariant at the type level? Seems tough, given that by default type aliases don't allow for circular references.

score 1 · Answer 1 · answered Jun 19 '19 at 01:05

Wow I love this question. I'm not sure if there's a clean or correct way to do this using just the type system.

Here's an unclean and possibly incorrect way: force the type system to go through the calculation of starting the state machine for every state and running it for some large number of steps. If every possible end state is never, then there are no cycles. Otherwise, there are either cycles or you have some really long acyclic paths in your graph.

Imagine you have an object type M which extends Record<keyof M, keyof M>, meaning that the values of M are also keys of M. This describes a state machine (you have such a type inside your definition of ValidNextStep but you destroy it by indexing into it... don't worry, we can reconstruct it as { [K in ProcessStep]: ValidNextStep<K> }). For any key K of M you can calculate M[K] for one step, or M[M[K]] for two steps, or M[M[M[K]]] for three steps, etc.

We can very quickly compose these operations to get crazy numbers of steps:

type TwoSteps<M extends Record<keyof M, keyof M>> = { [K in keyof M]: M[M[K]] };
type FourSteps<M extends Record<keyof M, keyof M>> = TwoSteps<TwoSteps<M>>;
type SixteenSteps<M extends Record<keyof M, keyof M>> = FourSteps<FourSteps<M>>;
type TwoHundredFiftySixSteps<M extends Record<keyof M, keyof M>> = SixteenSteps<
  SixteenSteps<M>
>;

That's about as far as I can get without the compiler yelling at me.

Then we can make a witness type that causes a compiler error if a cycle (or a very long path) is detected:

type NoCycles<
  N extends never = TwoHundredFiftySixSteps<
    { [K in ProcessStep]: ValidNextStep<K> }
  >[ProcessStep]
> = true;

That is fine for your original definition of ValidNextStep, but if we change it to the following:

type ValidNextStep<Step extends ProcessStep> = {
  [ProcessStep.STEP_1]: ProcessStep.STEP_2a | ProcessStep.STEP_2b;
  [ProcessStep.STEP_2a]: ProcessStep.STEP_3;
  [ProcessStep.STEP_2b]: ProcessStep.STEP_3;
  [ProcessStep.STEP_3]: ProcessStep.STEP_2a; // oops
}[Step];

Then the NoCycles definition yields the following error:

// Type 'ProcessStep.STEP_2a | ProcessStep.STEP_3' does not satisfy the constraint 'never'.

which shows that after running the machine for 256 steps it's still possible to be in either STEP_2a or STEP_3, which is indicative of a cycle.

Is this a good idea? Probably not... it is not guaranteed to be correct and it probably puts more strain on the compiler than is warranted. But I don't know how hard I'd want to try to find something better. With a general purpose language you'd try to find some efficient algorithm to detect a cycle, but it's unlikely that the type system in TypeScript is expressive enough to implement it.

So use that at your own risk, and good luck!

Link to code

Thanks for the interesting approach! Yeah, this would probably work for most cases so long as it's a relatively simple state machine, though it's definitely not ideal. Though for my purposes going for the, "terminates within at most n steps" approach is perhaps not the worst idea... I'll meditate on it! — osdiab, Jun 21 '19 at 00:31

TS: Disallow cycles in types describing a state machine

1 Answers1