Алгебраически интерпретирующий полиморфизм

Ответ 1

Это известная лемма Yoneda для функции идентификации.

Отметьте этот пост для читаемого введения и любого учебника теории категорий для более.

Вкратце, учитывая f :: forall r. (a -> r) -> r, вы можете применить f id для получения a, и, наоборот, с учетом x :: a вы можете взять ($x), чтобы получить forall r. (a -> r) -> r.

Эти операции взаимно обратны. Доказательство:

Очевидно, ($x) id == x. Я покажу, что

($(f id)) == f,

поскольку функции равны, когда они равны для всех аргументов, возьмем x :: a -> r и покажем, что

($(f id)) x == f x i.e.

x (f id) == f x.

Так как f является полиморфным, он работает как естественное преобразование; это диаграмма естественности для f:

               f_A
     Hom(A, A)  →  A
(x.)      ↓        ↓ x
     Hom(A, R)  →  R
               f_R

So x . f == f . (x.).

Подключить идентификатор, (x . f) id == f x. QED

Ответ 2

(переписано для ясности)

Кажется, есть две части вашего вопроса. Один из них подразумевается и спрашивает, что такое алгебраическая интерпретация forall, а другая спрашивает о трансформации cont/Yoneda, которую ответ sdcvvc уже довольно хорошо охватывает.

Я попытаюсь обратиться к алгебраической интерпретации forall для вас. Вы отмечаете, что A -> B есть B^A, но я хотел бы сделать этот шаг дальше и развернуть его до B * B * B * ... * B (|A| times). Хотя у нас есть возведение в степень как обозначение для повторного умножения, то есть более гибкая нотация ∏ (верхний регистр Pi), представляющий произвольные индексированные продукты. В Pi есть два компонента: диапазон значений, которые мы хотим размножить, и выражение, которое мы умножаем. Например, на уровне значения вы можете выразить факториальную функцию как fact i = ∏ [1..i] (λx -> x).

Возвращаясь к миру типов, мы можем рассматривать оператор экспоненциальности в соответствии с A -> B ~ B^A как Pi: B^A ~ ∏ A (λ_ -> B). Это говорит о том, что мы определяем A -ричный продукт B s, такой, что B не может зависеть от выбранного нами A. Разумеется, это эквивалентно простому возведению в степень, но оно позволяет перейти к случаям, в которых есть зависимость.

В самом общем случае мы получаем зависимые типы, например, то, что вы видите в Agda или Coq: в синтаксисе Agda replicate : Bool -> ((n : Nat) -> Vec Bool n) - одно из возможных применений типа Pi, которое может быть выражено более явно как replicate : Bool -> ∏ Nat (Vec Bool), или далее как replicate : ∏ Bool (λ_ -> ∏ Nat (Vec Bool)).

Обратите внимание, что, как вы могли бы ожидать от лежащей в основе алгебры, вы можете сплавить обе ∏ в определении replicate выше в один диапазон ∏ по декартовому произведению доменов: ∏ Bool (\_ -> ∏ Nat (Vec Bool)) is эквивалентно ∏ (Bool, Nat) (λ(_, n) -> Vec Bool n) точно так же, как и на уровне значений. Это просто беспорядочно с точки зрения теории типов.

Я понимаю, что ваш вопрос касался полиморфизма, поэтому я остановлюсь на зависимых типах, но они имеют значение: forall в Haskell примерно эквивалентен ∏ с доменом над типом (видом) типов, *. Действительно, функциональноподобное поведение полиморфизма можно наблюдать непосредственно в ядре GHC, которое называет их капитальными лямбдами (Λ). Таким образом, полиморфный тип типа forall a. a -> a на самом деле просто ∏ * (Λ a -> (a -> a)) (используя теперь обозначение Λ, чтобы различать типы и значения), которые можно разложить до бесконечного произведения (Bool -> Bool, Int -> Int, () -> (), (Int -> Bool) -> (Int -> Bool), ...) для каждого возможного типа. Активация переменной типа просто проецирует подходящий элемент из продукта * -ary (или применяя функцию типа).

