関数タイプ

コンピュータサイエンスと数理論理学において、関数型（または矢印型、指数型）は、関数が持つ、または代入できる変数またはパラメータの型、あるいは関数を受け取ったり返したりする高階関数の引数または結果の型です。

関数の型は、関数のパラメータの型と結果の型に依存します（関数の型、より正確には、適用されていない型構築子は、 高カインド型· → ·です）。単純型ラムダ計算など、関数がカリー化形式で定義されている理論的設定とプログラミング言語では、関数の型は、定義域Aと値域Bのちょうど 2 つの型に依存します。ここで、関数の型は、数学的な慣例に従ってA → Bと表記されることが多く、または、集合のカテゴリにAからBへの集合論的関数のマッピングがちょうどB ^{A 個}（指数的に多い）存在することから、 B A と表記されることもあります。^このようなマップまたは関数のクラスは、指数オブジェクトと呼ばれます。カリー化を行うと、関数の型は積の型に随伴します。これについては、カリー化に関する記事で詳しく説明します。

関数型は、他の特性の中でも、多態的関数の概念を含む従属積型の特殊なケースと考えることができます。

いくつかのプログラミング言語の関数型に使用される構文は、高階関数合成関数の型シグネチャの例を含めて要約できます。

たとえば C# の型シグネチャの例を見ると、関数の型はcompose実際には ですFunc<Func<A,B>,Func<B,C>,Func<A,C>>。

C++11 の型消去により、高階関数のパラメータにはテンプレートを使用し、クロージャには型推論( )std::functionを使用するのが一般的になっています。 auto

プログラミング言語の関数型は、すべての集合論的関数の空間に対応しているわけではありません。定義域として自然数の可算無限型、値域としてブール値を考えると、それらの間には非可算無限数 (2 ^{ℵ ₀} = c ) の集合論的関数が存在します。この関数空間は、可算数のプログラム (有限個の記号の有限シーケンスであるプログラム) しか存在せず、集合論的関数の 1 つが停止問題を効果的に解決するため、どのプログラミング言語でも定義できる関数の数よりも明らかに大きいです。

表示的意味論は、関数型などのプログラミング言語の概念をモデル化するためのより適切なモデル (ドメインと呼ばれる) を見つけることに関係しています。プログラミング言語が非終了計算の記述を許可している場合 (プログラミング言語がチューリング完全である場合)、式を計算可能な関数の集合に制限するだけでは不十分であることが判明しています。式は、いわゆる連続関数(スコット位相における連続性に対応し、実際の解析的な意味での連続性ではありません) に制限する必要があります。その場合でも、連続関数の集合には並列論理和関数が含まれており、これをすべてのプログラミング言語で正しく定義できるわけではありません。

• デカルトの閉カテゴリ
• カレー作り
• 指数オブジェクト、圏論的同値
• ファーストクラスの機能
• 関数空間、集合論的等価物

• ピアス、ベンジャミン C. (2002)。型とプログラミング言語。MIT 出版。pp. 99–100。ISBN 9780262162098。
• ミッチェル、ジョン C. プログラミング言語の基礎。MIT プレス。
• nラボの機能タイプ
• ホモトピー型理論: 数学のユニバレント基礎、ユニバレント基礎プログラム、高等研究所。セクション 1.2 を参照してください。