🪨型システム(Type System)とは

プログラミング言語において, その式などの部分が持つ値を, その種類 (型 (type)) に沿って分類し, プログラムが正しく振る舞うこと, といった性質について保証する手法である.

型システムは, 型理論に基づいており, プログラミング言語の理論において最も確立された軽量形式手法である.

📝型(Type)は, 一般的には📝データ構造として知られている. このメモでもここのデータ構造はそちらにまとめて, このメモではシステムとしての側面をまとめる.

📝データ抽象(Data Abstruction)

データ抽象, Data Abstruction. Expression Problem における解決策.

データ抽象の実現方法

Data Abstruction は 2 つの実現方法がある.

🧩データ抽象の構成要素

3 つの構成要素がある.

  • Input
  • Output
  • Interface

データ抽象は内部と外部からなるプログラムかつ, 両者がインターフェースを通じてやりとりするもの.

A data abstraction is a part of a program that has an inside, an outside, and an interface in between The inside is hidden from the outside.

データを抽象的に使う, 使い方.実装にとらわれずにデータを使うこと. インタフェースと呼ばれる規則にしたがって使用される具体化の集合.

Input/Output

内部は外部からは隠蔽されている場合を🔖カプセル化(Encapsulation)という.

The inside is hidden from the outside.

📝インタフェース(Interface)

抽象データ型のメソッド.

The interface is a set of operations that an be used according to certain rules.

Object 型を分類し, 同じカテゴリに属するクラスに共通のインターフェイスを取り決める.

implements ステートメントは, クラスたちのカテゴリ分類を明確にする方法.

変数の型としてカテゴリクラスを指定すると, そのカテゴリを Implements したクラス (つまり, カテゴリに属するクラス) のインスタンスも格納できるようになる.

オブジェクトが共通のインターフェイスを実装している場合, 他のオブジェクトに置き換えることができる.

🔦データ抽象の説明いろいろ

CPMCPにおける説明

CPMCP p431.

データ抽象を型 (Type) といって済ますこともある. 📝抽象データ型(ADT)とは, 特殊なデータ抽象. 値の集合と, それに関する操作の集合. 以下のコンセプトに支えられている

  • High-order Programming (高階関数)
  • Static Scoping (クロージャ)
  • Explicit State (明示的状態)

SICP における説明

データオブジェクトをどう表現するかに関するプログラムの部分を, データオブジェクトをどう使うかに関するプログラムから隔離する方法.(SICP)

constructor(構成子), selector(選択子) によって、どう使うかに関するプログラムの 抽象の壁 を構築し、抽象レイヤを構築する.

これを、Data Abstruction(データ抽象) という.

データによるレイヤー構造を構築することで複雑なシステムをうまく構築することができる.

抽象の壁という意味は、壁をつくることで、ある場所での変更を局所的なレイヤの変更に封じこめることができる.

📝型(Type)

型, データ型, Type. 互いに関係する値の集合.

(OOP においては) 値の集合と値に対する操作の集合を一緒にしたもの.

📝型検査(Type Checking)

プログラムが型に整合性があるかどうかをチェックすること. 型チェック.

📝型推論

🔖動的型付け言語

🔖静的型付け言語

🆚動的型付け vs 静的型付け

動的型付けと静的型付けよる分類.

  • 動的片付け .. 実行時に型検査
  • 静的片付け .. コンパイル時に型検査

宗教論争のように根深いので, このdiscusstionをまとめる.

🔦静的型が邪魔だと言う人は限界な人達が書いた限界動的コードの面倒のつらさを知らない

;; https://x.com/ncaq/status/1699726265996263652

Clojureの作者もDHHもそうだけど、お前ら頭の良い人(皮肉)の基準で静的型が邪魔とか言ってるけど、限界な人達が書いた限界動的コードの面倒を見ないといけない人にとってはたまったものではないぞ

<2024-10-29 Tue 11:22> 笑ったwww

🆚型あり/型なし

型があるかないかよる分類.

  • 型なし (untyped)
  • 型あり (typed)

🔗References

up: 📂プログラミング言語処理系