コンピュータープログラミングにおいて型システムとは、型と呼ばれるプロパティ(たとえば、integer、float、string ) をすべての用語(単語、語句、またはその他の記号のセット)に割り当てる一連のルールで構成される論理システム。

通常、用語は、変数、式、関数、モジュールなど、コンピュータプログラムのさまざまな言語構成要素です。型システムは、用語に対して実行できる操作を決定します。変数の場合、型システムによってその用語の許容値が決定されます。型システムは、代数データ型、データ構造、またはその他のコンポーネント (「文字列」、「浮動小数点数の配列」、「ブール値を返す関数」など)に対してプログラマが使用する暗黙のカテゴリを形式化し、強制する。

型システムは多くの場合、プログラミング言語の一部として指定され、インタプリタやコンパイラに組み込まれますが、言語の型システムは、言語の元の型構文と文法を使用して追加のチェックを実行するオプションのツールによって拡張できます。プログラミング言語における型システムの主な目的は、型エラーによるコンピュータープログラムのバグの可能性を減らすことです。問題の与えられた型システムは、型エラーの構成要素を決定しますが、一般に、目的は、特定の種類の値を期待する操作が、その操作が意味をなさない値 (妥当性エラー) で使用されるのを防ぐことです。型システムを使用すると、コンピュータープログラムのさまざまな部分間のインターフェイスを定義し、それらの部分が一貫した方法で接続されていることを確認できます。このチェックは、静的 (コンパイル時)、動的 (実行時)、またはその両方の組み合わせとして実行できます。型システムには、ビジネスルールの表現、特定のコンパイラの最適化の有効化、複数のディスパッチの許可、ドキュメントの形式の提供など、他の目的もあります。

【プログラミング】型システムの使用例

単純な型システムの例としては、C言語の型システムがあります。C プログラムの部分は関数定義です。ある関数が別の関数によって呼び出されます。関数のインターフェイスには、関数の名前と、関数のコードに渡されるパラメーターのリストが示される。呼び出し元の関数のコードには、呼び出される関数の名前と、その関数に渡す値を保持する変数の名前が示されます。実行中、値は一時ストレージに配置され、その後、実行は呼び出された関数のコードにジャンプします。呼び出された関数のコードは値にアクセスし、それらを使用します。

関数内の命令が整数値を受け取ることを想定して書かれているのに、呼び出しコードが浮動小数点値を渡した場合、呼び出された関数によって間違った結果が計算されます。C コンパイラは、関数が呼び出されたときに関数に渡された引数の型を、関数の定義で宣言されたパラメータの型と照合してチェックします。型が一致しない場合、コンパイラはコンパイル時エラーまたは警告をスローします。

コンパイラは、値の静的型を使用して、必要なストレージと値の操作のアルゴリズムの選択を最適化することもできます。たとえば、多くのCコンパイラでは、単精度浮動小数点数に関する IEEE 仕様に従って、float データ型は 32ビットで表されます。したがって、それらの値に対して浮動小数点固有のマイクロプロセッサ操作(浮動小数点加算、乗算など) を使用します。

型制約の深さとその評価方法は、言語の型指定に影響します。プログラミング言語はさらに、型多態性の場合、演算を型ごとのさまざまな解決策に関連付けることがあります。型理論は型システムの研究です。整数や文字列など、一部のプログラミング言語の具体的な型は、コンピューター アーキテクチャ、コンパイラーの実装、および言語設計の実際的な問題によって異なります。

コンピューター：自動装置

アーキテクチャ：建築

コンパイラー：翻訳

コンピュータ（英: computer）は、広義には、計算やデータ処理を自動的に行う装置全般のことである。今日では、特に断らない限りエレクトロニクスを用いたエレクトロニック・コンピュータ（英: electronic computer、漢字表記では電子計算機）を指す。

【プログラミング】型システムと型理論

型理論は型システムを研究する。プログラミング言語には、コンパイル時または実行時、手動で注釈が付けられたか自動的に推論されたかにかかわらず、型システムを使用して型チェックを行う機会が必要である。

型理論が扱う基本的な問題は、プログラムに意味があることを保証すること。型理論によって引き起こされる根本的な問題は、意味のあるプログラムが、それらに割り当てられた意味を持たない可能性があることでもあります。よりリッチ、複雑であり高価な型システムの探求は、より自分自身の勉強を深め楽しくさせるものでもある。

