reperiendi

Dependent types and function bivariance

Posted in Uncategorized by Mike Stay on 2021 January 27

TypeScript is unsound in part because of a desire to avoid forcing programmers to write a cast with no runtime effect just to satisfy the type checker. This code comes from their documentation on the unsoundness:

enum EventType {
  Mouse,
  Keyboard,
}

interface Event {
  timestamp: number;
}
interface MyMouseEvent extends Event {
  x: number;
  y: number;
}
interface MyKeyEvent extends Event {
  keyCode: number;
}

function listenEvent(eventType: EventType, handler: (n: Event) => void) {
  /* ... */
}

// Unsound, but useful and common
listenEvent(EventType.Mouse, (e: MyMouseEvent) => console.log(e.x + "," + e.y));

// Undesirable alternatives in presence of soundness
listenEvent(EventType.Mouse, (e: Event) =>
  console.log((e as MyMouseEvent).x + "," + (e as MyMouseEvent).y)
);
listenEvent(EventType.Mouse, ((e: MyMouseEvent) =>
  console.log(e.x + "," + e.y)) as (e: Event) => void);

// Still disallowed (clear error). Type safety enforced for wholly incompatible types
listenEvent(EventType.Mouse, (e: number) => console.log(e));

However, TypeScript now supports a restricted notion of dependent type, so the motivating example is no longer a problem:

// Assuming EventType, Event, MyMouseEvent, and MyKeyEvent as above

type GenericEvent<E extends EventType> = E extends EventType.Mouse ? MyMouseEvent : MyKeyEvent

function listenEvent<E extends EventType>(eventType: E, handler: (n: GenericEvent<E>) => void): void;
function listenEvent(eventType: EventType, handler: (n: GenericEvent<typeof eventType>) => void): void {
  /* ... */
}

// Valid
listenEvent(EventType.Mouse, (e: MyMouseEvent) => console.log(e.x + "," + e.y));
// Valid
listenEvent(EventType.Keyboard, (e: MyKeyEvent) => console.log(e.keyCode));
// Invalid
listenEvent(EventType.Mouse, (e: MyKeyEvent) => console.log(e.keyCode));
// Invalid
listenEvent(EventType.Mouse, (e: Event) => console.log(e.x + "," + e.y));

Dependent types don’t solve all the usability issues preventing soundness, but they remove a major one, and libraries should be updated to take advantage of dependent types.