Теперь, для большой части, которую я пропустил в своей первоначальной версии этого ответа: параметричность. Параметричность может быть описана несколькими различными способами, но ни одна из тех, что я знаю (типы просмотра как отношения или (ди) естественность в теории категорий), действительно имеет очень алгебраическую интерпретацию. Однако для наших целей это сводится к чему-то довольно простому: вы не можете сопоставить образ на *. Я знаю, что GHC позволяет вам делать это на уровне типа с типами семейств, но при этом вы можете покрывать только конечный фрагмент *, поэтому обязательно всегда есть точки, в которых ваше семейство типов undefined.

Что это означает, с точки зрения полиморфизма, состоит в том, что любая функция типа F, которую мы пишем в ∏ * F, должна либо быть постоянной (т.е. полностью игнорировать тип, который был полиморфным), либо передавать тип через без изменений. Таким образом, ∏ * (Λ _ -> B) справедливо, поскольку игнорирует его аргумент и соответствует forall a. B. Другой случай - это что-то вроде ∏ * (Λ x -> Maybe x), что соответствует forall a. Maybe a, который не игнорирует аргумент типа, а только "передает его". Таким образом, a ∏ A, который имеет нерелевантную область A (например, когда A = *), можно рассматривать как большее число индексированного пересечения A (с учетом общих элементов во всех экземплярах индекса) а не продукт.

Важнейшим образом, на уровне значения правила параметричности предотвращают любое смешное поведение, которое может предполагать, что типы больше, чем они есть на самом деле. Поскольку у нас нет typecase, мы не можем построить значение типа forall a. B, которое делает что-то другое в зависимости от того, для чего был создан экземпляр A. Таким образом, хотя тип технически является функцией * -> B, он всегда является постоянной функцией и, таким образом, эквивалентен одному значению B. Используя интерпретацию ∏, она действительно эквивалентна бесконечному * -арьерному продукту B s, но те значения B всегда должны быть одинаковыми, поэтому бесконечное произведение эффективно превосходит единицу B.

Аналогично, хотя ∏ * (Λ x -> (x -> x)) (aka, forall a. a -> a) технически эквивалентен бесконечному произведению функций, ни одна из этих функций не может проверять тип, поэтому все ограничены только возвратом их входного значения, а не смешными бизнес, например (+1) : Int -> Int при создании экземпляра Int. Поскольку существует только одна функция (при условии полного языка), которая не может проверять тип своего аргумента, но должна возвращать значение того же типа, бесконечное произведение таким образом равно как одно значение.

Теперь о вашем прямом вопросе о (forall r . (a -> r) -> r) ~ a. Во-первых, более формально выразить оператор ~. Это действительно изоморфизм, поэтому нам нужны две функции, идущие туда и обратно, и аргумент, что они обращаются.

data Iso a b = Iso 
  { to   :: a -> b
  , from :: b -> a
  -- proof1 :: forall x. to (from x) == x
  -- proof2 :: forall x. from (to x) == x
  }

и теперь мы выражаем ваш первоначальный вопрос более формальными терминами. Ваш вопрос сводится к построению термина следующего (непроизводительного, поэтому у GHC есть проблемы с ним, но мы выживем):

forall a. Iso (forall r. (a -> r) -> r) a

Что, используя мою более раннюю терминологию, составляет ∏ * (Λ a -> Iso (∏ * (Λ r -> ((a -> r) -> r))) a). Еще раз у нас есть бесконечный продукт, который не может проверить его аргумент типа. Посредством ручной работы мы можем утверждать, что только возможные значения, учитывающие правила параметричности (два других доказательства соблюдаются автоматически) для to и from являются ($ id) и flip id.

Если это кажется неудовлетворительным, это, вероятно, потому, что алгебраическая интерпретация forall действительно ничего не добавила к доказательству. Это действительно простая теория старого типа, но я надеюсь, что смогу обеспечить что-то, что кажется немного менее категоричным, чем форма Йонеды. Стоит отметить, что на самом деле нам не нужно использовать параметричность для написания выше proof1 и proof2. Параметричность входит только в изображение, когда мы хотим заявить, что ($ id) и flip id являются нашими единственными опциями для to и from (которые мы не можем доказать в Agda или Coq по этой причине).

Ответ 3

Чтобы (попытаться) ответить на фактический вопрос (что менее интересно, чем ответы на более широкие вопросы, поднятые), вопрос плохо сформирован из-за "ошибки типа"

Either ~ (+) 
(,)    ~ (*)
(->) b ~ flip (^)
()   ~ 1
Void ~ 0 

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

