型つきの、あなたの言語

最後の部品

コース2の終わりに、あなたは自分の言語に名前をつけて、リンクにして世に出しました。その言語は、いまもリンクの中に棲んでいます。今日の仕事は、その言語に最後の部品——型の目——を組みこむことです。

このコースのあいだ、型の目はずっと「庭が用意してくれた装置」でした。最終レッスンでは、それをあなたの側に引き取ります。確かめることは2つ——型検査器も作れるものであること、そしてその作りにはあなたが決めることが残っていることです。

木を、型に畳む

コース2で、あなたは評価器を作りました。あれは「木を値に畳むプログラム」でした——数の葉はその数、+ の節は左右を畳んでから足す、というふうに、switch文で木をたどる作りです。

型検査器の骨組みは、それとまったく同じです。ちがうのは、畳む先が値ではなく型であることだけ。

数の葉              → 数
名前の葉            → 型の名簿を引いて、その型
+ などの計算の節    → 左右を畳む。両方とも 数 なら、数。ちがえば、ここで報告
== などのくらべの節 → 左右を畳んで、真偽
呼び出しの節        → 引数の型を関数の札と照らして、合えば戻りの型

擬似コードで5行です。この庭の型の目の本体も、ほんとうにこの形のswitch文でできています——節の種類も、上に並べた5つ（数・名前・計算・くらべ・呼び出し）そのままです。評価器を一度自分の手で作ったあなたなら、この5行は「読める」だけでなく「作れる気がする」はずです。

どれも正解ではなく、選択

この庭の型の目には、作りの上の決めごとが3つあります。どれも、このコースのどこかであなたが踏んだものです。

• 注釈は必須——fn f(x) { x } と書くと「引数「x」の型が書かれていません。」と返ります。レッスン5で見たとおり、注釈を書かせず使われ方から型を推理する道（推論）もありました
• 名前の型は固定——x = 1 のあとで x に真偽を入れようとすると、「ひとつの名前には、ひとつの型」と止められます。同じ名前に別の種類を入れ直せて、実行のときに種類を確かめる言語も、世の中にはたくさんあります
• 検査は最初のまちがいで止まる——まちがいが2つあっても、報告されるのは手前の1つだけです。まちがいをできるだけ集めて、まとめて報告する作りの言語もあります

3つとも、正解ではありません。選択です。 コース2のレッスン11で「文法は、きみが決める」と学びました——あれはキーワードの話でしたが、型の目の作りにも、同じ問いがそのまま立ちます。あなたの言語なら、どう決めますか。

あなたの文法で、型の目が動く

最後の実験室です。コース2のレッスン11で差し替えたキーワード表と、このコースの型の目が、はじめてひとつの机に載っています。

fn を ことば に差し替えて、コードもそのことばで書き直してみてください。型の目は、何ごともなかったように働きつづけます——検査が見ているのは表記ではなく木であり、表記の自由と検査の厳しさは、ぶつからないのです。

それから、最後の行を nibai(1 == 2) にしてみてください。実行より先に「1番目の引数は 数 のはずですが、真偽 が渡されています。」と止まります。あなたの設計した見た目の言語が、あなたが雇った読み手に守られて動く——この一画面が、コース2とコース6の合流点です。

ひとつ、正直に言っておきます。この表で差し替えられるのは4つのキーワードだけで、型注釈の「数」「真偽」「:」は固定です。これもまた、この庭の選択でした——型の書き表し方まで設計できる作りにする道も、もちろんありえます。

歩いてきた道（コース6の総括）

• 実行は一本の道しか調べない。「動いた」と「正しい」はちがう
• 型とは、値の種類と、その種類にゆるされた操作の決まり
• 型検査器は、実行せずにプログラムを読むもうひとりの読み手。すべての道をいっぺんに調べる
• その正体は木を型に畳むswitch文——評価器と同じ骨格の、作れるもの
• 実行前の検査には登れる丘と登れない崖があり、型の目とテストは分業する
• 注釈か推論か、名前の型は固定か、どこで止まるか——どれも設計者の選択

六つの区画、ひとつの庭

ここで、入口からの道のりを一望します。あなたが歩いたのは、6つの区画でした。

• コース1 ことば——世界一誠実な読み手と、ことばを交わしました。エラーは攻撃ではなく、返事でした
• コース2 つくる——その読み手そのものを作りました。粒に分け、木にし、意味にする
• コース3 もよう——検索窓の裏に住む、いちばん小さな部類の言語の話者になりました
• コース4 かたち——同じ仕事の手順を、回数で測る目を得ました
• コース5 けいさん——計算の限界の崖まで歩いて、機械にできないことを証明つきで知りました
• コース6 かた——実行する前に読む、もうひとりの読み手を雇いました

並べてみると、6つの区画はぜんぶ、ひとつのことの周りを歩いていたと分かります。人がことばを書き、機械がそれを読む。 その営みを、使う側から、作る側から、測る側から、限界の側から、そして検査する側から眺めてきました。

庭の入口で、あなたはボタンを押して、誰かの言語に動いてもらう人でした。いまのあなたは、言語の読まれ方を知り、文法と型の目の決めごとをならべて、「自分ならこう決める」と言える人です。あなたはもう、言語を使う人ではなく、言語を設計する人です。

庭の出口で

あなたの言語は、ことばの工房でいつでも手に取れます。名前と、キーワード表と、プログラムをリンクにして、誰かに手渡せることも、コース2のままです。

この庭は無料で、登録もいらず、これからもこの場所にあります。何かを忘れた日も、誰かに説明したくなった日も、歩きたくなったら戻ってきてください——道は、あなたが覚えているとおりの場所にあります。

6つの区画ぜんぶの修了、おめでとうございます！　ここから先のことばは、あなたが決めてください。