型に関連するよく分からん用語がありすぎる

Rustのドキュメントを読んだりTwitterで型について話している人が使う用語でわからないものが結構ある。CSを体系的に学ぶ過程でおそらく共通で皆通ってきているのだろうが自分には抜け落ちている。この分野の用語を最低限自分も理解して使えるようになりたい。

とりあえず分からん用語調べてく

型付きラムダ計算

ラムダ計算 = 関数型プログラミングの中核機能を成す、変数、抽象(関数)、適用(関数呼び出し)のみをモデル化したもの

型付きラムダ計算 = ラムダ計算に型をつけたもの

部分型

型のポリモーフィズムの形態であり、上位と定義された型を、その下位と定義された型で、型安全性に則って代替できるというプログラミング言語理論の概念および実装を意味している。

例

subtype <: supertype

Integer <: Float <: Number

アヒル <: トリ

公称型 nominal subtyping

部分型であると宣言されたもののみを部分型とするもの

例

クラスベースオブジェクト指向言語

JavaやC++とか

構造的部分型 structual subtyping

型 A のオブジェクトが型 B のオブジェクトの処理できるメッセージすべてを処理できるなら（言い換えると、同じメソッドを実装していれば）、継承関係に関係なく、A は B の部分型となる。

シグネチャが同じであれば可換になる関係

例

sayのみを持つAliceクラスとsayのみを持つJohnクラスは互いに部分型の関係

TypeScriptやGolangとか

多相 polymorphism

それぞれ異なる型に一元アクセスできる共通接点の提供、またはそれぞれ異なる型の多重定義を一括表現できる共通記号の提供を目的にした、型理論またはプログラミング言語理論（英語版）の概念および実装

TaPL 22.7 let多相

多相性という言葉は、プログラムの一部分を、異なる文脈では異なる型として用いることを可能にする各種言語機能を指す。

TaPL 23.2 全称型

一つのコードを複数の型で扱えるようにする型システム

多相は文字通りポリモーフィクのことっぽい

部分型多相 subtype polymorphism

上位型をその下位型の数々で代替できるようにすること

オブジェクト指向言語の多態性

パラメトリック多相 parametric polymorphism

詳細化されていない型要素を内包する抽象的な型に記号表現を提供すること。

ジェネリクスや関数型言語の型構築子。

アドホック多相 ad-hoc polymorphism

恣意的な型の集合に一つの共通接点を提供する。

関数オーバーロード、Mix-inの実装、型クラスなど。

let多相

けど効率が悪いので、「決まらない型変数には∀をつける」方式を実際には採用

副作用を伴う場合は問題が起こるので値制限を導入する

誤解を生む多相性という言葉について

TaPL 23.2 全称型

System F(多相ラムダ計算)

そもそも全称とは

Wikipediaでは全称型=System Fになっているがどういうこと？

変数，抽象，適用からなる単純型付きラムダ計算に型抽象と型適用を加えて拡張した計算体型のこと

パラメータ多相を持った単純型付きラムダ計算

型抽象と型適用

つまり単純型付きラムダ計算に↑の型の抽象の仕組みを入れたモデルがSystem Fってやつか

存在型

■存在型は{ ∃X, T } と表記されています

つまり { ∃X, T } は「ある型X」と「Xを使った型」のペアを表しています。

■存在型の値は { *S, t } as { ∃X, T } と表記されています

{ *Bool, (false, 1) } as { ∃X, (X, Int) }

{ *Int, (1, 2) } as { ∃X, (X, Int) }

わかりやすい〜〜〜

code:ts

function useNumber(num: number) {

console.log(num);

}

function useString(str: string) {

console.log(str);

}

const thunks = [

];

func(param);

}

有界量化 bounded quantification

量化（りょうか、英: Quantification）とは、言語や論理学において、論理式が適用される（または満足される）議論領域の個体の「量」を指定すること。

例えば、算術において、「全ての自然数にはその次の数が存在する」と言った場合、あるいは論理学で、「ある議論領域に特定の属性をもつ事象が少なくとも1つ存在する」と言った場合、いずれも量化を行っている

型理論では、有界量化（有界量化または制約付き一般性）は、特定のタイプのサブタイプのみに及ぶように制限されている（「有界量化」）普遍的または存在記号を指します

パラメトリック多相とサブタイピングを組み合わせた型システムのことっぽい

有界量化とは、型パラメーターに対して部分型関係による制約を与えたものである。forall a. が forall a <: B. （型変数 a は型 B の部分型を動く）のようになる。Top 型があれば、非有界な量化と有界量化を統一できる。

System F に部分型付けと有界量化を加えたものは、 System F<: (System Fsub) と呼ばれる。

Java のジェネリクスを extends で制限するやつは有界量化っぽい。

code:example.ts

function changeBkColor<T extends HTMLElement>(element: T) {

element.backgroundColor = "red"

return element // => T

}

F有界量化 F-bounded quantification

System F に部分型付けと有界量化を加えたもの = System F<: (System Fsub)

型構築子

データ型の名前を定義するもの

Haskellでは

カインド(種類)

型式を引数の数によって分類するもの。「型の型」。単純型付きラムダ計算の1レベル上へ複製したもの。

調べるとHaskellの記事ばかり出てくるのでHaskellをちゃんとやればもっと何が嬉しいのかの実践的な理解が得られそう

バリアント

異種の値の混在した集まりを表す機構

例えば二分木(葉か二つの子を持った内部ノード)とか抽象構文木(変数とラムダ抽象と関数適用)

型変数の変性 variance