Но это другое:

(forall r . (a -> r) -> r) ~ a

Он отображает тип в другой тип! Он не является частью вышеупомянутого функтора. Это просто изоморфизм в категории типов. Поэтому давайте укажем другой символ, <=>

Теперь мы имеем

(forall r . (a -> r) -> r) <=> a

Теперь вы заметите, что мы можем не только отправлять типы на nats и стрелки на стрелки, но и некоторые изоморфизмы на другие изоморфизмы:

(a, (b, c)) <=> ((a, b), c) ~ a * (b * c) = (a * b) * c

Но здесь происходит что-то тонкое. В некотором смысле последний изоморфизм на парах истинен, поскольку алгебраическое тождество истинно. Это означает, что "изоморфизм" в последнем просто означает, что эти два типа эквивалентны по образу нашего функтора для nats.

Первый изоморфизм нам нужно доказать непосредственно, а именно, где мы начинаем добираться до основного вопроса - задан наш функтор для нац, что означает forall r.? Но ответ заключается в том, что forall r. не является ни типом, ни значимой стрелкой между типами.

Введя forall, мы отошли от типов первого порядка. Там нет оснований ожидать, что все должны вписаться в наш вышеупомянутый Functor, и действительно, это не так.

Итак, мы можем исследовать, как и другие выше, почему изоморфизм имеет место (что очень интересно), но при этом мы отказались от алгебраического ядра вопроса. На вопрос, на который можно ответить, я думаю, есть категория высших порядков и конструкторов как стрелки между ними, что есть смысл Functor to?

Edit: Итак, теперь у меня есть другой подход, который показывает, почему добавление полиморфизма заставляет вещи сходить с ума. Начнем с более простого вопроса - имеет ли данный полиморфный тип нуль или больше нуля? Это проблема типа проблемы жилого помещения, и заканчивается тем, что через Карри-Ховард проблема в измененная реализуемость, поскольку это то же самое, что спрашивать, реализуется ли какая-либо формула в некоторой логике в соответствующей вычислительной модели. Теперь, как объясняет эта страница, это разрешимо в просто типизированном лямбда-исчислении, но PSPACE-complete. Но как только мы перейдем к чему-то более сложному, добавив, например, полиморфизм и перейдя в систему F, тогда он переходит к неразрешимым!

Итак, если мы не можем решить, где вообще заселен произвольный тип, то мы, очевидно, не можем решить, сколько у него жителей!

Ответ 4

Это интересный вопрос. У меня нет полного ответа, но это слишком долго для комментария.

Подпись типа (forall r. (a -> r) -> r) может быть выражена как я, говоря

Для любого типа r, который вы хотите назвать, если вы дадите мне функцию, которая принимает a и создает r, я верну вам r.

Теперь это должно работать для любого типа r, но может быть конкретным типом a. Таким образом, путь для меня в этом аккуратном трюке состоит в том, чтобы где-то где-то сидеть a, который я передаю функции (которая создает для меня r), а затем передаю вам r.

Но если у меня есть a, сидящий, я могу дать его вам:

Если вы дадите мне 1, я дам вам a.

который соответствует сигнатуре типа 1 -> a или просто a. По этому неофициальному рассуждению имеем

(forall r. (a -> r) -> r) ~ a

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

Ответ 5

Несколько ссылок на nLab:

• Универсальный квантификатор, соответствует зависимому продукту.

• Экзистенциальный квантификатор, соответствует зависимой сумме (зависимый копродукт).

Таким образом, в настройках теории категорий:

Type               | Modeled¹ as               | In category
-------------------+---------------------------+-------------
Unit               | Terminal object           | CCC
Bottom             | Initial object            |
Record             | Product                   |
Union              | Sum (coproduct)           |
Function           | Exponential               |
-------------------+---------------------------+-------------
Dependent product² | Right adjoint to pullback | LCCC
Dependent sum      | Left adjoint to pullback  |

¹) в соответствующей категории ─ CCC для общего и неполиморфного подмножества Haskell (ссылка), CPO для неопределенных черт Haskell (ссылка), LCCC для зависимых языков.

²) forall количественное определение является частным случаем зависимого продукта:

∀(x :: *). y[x] ~ ∏(x : Set)y[x]

где Set - universe всех малых типов.