update: 型システムの背景理論を修正

docs/reference/advanced-topics/mental-model-of-types.md

@@ -4,15 +4,15 @@ sidebar_label: 型のメンタルモデル
 
 # 型システムの背景理論
 
-プログラミング言語の型システムにはそれぞれ固有の世界観があり、言語ごとにできること (型の機能) が異なります。その一方で、共有している機能もあります。さまざまな型の機能は唐突にどこからともなく出現してきたわけではありません。それぞれの背景には大きくは**型理論** (Type theory) と呼ばれる研究分野があり、各言語の型システムは型理論に基づいて実装されています。
+プログラミング言語の型システムにはそれぞれ固有の世界観があり、言語ごとにできること (型の機能) が異なります。
 
-たとえば、TypeScript の `unkown` 型や `never` 型といった一見なんのためにある型かわからないようなものであっても役割や機能は型理論においては一般にその概念を説明することができます。
+その一方で、共有している機能もあるわけで、それらのさまざまな型の機能は唐突にどこからともなく出現してきたわけではありません。背景として大きくは**型理論** (Type theory) と呼ばれる研究分野があり、各言語の型システムは型理論に基づいて実装されています。
 
-言語固有の型を一般化するような用語もあります。`unknown` 型や `never` 型は型理論においては Top 型や Bottom 型と呼ばれる型の種類に分類することができます。
+たとえば、TypeScript の `unkown` 型や `never` 型のような一見何のためにある型かわからないようなものであっても、型理論においてはその役割や機能を一般的に説明することができます。これらの型は Top 型や Bottom 型と呼ばれる型の種類に分類され、部分型関係の端点に位置する型として振る舞います。
 
 さらに型理論的な観点からの一般知識を持つことで似たような型システムを持つ他の言語においても型の機能について自然に推論することが可能になります。たとえば Scala という言語では `Any` 型と `Nothing` 型が `unknown` 型と `never` 型と同じ働きをすることが推論できます。一般化された型についての知識を使えるため、プログラミング言語をスイッチするような場合においてもスムーズに機能の類推や学習を行うことができるようになります。
 
-ただし、型理論は非常に奥深く難解でもあるため、一般にはとっつきにくい分野です。その一方で、比較的簡単に理解できて実用的にも役立つ概念も非常に多くあります。このドキュメントではそういった知識から TypeScript の型の世界観、いわばメンタルモデルを構築するための知識を紹介します。
+ただし、型理論は非常に奥深く難解でもあるため、一般にはとっつきにくい分野です。その一方で、比較的簡単に理解できて実用的にも役立つ概念も非常に多くあります。このドキュメントではそういった知識から TypeScript の型の世界観、いわば**メンタルモデル**を構築するための知識を紹介します。
 
 逆に、型理論の知識をもっておくことで一般化された型についての知識を使えるため、プログラミング言語をスイッチするような場合にはスムーズに機能の類推や学習を行うことができるようになります。