Параметричность

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

Идея

Рассмотрим этот пример, основанный на множестве X и типе T ( X ) = [ X → X ] функций из X в себя. Функция высшего порядка дважды _X : T ( X ) → T ( X ), заданная дважды _X ( f ) = f ∘ f , интуитивно независима от множества X . Семейство всех таких функций дважды _X , параметризованных множествами X , называется « параметрически полиморфной функцией ». Мы просто напишем дважды для всего семейства этих функций и запишем его тип как $\forall$Х. ​ Т ( Икс ) → Т ( Икс ). Отдельные функции дважды _X называются компонентами или экземплярами полиморфной функции. Обратите внимание, что все функции-компоненты дважды _X действуют «одинаково», потому что они заданы по одному и тому же правилу. Другие семейства функций, полученные выбором одной произвольной функции из каждого T ( X ) → T ( X ), не имели бы такой однородности. Их называют « специальными полиморфными функциями» . Параметричность — это абстрактное свойство, которым обладают равномерно действующие семейства, такие как дважды , что отличает их от специальных семейств. При адекватной формализации параметричности можно доказать, что параметрически полиморфные функции типа $\forall$Х. ​ T ( X ) → T ( X ) взаимно однозначны с натуральными числами. Функция, соответствующая натуральному числу n, задается правилом f $\mapsto$ ж ^н , т. е. полиморфное числительное Чёрча для n . Напротив, коллекция всех специальных семейств была бы слишком велика, чтобы представлять собой набор.

История

Теорема параметричности была первоначально сформулирована Джоном К. Рейнольдсом , который назвал ее теоремой абстракции . В своей статье «Теоремы бесплатно!» Филип Вадлер описал применение параметричности для вывода теорем о параметрически полиморфных функциях на основе их типов.

Реализация языка программирования

Параметричность — основа многих программных преобразований , реализованных в компиляторах языка программирования Haskell . Эти преобразования традиционно считались правильными в Haskell из-за нестрогой семантики Haskell. Несмотря на то, что Haskell является ленивым языком программирования, он поддерживает некоторые примитивные операции, такие как оператор seq- которые включают так называемую «выборочную строгость», позволяющую программисту принудительно вычислить определенные выражения. В своей статье «Свободные теоремы при наличии seq » Патрисия Йоханн и Янис Фойгтлендер показали, что из-за наличия этих операций общая теорема параметричности не справедлива для программ на Haskell; таким образом, эти преобразования в целом несостоятельны.

См. также

• Параметрический полиморфизм
• Нестрогий язык программирования

Внешние ссылки

• Вадлер: Параметричность