Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Введение
В информатике и математической логике тип функции (или тип стрелки, или экспоненциальный тип) — это тип переменной или параметра, которому может быть присвоена функция, либо тип аргумента или результата функции высшего порядка, принимающей или возвращающей функцию. Тип функции зависит от типов параметров и типа результата функции (он, или точнее, непримененный конструктор типа · → ·, является типом высшего рода). В теоретических построениях и языках программирования, где функции определены в каррированной форме, таких как просто типизированное лямбда-исчисление, тип функции зависит ровно от двух типов: области определения A и области значений B. Здесь тип функции часто обозначается как A → B, следуя математической традиции, или B^(A), исходя из того, что существует ровно B^(A) (экспоненциально много) теоретико-множественных функций, отображающих A в B в категории множеств. Класс таких отображений или функций называется экспоненциальным объектом. Каррирование делает тип функции сопряженным к типу произведения; это подробно рассматривается в статье о каррировании. Тип функции можно рассматривать как частный случай зависимого типа произведения, который, помимо прочего, включает в себя понятие полиморфной функции.
In computer science and mathematical logic, a function type (or arrow type or exponential) is the type of a variable or parameter to which a function has or can be assigned, or an argument or result type of a higher order function taking or returning a function. A function type depends on the type of the parameters and the result type of the function (it, or more accurately the unapplied type constructor · → ·, is a higher kinded type). In theoretical settings and programming languages where functions are defined in curried form, such as the simply typed lambda calculus, a function type depends on exactly two types, the domain A and the range B. Here a function type is often denoted A → B, following mathematical convention, or B^(A), based on there existing exactly B^(A) (exponentially many) set theoretic functions mappings A to B in the category of sets. The class of such maps or functions is called the exponential object. The act of currying makes the function type adjoint to the product type; this is explored in detail in the article on currying. The function type can be considered to be a special case of the dependent product type, which among other properties, encompasses the idea of a polymorphic function.
Денотационная семантика
Тип функции в языках программирования не соответствует пространству всех функций теории множеств. Если рассматривать счетно бесконечный тип натуральных чисел как область определения и булевы значения как область значений, то между ними существует несчетно бесконечное число (2ℵ₀ = c) функций теории множеств. Очевидно, что это пространство функций больше, чем число функций, которые могут быть определены в любом языке программирования, поскольку существует лишь счетное количество программ (программа – это конечная последовательность конечного числа символов), и одна из функций теории множеств эффективно решает проблему останова. Денотационная семантика занимается поиском более подходящих моделей (называемых доменами) для моделирования концепций языков программирования, таких как типы функций. Оказывается, что ограничение выражений множеством вычислимых функций также недостаточно, если язык программирования позволяет записывать вычисления, которые не завершаются (что имеет место, если язык программирования является Тьюринг-полным). Выражения должны быть ограничены так называемыми непрерывными функциями (соответствующими непрерывности в топологии Скотта, а не непрерывности в реальном аналитическом смысле). Даже в этом случае множество непрерывных функций содержит параллельную или функцию, которую нельзя корректно определить во всех языках программирования.
The function type in programming languages does not correspond to the space of all set theoretic functions. Given the countably infinite type of natural numbers as the domain and the booleans as range, then there are an uncountably infinite number (2ℵ0 = c) of set theoretic functions between them. Clearly this space of functions is larger than the number of functions that can be defined in any programming language, as there exist only countably many programs (a program being a finite sequence of a finite number of symbols) and one of the set theoretic functions effectively solves the halting problem. Denotational semantics concerns itself with finding more appropriate models (called domains) to model programming language concepts such as function types. It turns out that restricting expression to the set of computable functions is not sufficient either if the programming language allows writing non terminating computations (which is the case if the programming language is Turing complete). Expression must be restricted to the so called continuous functions (corresponding to continuity in the Scott topology, not continuity in the real analytical sense). Even then, the set of continuous function contains the parallel or function, which cannot be correctly defined in all programming languages.