К сожалению, «полярность» является несколько перегруженным понятием в теории типов. «Положительная позиция» и «отрицательная позиция» относятся к другому понятию полярности, чем то, о чем Боб говорит о фокусировке / поляризации.
Ваше значение
Когда вы определяете индуктивный тип, вы даете ряд правил, которые соответствуют операциям для определяемого вами типа. Например, вы можете сказать, что Natэто что-то с
- ценность
zero : Nat
- функция
suc : Nat -> Nat
А затем ожидать, что Natсодержит все значения, которые могут быть сгенерированы от повторного применения sucк другим Nats и включает zero. В соответствии с этой индуктивной конструкцией мы получаем принцип рекурсии по Nats, который работает на основе того факта, что что-либо Natгенерируется этими конструкторами.
rec : A -> (A -> A) -> Nat -> A
так что
rec Z S zero = zero
rec Z S (suc n) = S (rec Z S n)
Однако существуют некоторые ограничения на то, что мы можем написать как правила. В противном случае мы можем записать ряд правил, для которых принцип рекурсии не может быть оправдан. Рассмотрим «индуктивный тип» Dс одним конструктором
Здесь нет нормального принципа рекурсии. и не зря! Если бы у нас был какой-то принцип рекурсии, мы могли бы использовать его для кодирования версии собственного приложения, а вместе с ним - нетерминации. Это средство Dнельзя назвать «индуктивным», потому что индуктивные типы - это конечные конструкции, генерируемые из многократного применения конструкторов!
Чтобы справиться с этим, мы ограничимся тем, как индуктивные типы могут быть рекурсивными в теории типов. В частности, мы не дадим им появляться в «негативных местах». Это то понятие полярности, о котором вы говорили. Полярность положения определяется таким образом,
- Аргумент начинается в положительной позиции
- Каждый раз, когда мы идем влево стрелка, полярность меняется
Так Xчто положительный в первых двух и отрицательный во вторых двух
X
Int -> X
X -> Int
(Unit -> X) -> Int
Эта идея обосновывается обращением к теории категорий, где индуктивный тип, чьи единственные повторения являются положительными, порождает ковариантный функтор. Детали того, как это работает и почему это интересно, немного длинны.
Значение Боба Харпера
В своем блоге Харпер говорил о другом значении полярности. Эта полярность является ссылкой на то, как различные соединительные элементы в логике имеют значение. В частности, мы можем классифицировать соединительные элементы двумя способами
- Положительные связки могут быть определены путем определения того, как их вводить (правила их введения)
- Отрицательные связки могут быть определены путем определения их использования (правила их исключения)
В терминах языка программирования это хорошо отражает различие между ленивыми и строгими типами. Строгий тип определяется его значениями. Ленивый определяется тем, как образец может соответствовать им. Для правильной обработки мы определили язык с двумя основными конструкциями, способами построения положительных типов и «позвоночниками» для разложения отрицательных типов. Мы можем использовать это для включения как строгих, так и ленивых вычислений в один язык.
Для того , чтобы понять это лучше, я отсылаю вас к главе 38 Боба Харпера книги .
