Тип функции
В информатике и математической логике тип функции ( или стрелочный тип , или экспоненциальный тип ) — это тип переменной или параметра , которому функция может быть присвоена или которому она может быть присвоена, или тип аргумента или результата функции высшего порядка, принимающей или возвращающей функцию.
Тип функции зависит от типа параметров и типа результата функции (он, или, точнее, непримененный конструктор типа · → · , является типом более высокого рода ). В теоретических установках и языках программирования , где функции определяются в каррированной форме , таких как просто типизированное лямбда-исчисление , тип функции зависит ровно от двух типов: домена A и диапазона B. Здесь тип функции часто обозначается как A → B , следуя математическому соглашению, или B A , на основе существующего ровно B A (экспоненциально много) теоретико-множественных функций, отображающих A в B в категории множеств . Класс таких отображений или функций называется экспоненциальным объектом . Действие каррирования делает тип функции сопряженным к типу продукта ; это подробно рассматривается в статье о каррировании.
Тип функции можно рассматривать как частный случай типа зависимого произведения , который, помимо прочих свойств, включает в себя идею полиморфной функции .
Языки программирования
Синтаксис, используемый для типов функций в нескольких языках программирования, можно обобщить, включив пример сигнатуры типа для функции композиции функций высшего порядка :
| Язык | Обозначение | Пример подписи типа | |
|---|---|---|---|
| С функциями первого класса , параметрический полиморфизм | С# | Func<α1,α2,...,αn,ρ> | Func<A,C> compose(Func<B,C> f, Func<A,B> g); |
| Хаскелл | α -> ρ | compose :: (b -> c) -> (a -> b) -> a -> c | |
| OCaml | α -> ρ | compose : ('b -> 'c) -> ('a -> 'b) -> 'a -> 'c | |
| Скала | (α1,α2,...,αn) => ρ | def compose[A, B, C](f: B => C, g: A => B): A => C | |
| Стандартный МЛ | α -> ρ | compose : ('b -> 'c) -> ('a -> 'b) -> 'a -> 'c | |
| Быстрый | α -> ρ | func compose<A,B,C>(f: (B) -> C, g: (A) -> B) -> (A) -> C | |
| Ржавчина | fn(α1,α2,...,αn) -> ρ | fn compose<A, B, C>(f: fn(A) -> B, g: fn(B) -> C) -> fn(A) -> C | |
| С функциями первого класса , без параметрического полиморфизма | Идти | func(α1,α2,...,αn) ρ | var compose func(func(int)int, func(int)int) func(int)int |
| C++ , Objective-C , с блоками | ρ (^)(α1,α2,...,αn) | int (^compose(int (^f)(int), int (^g)(int)))(int); | |
| Без функций первого класса , параметрический полиморфизм | С | ρ (*)(α1,α2,...,αn) | int (*compose(int (*f)(int), int (*g)(int)))(int); |
| С++11 | Не уникально.
| function<function<int(int)>(function<int(int)>, function<int(int)>)> compose; | |
Если посмотреть на пример сигнатуры типа, например, C#, то тип функции composeна самом деле будет Func<Func<A,B>,Func<B,C>,Func<A,C>>.
Из-за стирания типов в C++11 для параметров функций высшего порядкаstd::function чаще используются шаблоны , а для замыканий — вывод типов ( ) .auto
Денотационная семантика
Тип функции в языках программирования не соответствует пространству всех теоретико-множественных функций. Если в качестве области определения взять счетно-бесконечный тип натуральных чисел , а в качестве диапазона — булевы значения, то между ними существует несчетно-бесконечное число (2 ℵ 0 = c ) теоретико-множественных функций. Очевидно, что это пространство функций больше числа функций, которые можно определить в любом языке программирования, поскольку существует только счетное число программ (программа — это конечная последовательность конечного числа символов), и одна из теоретико-множественных функций эффективно решает проблему остановки .
Денотационная семантика занимается поиском более подходящих моделей (называемых доменами ) для моделирования концепций языка программирования, таких как типы функций. Оказывается, что ограничение выражения набором вычислимых функций также недостаточно, если язык программирования позволяет писать нетерминированные вычисления (что имеет место, если язык программирования является полным по Тьюрингу ). Выражение должно быть ограничено так называемыми непрерывными функциями (соответствующими непрерывности в топологии Скотта , а не непрерывности в реальном аналитическом смысле). Даже тогда набор непрерывных функций содержит функцию parallel-or , которая не может быть правильно определена во всех языках программирования.
Смотрите также
- Декартово замкнутая категория
- Каррирование
- Экспоненциальный объект , категориально-теоретический эквивалент
- Первоклассная функция
- Функциональное пространство , эквивалент теории множеств
Ссылки
- Пирс, Бенджамин С. (2002). Типы и языки программирования . MIT Press. стр. 99–100. ISBN 9780262162098.
- Митчелл, Джон К. Основы языков программирования . MIT Press.
- тип функции в n Lab
- Теория гомотопических типов: унифицированные основы математики, Программа унифицированных основ, Институт перспективных исследований. См. раздел 1.2 .