データ型の割り当て (タイピング)は、メモリ内の値や変数などのオブジェクトなどのビットシーケンスに意味を与えます。汎用コンピュータのハードウェアは、メモリ アドレスと命令コード、または文字、整数、浮動小数点数などを区別することができません。これは、可能性のある値の間で本質的な区別がないためです。ビットのシーケンスは を意味する可能性があります。ビットのシーケンスを型に関連付けると、その意味がプログラマブル ハードウェアに伝達され、そのハードウェアと何らかのプログラムで構成される記号システムが形成されている。

プログラムは各値を少なくとも 1 つの特定のタイプに関連付けますが、1 つの値が多数のサブタイプに関連付けられることもあります。オブジェクト、モジュール、通信チャネル、依存関係などの他のエンティティをタイプに関連付けることができます。タイプであっても、タイプに関連付けられる可能性があります。型システムの実装では、理論的には、データ型(値の型)、クラス(オブジェクトの型)、および種類( typeまたはメタタイプの型)と呼ばれる識別を関連付けることができます。これらは、システムに含まれるレベルの階層上で、入力が通過できる抽象化です。

プログラミング言語がより複雑な型システムを進化させると、基本的な型チェックよりもきめ細かいルール セットが得られますが、型推論 (およびその他のプロパティ) が決定不能になり、より多くの注意を払う必要がある場合、これには代償が伴います。プログラマは、コードに注釈を付けたり、コンピュータ関連の操作や機能を検討したりできます。タイプセーフな方法ですべてのプログラミング実践を満たす、十分に表現力豊かな型システムを見つけるのは困難です。

プログラミング言語コンパイラは、依存型またはエフェクト システムを実装することもできます。これにより、さらに多くのプログラム仕様を型チェッカーで検証できるようになります。単純な値と型のペアを超えて、コードの仮想「領域」は、what で何が行われているかを記述し、たとえばエラー レポートを「スロー」できるようにする「エフェクト」コンポーネントに関連付けられます。したがって、シンボリック システムは型と効果のシステムである可能性があり、型チェックだけよりも安全性チェックが強化されます。

コンパイラによって自動化されるか、プログラマによって指定されるかに関係なく、型システムは、型システムの規則から外れる場合、プログラムの動作を不正にします。

・抽象化（アブストラクション/Abstraction) – 型を使用すると、プログラマは低レベルの実装に煩わされることなく、ビットやバイトよりも高いレベルで考えることができます。たとえば、プログラマは文字列を単なるバイトの配列ではなく、文字値のセットとして考えることができるようになります。さらに言えば、型を使用すると、プログラマは任意のサイズの2 つのサブシステム間のインターフェイスを考えて表現できます。これにより、より多くのレベルのローカリゼーションが可能になり、2 つのサブシステムが通信するときにサブシステムの相互運用性に必要な定義の一貫性が保たれます。

・記録物化、文書化（ドキュメント/Document）– より表現力豊かな型システムでは、型はプログラマの意図を明確にするドキュメントの形式として機能します。たとえば、プログラマがタイムスタンプ型を返す関数を宣言した場合、コードのより深い部分でタイムスタンプ型を整数型として明示的に宣言できる場合、これはその関数を文書化します。

・最適化（オプティマイゼイション/Optimization）– 静的型チェックにより、コンパイル時に役立つ情報が得られる場合があります。たとえば、型が値をメモリ内で 4 バイトの倍数に整列させる必要がある場合、コンパイラはより効率的な機械命令を使用できる可能性があります。

・安全性（セイフティ/Safety）– 型システムにより、コンパイラーは無意味なコードまたは無効なコードを検出できます。たとえば、整数を文字列で3 / "Hello, World"割る方法がルールで指定されていない場合、式は無効であると識別できます。強い型付けは安全性を高めますが、完全な型の安全性を保証することはできません。

【プログラミング】タイプエラー（型エラー）

