関数型 - pogi-log

関数型

関数型(function type)

域(domain)が$ A 、余域(codomain)が$ B であるような関数の型$ A \to B

$ \to : 型構築子、型コンストラクタ

型理論では指数型と呼べそう

型（＝集合）に対してと書かれる型（＝集合）を指数型〈exponential type〉と呼ぶことにします。これも大丈夫だよな、と思ったら、Wikipediaの exponential type は複素解析の話だった。けど、function type へのリンクもありました。指数型〈exponential type〉＝関数型〈function type〉です。

リスト、タプル、タグ付きデータ、関数、依存関数 - 檜山正幸のキマイラ飼育記 (はてなBlog)

対応するもの

(論理) 含意$ P \to Q

(集合) 関数集合(余域Bがサブシングルトンのとき) $ B^A

(圏論) 内部Hom/冪対象？(余域Bが部分終対象のとき)$ [A, B]

(型理論) 関数型(余域Bが命題/h-propositionのとき) $ A \to B

(ホモトピー論) 関数空間(余域Bがmere propositionのとき？)

確認用

Q. 関数型