TypeScriptで、アロー（二重矢印「=>」〉で関数や型を書けるのはとても便利です。Lean 4では、アロー（一重矢印「→」）により依存関数空間型〈パイ型〉も記述できます。さらに便利です。
内容：
TypeScriptのアロー関数
TypeScriptでは、無名関数〈ラムダ抽象〉を(s: string) => s.length + 1のように書けます。これは、以前の書き方function(s: string){return (s.length + 1);}に比べると非常に簡潔で素晴らしい！ この簡潔な書き方による関数をアロー関数〈arrow function〉と呼ぶそうです。「アロー関数」という関数の種類があるわけではなくて、あくまで書き方です。
アロー記号〈二重矢印〉は型の構成にも使えて、上記のアロー関数の型は(s: string) => number型になります（TypeScriptにinteger型はありません）。次のような、型を明示した定義が書けます。
const f: (s: string) => number = (s: string) => s.length + 1;
ちょっと視認性が悪いですが、関数fの型が(s: string) => numberだと宣言しています。アロー記号で書ける型は関数型ですが、「関数型」は形容詞（英語なら functional）と誤解されるリスクがあるので、最近は「関数空間型」〈function space type〉「関数集合型〈function set type〉」と言うようにしています。圏論の言葉づかいなら「指数型」「内部ホム型」です。
関数と関数空間型の記述にアロー記号が使えるのはホントに便利なんですが、以前僕は悩んでしまったことがあります。次のように書いたのです。
const f: string => number = (s: string) => s.length + 1;
これはエラーになります。型の記述において、引数の名前は無意味なのでstring => stringと省略してもよさそうなもんですが‥‥。なぜ引数名が必須なのか事情はわかりませんが、そういう約束だと諦めましょう。
Lean 4の場合
最近気に入っているLean 4（「プログラミング言語Lean 4の現状」参照）でも、TypeScriptと同様な書き方ができます（「アロー関数」という言い方はしませんが）。
def f : String → Int := λ s => s.length + 1
関数空間型に引数名は不要で、String → Intと書けます。が、引数名を書いてもかまいません。
def f : (s : String) → Int := λ s => s.length + 1
多相関数の型の記述では引数名（パラメータ）が必要になります。
def g : (X : Type) → (List X → Int) := λ X => λ lis : List X => lis.length + 1
ここでXは型変数〈型パラメータ〉ですが、List Xのところで使われるので省略できません。TypeScriptで同様なことを書くと：
const g : (a: Array<X>) => number = (arr: Array<X>) => arr.length + 1
型変数は特に宣言されずに、山形括弧< >に入れることで型変数であることを示しています。型変数は特別扱いです。
Lean 4では、型変数を特別扱いすることはありません。普通のデータの変数、例えば整数変数と、型変数は同じように扱います。整数の自乗も型の自乗も同じ形です。
def square : Int → Int := λ n: Int => n*n def Square : Type → Type := λ X: Type => X×X
TypeScripでは、こんなに綺麗には揃いません。
const square : (n: number) => number = (n: number) => n*n; type Square<X> = [X, X];
パイ型〈依存関数空間型〉の記法
Lean 4の記法で書いた型(X : Type) → (List X → Int)は、依存型理論におけるパイ型〈Pi type〉です。パイ型は、依存関数達の型です。依存関数〈dependent function〉とは、引数値により余域（値を取る集合）の型が変わる関数です。パイ型を依存関数空間型〈dependent-function space type〉と言ってもいいでしょう*1。
パイ型の書き方は色々あります。
- 集合論的な記法： $`\prod_{X\in{\bf Type}} [\mathrm{List}(X), \mathrm{Int}]`$
- 述語論理の記法： $`\forall X\in{\bf Type}. \mathrm{List}(X) \Rightarrow \mathrm{Int}`$
- 束論的な記法： $`\bigwedge_{X\in{\bf Type}} [\mathrm{List}(X), \mathrm{Int}]`$
- 圏論的な記法： $`\mathrm{lim}_{X\in{\bf Type}} [\mathrm{List}(X), \mathrm{Int}]`$
一般的な形式は：
- 集合論的な記法： $`\prod_{x\in A} B`$
- 述語論理の記法： $`\forall x\in A. B`$
- 束論的な記法： $`\bigwedge_{x\in A} B`$
- 圏論的な記法： $`\mathrm{lim}_{x\in A} B`$
細かい差異まで入れると何十種類も書き方があるでしょう。重要な概念は何度も再発見されるために、単一の概念に多数の方言が存在します（「矢印の混乱に対処する： デカルト閉圏のための記法 // 矢印記号の憂鬱」も参照）。
Lean 4のパイ型の書き方(x: A) → B（$`(x: A) \to B`$）は非常に簡略で書くのが楽チンです。それと、指数型〈関数空間型〉A → Bとシームレスに統合されています。通常の関数の適用〈apply〉と依存関数の適用は次のように書けます。
$`\quad f: A \to B\quad a : A\\
\text{apply}\downarrow\\
\quad f\; a : B
`$
依存関数の場合は：
$`\quad f: (x : A) \to B\quad a : A\\
\text{dependent apply}\downarrow\\
\quad f\; a : B[a/x]
`$
ここで、$`A[a/x]`$ は、$`A`$ に含まれていた変数 $`x`$ を $`a`$ で置き換えたものです。
パイ型を(x: A) → Bとする書き方は、Agdaから借用したようですが、とても使い勝手がいいですね。簡潔すぎるのがデメリットとも言えます。Lean 4では、論理を扱うので∀x:X, Bという記法は残していますが、以前使えたΠx:X, Bは廃止しています。
僕は、歴史的経緯から同義な記法や用語が氾濫している事態にストレスを感じるので、スッキリした(x: A) → B（$`(x: A) \to B`$）が普及したらいいな、と思っています。
*1:パイ型／シグマ型の呼び名でドタバタした話は「依存型と総称型の圏論的解釈」の冒頭参照。その結果、パイ／シグマだけを使おうと決心したことは「依存型とΣ-Δ-Π随伴、そしてカン拡張」の冒頭。