データコンテナのサブタイプ関係が、そのデータ要素のサブタイプ関係に連動して定義されるという概念を指す。また、関数の型のサブタイプ関係での、引数型と返り値型の汎化特化の制約を定義する概念でもある。ジェネリックなデータ構造、関数の型、クラスのメソッド、ジェネリックなクラス、ジェネリック関数などに適用されている

よく分からん!

変性というのは圏論由来の言葉らしい

変性（variance）とは、任意の型Tに対してどのような性質を持つのか示したもの

共変 covariant

?

Tそのものか、そのサブタイプが必要

例) Objectの場合

code:ts

// Objectはプロパティに対して共変なのでxはnumberかそのサブタイプ(1や2など)、yは1かそのサブタイプ(この場合は1しかない)

type Foo = {x: number, y: 1}

let a: Foo = {x: 1, y: 1} // ok

let b: Foo = {x: 1, y: 2} // error yは1でなきゃダメ

let c: Foo = {x: '1', y: 1} // error xはnumberじゃなきゃダメ

反変 contravariant

?

Tそのものか、そのスーパータイプが必要

code:ts

class A {}

class B extends A {}

class C extends B {}

type f = (args: B) => void;

// 反変なのでT(ここではB)かそのスーパータイプ(ここではA)だけが引数に取れる

const a: f = (args: A) => {} // ok

const b: f = (args: B) => {} // ok

const c: f = (args: C) => {} // error

双変 bivariant

?

要素型のサブタイプ関係を双方向にしてコンテナに反映させる。反変と同様にそのデータ要素は写像にされることが多い。双変は例えば、特化された定義域の写像コンテナと、汎化された定義域の写像コンテナを相互に置き換え可能にしたい時などに使われ、その写像の値域は通常invariantなのでList<特化> ≡ List<汎化> になる。

Tそのものか、そのスーパータイプ、もしくはサブタイプが必要

code:ts

class A {}

class B extends A {}

class C extends B {}

type f = (args: B) => void;

// 双変なのでT(ここではB)かそのスーパータイプ(ここではA)かそのサブタイプ(ここではC)が引数に取れる

const a: f = (args: A) => {} // ok

const b: f = (args: B) => {} // ok

const c: f = (args: C) => {} // ok

非変 invariant

?

要素型のサブタイプ関係をコンテナに反映しない。List<Cat>とList<Animal>は別系統のクラスになる。従ってList<Animal>型の変数に、List<Cat>型のインスタンスを代入するサブタイピングなどは出来ない。

Tそのものが必要

型安全性

型システムが条件を満たしたプログラムだと判断すれば、そのプログラム（またはプログラムフェーズ）は正しく型付けされていると言えます。型安全は正しく型付けされたプログラムが決して不正な動作をしないように保証します。そういうプログラムは（正しく定義された）意味を持つことになります。

一般に、「型検査で正しく型が付けられる」場合に「型エラーが起こらない」ことが保証される場合、その型システムは「健全である」あるいは「安全である」といい、このような性質を「健全性」あるいは「安全性」といいます。

つまり、型安全性というのはあくまで「その言語がどのような型システムを持つか」や「その言語でどのような場合を型エラーとするか」に基いて決まる、ということです。

これは、「A言語が型安全である」といった場合と、「B言語が型安全である」といった場合に、その論点がずれている可能性があることを示唆しています。

⊤型と⊥型

⊤型: トップ型

全ての型になり得る型

全ての上位型になる

⊥型: ボトム型

どの値も存在しない型

全ての部分型になる

代数的データ型

まぁ何読んでもピンとこない。とりあえずHeskellをやれば良いらしいよ。

occurrence typing

抽象的な型が分岐の中でより具体的な型に決まるやつ

ある変数xに関して型情報がわかりそうなconditionalがあると､その後のbodyにその型情報が伝播する

Racketのドキュメントを読むとそんな感じのことが書いてる

stratified type system

ググってもあんまり情報が出てこない

依存型 dependent type

値に依存する型のこと

wikipediaを読んでも全く分からん...

Dependent types とは, 項に 依存して 決まる型である.

ここで Vect は型変数 a だけでなく, リストの長さを表す自然数 n をパラメータとして取る. すなわち自然数の項が与えられなければ型を構成できない. この点で型 Vect は項に依存しているといえる.

よかった

一般化代数データ型 GADTs, generalized algebraic data types

何読んでも分からん。これを理解するために必要な知識がたくさんありそう...

少し噛み砕かれてるけどそれでも難しい...

まだ少し理解しやすいがしっくりこない

OCamlが解れば理解できそう

高階多相 higher-order polymorphism/higher-kinded polymorphism/higher-kinded types

これまたどの説明を理解するにも必要な知識が多い。Heskellが理解できてたらわかるっぽい。

このように Type ではなく Type -> Type などの複雑な「型の型」を持つものに対するジェネリクスを高カインド多相と呼びます（「型の型」はカインド（Kind）と呼ばれています）。

つまり、カインドに多相を提供するものか〜

TSでの実装を試みている記事

この記事で高カインド多相の話が出てくるが、型クラスの型引数にジェネリクスを使えないというところがトレイトとHaskellの型クラスと違うところであると述べている。高カインドとか多相がわかってくる。

感想

前半の用語はある程度経験のある言語でOOのXXのような機能のことと説明されると「あ〜あれか」となる。実際このレベルの理解ができれば実生活レベルでは十分ではある。

代数的データ型あたりからはその用語を理解するために必要な用語の理解も難しくて理解があやふや。ラムダ計算、Haskell・OCamlあたりの関数型言語での解説がほとんどになるためこれらの記法や言語について学んだ方が理解につながりそう。

ざっと読んだ。わかるところは前よりも増えたかな？くらいな感じ....。