Что такое предикативность?

Ответ 1

Позвольте мне добавить пункт, касающийся проблемы "этимологии", поскольку другой ответ от @DanielWagner охватывает большую часть технической базы.

Предикат на чем-то вроде a равен a -> Bool. Теперь предикатная логика - это та, которая может в некотором смысле рассуждать о предикатах - поэтому, если у нас есть предикат P, и мы можем говорить о данном a, P(a), теперь в "предикатной логике" ( таких как логика первого порядка), мы также можем сказать ∀a. P(a). Таким образом, мы можем количественно определять переменные и обсуждать поведение предикатов по таким вещам.

Теперь, в свою очередь, мы говорим, что утверждение является предикативным, если все вещи, к которым применяется предикат, вводятся до него. Поэтому утверждения "основываются" на вещах, которые уже существуют. В свою очередь, утверждение непротиворечиво, если оно может в некотором смысле ссылаться на себя своими "бутстрапами".

Таким образом, в случае, например, приведенный выше пример id, мы обнаруживаем, что мы можем присвоить тип id таким образом, чтобы он взял что-то типа id в нечто другое типа id. Итак, теперь мы можем дать функции тип, в котором квантифицированная переменная (введенная forall a.) может "расширяться" таким же типом, как и для всей самой функции!

Следовательно, непредсказуемость вводит возможность определенной "самореференции". Но подождите, можно сказать, не приведет ли такое к противоречию? Ответ: "ну, иногда". В частности, "Система F", которая является полиморфным лямбда-исчислением и существенным "ядром" языка "Ядро" GHC, допускает форму непротиворечивости, которая, тем не менее, имеет два уровня - уровень ценности и уровень типа, который разрешен количественно над собой. В этой двухуровневой стратификации мы можем иметь непроизводительность, а не противоречие/парадокс.

Хотя обратите внимание, что этот аккуратный трюк очень деликатный и легкий в использовании, добавив больше возможностей, поскольку в этом сборнике статей Олега указано: http://okmij.org/ftp/Haskell/impredicativity-bites.html

Ответ 2

Основной вопрос этих систем типов: "Можете ли вы заменить полиморфный тип для переменной типа?". Системы с предикативным типом - это бессмысленный школьный вопрос, "АБСОЛЮТНО НЕ", в то время как системы нечестного типа - ваш беззаботный приятель, который думает, что это звучит как забавная идея и что может пойти не так?

Теперь, Хаскелл немного обсуждает обсуждение, потому что считает, что полиморфизм должен быть полезным, но невидимым. Поэтому для остальной части этого сообщения я буду писать на диалекте Haskell, где использование forall не только разрешено, но и требуется. Таким образом, мы можем различать тип a, который является мономорфным типом, который извлекает свое значение из среды ввода, которую мы можем определить позже, и типа forall a. a, который является одним из более сложных полиморфных типов, которые будут использоваться. Мы также разрешим forall перемещаться в любом месте в любом типе - как мы увидим, GHC ограничивает свой синтаксис своего типа как "отказоустойчивый" механизм, а не как техническое требование.

Предположим, что мы сказали компилятору id :: forall a. a -> a. Можем ли мы позже попросить использовать id, как если бы он имел тип (forall b. b) -> (forall b. b)? Системы импрессивного типа в порядке, потому что мы можем создать квантификатор в типе id до forall b. b и подставить forall b. b для a всюду в результате. Системы с предикативным типом немного более осторожны: допускаются только мономорфные типы. (Так что если бы у нас был конкретный b, мы могли бы написать id :: b -> b.)

Там похожая история о [] :: forall a. [a] и (:) :: forall a. a -> [a] -> [a]. В то время как ваш беззаботный приятель может быть в порядке с [] :: [forall b. b] и (:) :: (forall b. b) -> [forall b. b] -> [forall b. b], предикативной школьной школы не так много. Фактически, как вы можете видеть только из двух конструкторов списков, нет возможности создавать списки, содержащие полиморфные значения, без создания экземпляра переменной в своих конструкторах до полиморфного значения. Поэтому, хотя тип [forall b. b] разрешен на нашем диалекте Haskell, это не очень разумно - нет (завершающих) терминов этого типа. Это мотивирует решение GHC жаловаться, если вы даже думаете о таком типе - это способ компилятора сказать вам "не беспокойтесь". *

