Введение
Типизированный лямбда-исчисление, электронный транс-музыкант
System F (также полиморфное лямбда-исчисление или лямбда-исчисление второго порядка) — это типизированное лямбда-исчисление, которое добавляет к просто типизированному лямбда-исчислению механизм универсальной квантификации по типам. System F формализует параметрический полиморфизм в языках программирования, тем самым образуя теоретическую основу для языков, таких как Haskell и ML. Он был независимо открыт логиком Жаном Ивом Жираром (1972) и учёным-компьютерщиком Джоном К. Рейнольдсом. В то время как просто типизированное лямбда-исчисление имеет переменные, изменяющиеся в области термов, и связывающие для них, System F дополнительно имеет переменные, изменяющиеся в области типов, и связывающие для них. Например, тот факт, что функция тождества может иметь любой тип вида A → A, в System F формализуется как суждение
the electronic trance music artist
System F (also polymorphic lambda calculus or second order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphism in programming languages, thus forming a theoretical basis for languages such as Haskell and ML. It was discovered independently by logician Jean Yves Girard (1972) and computer scientist John C. Reynolds. Whereas simply typed lambda calculus has variables ranging over terms, and binders for them, System F additionally has variables ranging over types, and binders for them. As an example, the fact that the identity function can have any type of the form A → A would be formalized in System F as the judgement
где — переменная типа. Заглавные буквы традиционно используются для обозначения функций уровня типов, в отличие от строчных букв, используемых для функций уровня значений. (Надстрочный означает, что связанная x имеет тип ; выражение после двоеточия является типом предшествующего лямбда-выражения.) Как система переписывания термов, System F сильно нормализуема. Однако вывод типов в System F (без явных аннотаций типов) является неразрешимой задачей. В соответствии с изоморфизмом Карри-Ховарда, System F соответствует фрагменту интуиционистской логики второго порядка, использующему только универсальную квантификацию. System F можно рассматривать как часть лямбда-куба, вместе с ещё более выразительными типизированными лямбда-исчислениями, включая те, которые имеют зависимые типы. По словам Жирара, буква "F" в System F была выбрана случайно.
Использование в языках программирования
Версия Системы F, используемая в этой статье, является явно типизированным, или в стиле Церкви, исчислением. Информация о типах, содержащаяся в λ-термах, делает проверку типов простой. Джо Уэллс (1994) разрешил "неудобную открытую проблему", доказав, что проверка типов неразрешима для варианта Системы F в стиле Карри, то есть для варианта, которому не хватает явных аннотаций типов. Результат Уэллса подразумевает, что вывод типов для Системы F невозможен. Ограничение Системы F, известное как "Hindley–Milner" или просто "HM", действительно имеет простой алгоритм вывода типов и используется во многих статически типизированных функциональных языках программирования, таких как Haskell 98 и семейство ML. Со временем, по мере того как ограничения типовых систем в стиле HM становились очевидными, языки постепенно переходили к более выразительным логикам для своих типовых систем. GHC, компилятор Haskell, выходит за рамки HM (по состоянию на 2008 год) и использует Систему F, расширенную равенством типов, не являющимся синтаксическим; не-HM возможности в системе типов OCaml включают GADT.
Изоморфизм Жирара-Рейнольдса
В интуиционистской логике второго порядка полиморфный лямбда-исчисление второго порядка (F2) было открыто Жираром (1972) и независимо от него Рейнольдсом (1974).
Система F<:
Система F<:, произносится "F sub", является расширением системы F с подтипированием. Система F<: имеет ключевое значение для теории языков программирования с 1980-х годов, поскольку ядро функциональных языков программирования, таких как языки семейства ML, поддерживает как параметрический полиморфизм, так и подтипирование записей, которые могут быть выражены в системе F<:.