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