Функциональный тип

Функциональный тип (стрелочный тип, экспоненциал) в информатике — тип переменной или параметра, значением которой или которого может быть функция; либо тип аргумента или возвращаемого значения функции высшего порядка, принимающей или возвращающей функцию.

Функциональный тип зависит от типов параметров и типа результата функции. Другими словами, это тип высшего рода, или, более точно, неприменённый конструктор типов «${\displaystyle \cdot \to \cdot }$». В теоретических моделях и языках с поддержкой каррирования, например в просто типизированном лямбда-исчислении, функциональный тип зависит ровно от двух типов: области определения ${\displaystyle A}$ и области значений ${\displaystyle B}$. В этом случае функциональный тип, следуя математической традиции, обычно записывают как ${\displaystyle A\to B}$ (в практических языках программирования — A -> B), или как ${\displaystyle B^{A}}$, подразумевая, что существует ровно ${\displaystyle |B|^{|A|}}$ теоретико-множественных функций^[en], отображающих ${\displaystyle A}$ на ${\displaystyle B}$. С точки зрения соответствия Карри — Ховарда обитаемость функционального типа ${\displaystyle A\to B}$ эквивалентна доказуемости логической импликации ${\displaystyle A\Rightarrow B}$.

Функциональный тип можно рассматривать как частный случай зависимого произведения типов. Среди прочих свойств, такое представление несёт в себе идею полиморфной функции.

Языки программирования

В следующую таблицу сведён синтаксис, используемый в различных языках программирования для функциональных типов, а также соответствующие примеры сигнатуры типа для функции композиции функций.

Следует обратить внимание, что в примере на C# функция compose имеет тип «Func< Func<A,B>, Func<B,C>, Func<A,C> >».

Денотационная семантика

Функциональный тип в языках программирования не соответствует пространству всех теоретико-множественных функций. Если принять счётно бесконечный тип натуральных чисел в качестве области определения и тип булевых чисел в качестве области значений, то существует несчётное количество (${\displaystyle 2^{\aleph _{0}}={\mathfrak {c}}}$ — мощность континуума) теоретико-множественных функций между ними. Очевидно, это множество функций заведомо шире множества функций, определимых в языках программирования, так как существует лишь счётное множество программ (где программа представляет собой конечную цепочку из символов конечного набора).

Денотационная семантика занимается поиском более подходящих моделей (называемых областями^[en]), в том числе, для моделирования таких понятий языков программирования как функциональный тип. В денотационной семантике считается, что целесообразно не ограничиваться лишь вычислимыми функциями, а использовать любые непрерывные по Скотту функции на частично упорядоченных множествах, которыми возможно смоделировать также и незавершимые вычисления^[en] (а таковые возникают во всяком полном по Тьюрингу языке). Средства теории областей, используемые в денотационной семантике, достаточно выразительны, например, непрерывной по Скотту функцией моделируется «parallel or», определимый далеко не во всех языках программирования.

См. также

• Декартово замкнутая категория
• Экспоненциал — эквивалент в теории категорий
• Функции первого класса

Ссылки

• Бенджамин Пирс. Types and Programming Languages. — The MIT Press. — С. 99-100.
• Джон Митчел^[en]. Foundations for Programming Languages. — The MIT Press, 1996.
• Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program (англ.). Institute for Advanced Study (2013). — раздел 1.2

Эта страница в последний раз была отредактирована 25 апреля 2021 в 06:33.