Dependent types and function bivariance
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.
leave a comment