型エラーは、操作が予期したものとは異なる型のデータを受け取ったときに発生する。たとえば、コード上は稼働はするがサーバーやセキュリティ観点から見てみるとサーバー、セキュリティソフト、セキュリティシステムによって妨害されタイプエラーとなることはあります。これは、プログラム開発の複数の段階で現れる可能性があり意図しない状態でもある。したがって、型システムにはエラーを検出する機能が必要。Haskell など、型推論が自動化されている一部の言語では、エラーの検出を支援するためにコンパイラーで lintを利用できる場合があります。ですが安全性の面からみると型エラーは生じるのは必然ではなく確立した安全性のためでもあるでしょう。安全性の保障という意味合いでもセキュリティソフトやレンタルのサーバーがあるからです。

型安全性はプログラムの正確さに貢献しますが、型チェック自体を決定不可能な問題(停止問題など) にするという代償を払って正確性を保証するだけかもしれません。自動型チェックを備えた型システムでは、プログラムが正しく実行されていないことが判明しても、コンパイラエラーが発生しない場合があります。ゼロ除算は安全でなく、不正な操作ですが、コンパイル時にのみ実行される型チェッカーは、ほとんどの言語でゼロ除算をスキャンしません。この除算は実行時エラーとして表面化します。これらの欠陥がないことを証明するために、プログラム解析として総称される他の種類の形式的手法が一般的に使用されています。あるいは、依存型型言語などの十分に表現力豊かな型システムを使用すると、この種のエラー (たとえば、ゼロ以外の数値の型の表現) を防ぐことができます。さらに、ソフトウェア テストは、型チェッカーでは検出できないエラーを検出するための 経験的な方法です。

まとめ

・抽象化（アブストラクション/Abstraction)

・記録物化、文書化（ドキュメント/Document）

・最適化（オプティマイゼイション/Optimization）

・安全性（セイフティ/Safety）

プログラミングを勉強しているときに自分自身のパソコンのローカル環境をCDで入れるセキュリティソフトをインストールした時のローカル環境と普通のパソコン時でのローカル環境で２つで自分自身プログラミング言語で書いたプログラミングが作動するか調べているときに安全性の確証、保障という意味合いではお金を払って例えばサーバーを借りてブログをするという意味合いでもインターネットの検索エンジンでは探しても当たり前すぎて出てはこないが安全性の確証はどこにおいても大事だなと思った。

プログラミング言語においても大きな型システムのようなもので要はテクノロジーの切り抜きであり、私たちはその中で自然の中のものを切り抜いて使っていると思う。また、自然の中のものを切り抜いたうえで、いろいろとアーキテクチャである建築や組み立てなどを行っているのであると考えると楽しいなと思った。

パソコンにおいてもうろグラミング言語からプログラムであるソフトウェアをハードウェアで可視化されたものでもあるのでもう少し抽象度を上げるとすると、自然のプログラムを切り抜いて使っているものであり、かつ自然の中のテクノロジーを切り抜いているでもパソコンはあると。逆に電卓やスマートホン、イヤホン、コントローラー、ゲーム端末やゲームカセットもそうであろうと感じる。また逆に腕時計や時計なども裏には簡単ではあるが知らないプログラミング言語が書かれていたり、そのプログラミング言語によるっプログラムによって私たちはアナログの場合だと針や面に書いてある数字などで自分自身の今の時間帯を理解する。そのうえで私たちは誰かとご飯を行く約束をつけたり、だれかとデートする際はプランをある程度設計する。デジタル時計の場合もそうであり、裏のプラグラムによってデジタルで私たちは時間を可視化している。

最近の学びは自然の中の切り抜き✂。

わたしたちは自然の中のものを切り抜いて使っている。切り抜いたうえで自分自身の楽しいと思えるものを建築、組み立てたり、逆に１から作ったりしている。そう考えると自然っていいなと思った。

話を変えるとパソコンでもそうだが自動装置は、手動をあっての自動でもあり逆に機械の永遠の自動は難しい。そう考えると手動あっての機械ある程度の時間数のプログラムを入れて機械さんに動作してもらう。自動装置は自動だけど永遠に自動はできないがために何かの手動が１いるというものを最近は感じている。１回の手動で１つの機械の動作ではなくさまざまなバリエーションのプログラムを入れさまざまな自動間隔、自動数で機械の動作はできても永遠の自動は難しいなと思った。

最近読んだ本：タオは笑っている