コース 6

型のはなし — まちがいを、起きる前に

実行せずにプログラムを読む、もうひとりの読み手

誤りには、動かして初めて分かるものと、動かす前に分かるものがあります。コース2で作った言語に「型」という目を足して、後者を捕まえる仕組みを作ります。

01 まちがいには、種類がある動かして初めて分かる誤りと、動かす前に分かる誤り。実行は「通った道」しか調べてくれない。
02 値には、種類がある数と真偽。「値の種類」に名前をつけて、操作との相性を表にする——型という考え方の正体。
03 実行せずに読む、もうひとりの読み手型検査器の初登場。木はできたが、意味にする前——どの道も歩かずに、すべての道を調べる「型の目」。
04 名前の型は、変わらない最初の代入が、名前の型を決める。「動くのに止める」のは壊れ物の検知ではなく、型の目が選んだ約束——検査器の決まりも、設計である。
05 関数の型——注釈ということば引数の型は書き手が宣言し、戻りの型は機械が推論する。注釈は呼ぶ側と作る側、両方を縛る契約になる。
06 型は、うそをつかない説明書コメントはうそをついても誰も止めない。型注釈はうそをつくと、型の目が止める——「検査される説明書」の話。
07 型の目を、すりぬけるもの型のつじつまが合っていても、まちがいは起こりうる。値・時間・意図——型の目に見えない3つのものを、実験でたしかめます。
08 型つきの、あなたの言語最終レッスン。型検査器も「木を型に畳む」だけの、作れるもの。三つの設計の選択をたしかめて、あなたの言語に型の目を組みこむ——庭ぜんぶの、修了の回。