Хорошо, что делает школьную школу настолько строгой? Как обычно, ответ заключается в том, чтобы сохранить проверку типов и сделать вывод типа. Типовой вывод для недискриминационных типов справедлив. Проверка типа кажется, что это возможно,, но это чертовски сложно, и никто не хочет этого поддерживать.

С другой стороны, некоторые могут возразить, что GHC совершенно доволен некоторыми типами, которые, как представляется, требуют непротиворечивости:

> :set -Rank2Types
> :t id :: (forall b. b) -> (forall b. b)
{- no complaint, but very chatty -}

Оказывается, что некоторые слегка ограниченные версии непротиворечивости не так уж плохи: в частности, типы проверки типов более высокого ранга (которые позволяют заменять переменные типа полиморфными типами, когда они являются только аргументами для (->)), относительно просто. Вы теряете тип вывода выше ранга-2, а основные типы выше ранга-1, но иногда более высокие типы рангов - это то, что доктор заказал.

Не знаю об этимологии слова, хотя!

* Вы можете задаться вопросом, можете ли вы сделать что-то вроде этого:

data FooTy a where
     FooTm :: FooTy (forall a. a)

Тогда вы получили бы термин (FooTm), у которого тип имел что-то полиморфное как аргумент для чего-то другого, кроме (->) (а именно, FooTy), вам не нужно пересекать школьную школу, чтобы это сделать, и поэтому вера "применение не-t219 > материала к полиморфным типам не полезна, потому что вы не можете их сделать" будет признана недействительной. GHC не позволяет писать FooTy, и я признаю, что не уверен, существует ли принципиальная причина для ограничения или нет.

Ответ 3

Я хотел бы прокомментировать проблему этимологии, поскольку ответ @sclv не совсем прав (этимологически, а не концептуально).

Вернитесь во времени, к временам Рассела, когда все задано теорией, включая логику. Одним из логических понятий конкретного импорта является "принцип понимания"; то есть, учитывая некоторый логический предикат φ:A→2, мы хотели бы иметь некоторый принцип, чтобы определить множество всех элементов, удовлетворяющих этому предикату, написанное как "{x | φ(x) }" или некоторое изменение на нем. Ключевым моментом, который следует иметь в виду, является то, что "наборы" и "предикаты" рассматриваются как принципиально разные вещи: предикаты являются отображениями от объектов к значениям истинности, а наборы являются объектами. Таким образом, например, мы можем разрешить количественную оценку по множеству, но не квантуя по предикатам.

Теперь Рассел был довольно обеспокоен его одноименным парадоксом и искал способ избавиться от него. Существует множество исправлений, но интерес к ним заключается в том, чтобы ограничить принцип понимания. Но сначала формальное определение принципа: ∃S.∀x.S x ↔︎ φ(x); то есть для нашего конкретного φ существует некоторый объект (т.е. set) S такой, что для каждого объекта (также множества, но считающегося как элемент) x мы имеем S x (вы может думать об этом как о значении "x∈S", хотя логики того времени дали "∈" другое значение, чем просто сопоставление) истинно только в случае, если φ(x) истинно. Если мы возьмем принцип точно так, как написано, то мы получим теорию нецелесообразности. Однако мы можем установить ограничения, на которые φ нам разрешено понимать. (Например, если мы говорим, что φ не должно содержать кванторов второго порядка.) Таким образом, для любого ограничения R, если множество S определяется (т.е. Порождено посредством понимания) некоторым R -predicate, то мы говорим, что S является "R -предикативным". Если каждое множество нашего языка R -предикативно, то мы говорим, что наш язык "R -предикативный". И тогда, как это часто бывает с дефинированными префиксными вещами, префикс выпадает и остается неявным, откуда "предикативные" языки. И, естественно, языки, которые не являются предикативными, являются "непроницаемыми".

Это старая школьная этимология. С тех пор эти термины ушли и получили собственные жизни. Способы использования "предикативных" и "опровергающих" сегодня совершенно разные, потому что вещи, которые нас беспокоят, изменились. Поэтому иногда бывает трудно понять, как черт наш современный подход связан с этим. Честно говоря, я не думаю, что знание этимологии действительно помогает любому с точки зрения выяснения того, что на самом деле слова (в наши дни).