依存関数型
出力の型が入力の値によって異なるような関数型
表記
Leanでは以下のように表記する
(a : α) → β a
例えば、上記のような型を持つ関数f : (a : α) → β aを考えると
f によって返される値 f a の型 β a は、入力 a に依存して変わるということ
https://gyazo.com/81b4cc252727eef3e90bc3bd339ad0cc
$ \Pi_n:\mathrm{Nat}.A^n
Leanでの(n : Nat) -> A^nと同じ
通常の関数型の一般化
α → β という記法は
β が a : α に依存しないときの
(a : α) → β の略記に過ぎない。
code:lean
def cons (α : Type) (a : α) (as : List α) : List α :=
List.cons a as
#check cons Nat -- Nat → List Nat → List Nat #check cons Bool -- Bool → List Bool → List Bool #check cons -- (α : Type) → α → List α → List α これだけ見ると、単純なparametric多層と同じ様に見えるmrsekut.icon
code:ts
const cons = <A>(x: A) => (xs: A[]): A[] => x, ...xs; GPT-4.icon
Leanの依存型(dependent types)とTypeScriptのジェネリクス(generics)は、表面的に似ているように見えるかもしれませんが、本質的には異なる概念です。依存型システムは、型が値に依存することを可能にするため、より表現力が高いです。一方、ジェネリクスは型の再利用性を高めるための機能ですが、型が値に依存することはできません。
Leanの例では、cons関数は任意の型αに対して、その型の値を取り、その型のリストにその値を追加して新しいリストを返す関数です。この関数定義では、αは型引数であり、関数の引数aとasの型に依存しています。これは、αがどのような型であっても機能することを意味します。
TypeScriptのジェネリクスを使用した例では、cons関数はある型Aの値を取り、その型の配列にその値を追加して新しい配列を返します。ここでの<A,>はジェネリック型引数であり、関数が任意の型の値と配列で動作することを意味しますが、型が特定の値に依存するわけではありません。
依存型とジェネリクスの主な違いは、依存型が型が値に依存できるようにする点にあります。依存型を使用すると、例えば、特定の長さのベクターや値に基づいて変化する型を表現できます。これにより、コードの安全性をコンパイル時にさらに強化できます。Leanのような依存型言語では、このような性質を使って、プログラムの正確性に関する証明を書くことができます。
TypeScriptのジェネリクスは、コードの柔軟性と再利用性を高めるために非常に便利ですが、依存型言語が提供するレベルの厳密さや表現力には及びません。ジェネリクスは型レベルでの操作をより柔軟にしますが、依存型は型と値の間のより深い関係を許容し、プログラムの正確性をコンパイル時に検証するための強力なツールを提供します。
値と型の依存の方向性が逆ってこと？
どのように？
まあ、直積が関数の一般化というのは、依存型関係なくそうかmrsekut.icon
そういう意味で依存直積型に「Π」を使うのはわかる
nLabではdependent function typeのリンクを飛ぶとdependent product type (依存直積型)のページへリダイレクトされる GPT-4.icon
nLabで「dependent function type」が「dependent product type」にリダイレクトされるのは、型理論においてこれらが同じ概念を指すためです。つまり、依存関数型は依存直積型の特別なケースと見なされることがあります。依存和型は異なる概念ですが、依存型を使用する点で関連しています。
よくわからんmrsekut.icon
GPT-4.iconが言っていることが正しいのかどうかもわからん、たぶん違う気がする