Open8

Reconstructing TypeScript

unvalleyunvalley

型に対する理解を高める必要性に駆られていることがあり、TAPL.tsという勉強会に参加してる。現在は、Reconstructing TypeScriptというブログシリーズを読んでいる。このスクラップでは、そこで勉強したことや疑問などをまとめようと思う。

Reconstructing TypeScript, part 0: intro and background

unvalleyunvalley

Reconstructing TypeScript, part 0: intro and background

https://jaked.org/blog/2021-09-07-Reconstructing-TypeScript-part-0

What's a type checker?

As programmers, reasoning about the behavior of programs is our main job! We mostly do it in our heads, but it's really useful to automate it—to catch mistakes, and to support interactive development features like code completion. This is where a type checker comes in: it's a way to reason automatically at development time about the behavior of programs at run time.

プログラマーとして、プログラムの動作に関する推論は我々の主な仕事である!しかし、それを自動化することは、間違いを発見したり、コード補完のような対話的な開発機能をサポートしたりするのにとても便利だ。型チェッカーの出番だ。型チェッカーは、プログラムの実行時の振る舞いについて、開発時に自動的に推論する方法である。


Since a type checker runs at development time, it can't know the actual values flowing through a program at run time. Instead, for each expression in the program, it lumps together the values that might be computed by the expression, and gives the expression a type that describes attributes shared by all the values: what operations are supported; and, for some operations, what result they return.

型チェッカーは開発時に実行されるため、実行時にプログラムを流れる実際の値を知ることはできない。その代わりに、プログラム内の各式について、その式で計算される可能性のある値をひとまとめにし、すべての値に共通する属性(どのような演算がサポートされているか、演算によってはどのような結果を返すか)を記述した型をその式に与える。

What's cool about TypeScript?

Aside: unions vs. variants

Reconstructing TypeScript

Aside: Hindley-Milner type inference

Synthesizing a type from an expression

Subtyping

Checking an expression against a type

unvalleyunvalley

Reconstructing TypeScript, part 5: intersection types

https://jaked.org/blog/2021-10-28-Reconstructing-TypeScript-part-5

以下、論理的には同値になりそうだが、tscの都合で同じになっていない?

(x: number | string) => boolean
((x: number) => boolean) & ((x: string) => boolean)

intersectionの分配処理に対する分割統治法による最適化(uhyoさん提供)
https://github.com/microsoft/TypeScript/pull/57871


((x: number) => string) & ((x: number) => boolean))
// overloadによって解決されるけど、本当は number => neverの型定義になるはず?
type A1 = (1 | 2) & (2 | 3);
// intersection over union
// multiplication over addition
// 積の和に対して分配法則
type A2 = (1 & 2) | (1 & 3) | (2 & 2) | (2 & 3);