Реализовать в Haskell церковную кодировку пары для полиморфного λ-исчисления/System F

Question

Я хочу реализовать Church encoding of the pair в полиморфном лямбда-исчислении в Haskell.

На странице 77, раздел 8.3.3 из Peter Selinger's notes on lambda calculus, он дает конструкцию декартово произведение двух типов, как

A × B = ∀α. (A → B → & alpha;) & alpha; →
⟨ М, N⟩ = Λα.λf ^{A → B → & alpha;} .fMN

Для другого источника, на странице 54, раздел 4.2.3 Dider Rémy's notes on lambda calculus, он определяет Church кодирование пары в полиморфной Х-исчислении/Система F как

Λα₁.Λα₂.λx₁:α₁.λx₂ α₂.Λβ.λy:α₁ → α₂ → β. y x₁ x₂

Я думаю, что Реми говорит то же самое, только более подробно, как Селинджер.

В любом случае, согласно Википедии, система типов для Haskell основана на System F, поэтому я надеюсь, что эту кодировку Церкви можно реализовать непосредственно в Haskell. У меня есть:

pair :: a->b->(a->b->c)->c 
pair x y f = f x y 

но я не был уверен, как это сделать.

Λα.Λβ.λp ^{α × β} .pα (Хе ^α .λy ^β .x)

Пользуюсь Я, Haskell forall для типа квантора капитала лямбды?

Это в основном то же самое, что и my previous question, но в Haskell вместо Swift. Я думал, что дополнительный контекст и смена места могут сделать его более разумным.

Answer 1

Прежде всего , вы действительно правы, что Селинджер и Реми говорят то же самое; разница заключается в том, что Rémy определяет функцию конструктора пар ⟨-, -⟩, которая принимает в качестве аргументов M и N (его x₁ и x₂) вместе с их типами (α₁ и α₂); остальная часть его определения - это просто определение ⟨M, N⟩ с β и y, где Selinger имеет α и f.

Хорошо, с этим позаботимся, давайте начнем перемещать выступы буксировки. Прежде всего следует отметить связь между ∀, Λ, → и λ и их эквивалентами в Haskell. Напомним, что ∀ и его обитатели Λ работают на типах, где → и его жителей λ действуют на значения.Над в Haskell-земле, большинство из этих соответствий легко, и мы получаем следующую таблицу

  System F        Haskell 
Terms (e)  : Types (t)  Terms (e)  :: Types (t) 
──────────────────────────────────────────────────────────────── 
λx:t₁.(e:t₂) : t₁ → t₂   \x::t₁.(e::t₂) :: t₁ -> t₂ 
Λα.(e:t)  : ∀α.t    (e::t)   :: forall α. t 

Запись термина уровня является легко: → становится -> и λ становится \. Но что относительно ∀ и Λ?

По умолчанию в Haskell все ∀s являются неявными. Каждый раз, когда мы ссылаемся на переменную типа (идентификатор нижнего регистра в типе), он неявно определяется количественно. Поэтому тип подписи, как

id :: a -> a 

соответствует

ID: ∀α.α → α

в системе F. Можно включить расширения языка ExplicitForAll и получить возможность писать те явно :

{-# LANGUAGE ExplicitForAll #-} 
id :: forall a. a -> a 

По умолчанию, однако, Haskell позволяет нам поставить эти кванторы в начале наших определений; мы хотим, чтобы система F-style могла размещать forall в любом месте в наших типах. Для этого мы включаем RankNTypes. На самом деле, все Haskell коды теперь будут использовать

{-# LANGUAGE RankNTypes, TypeOperators #-} 

(Другое расширение позволяет имена типов, чтобы операторы.)

Теперь, когда мы знаем, что мы можем попытаться записать определение ×. Я назову его версию Haskell **, чтобы все было в порядке (хотя мы могли бы использовать ×, если бы захотели). Определение Селинджер является

A × B = ∀α. (A → B → α) → α

поэтому Haskell является

type a ** b = forall α. (a -> b -> α) -> α 

И, как вы сказали, функция создания является

pair :: a -> b -> a ** b 
pair x y f = f x y 

Но что случилось с нашими Λs? Они находятся в определении системы F ⟨M, N⟩, но pair не имеет!

Так что это последняя ячейка в нашей таблице: в Haskell, всех Λs неявные, и даже не расширение, чтобы сделать их explicit.¹ Никуда они показали бы, мы просто игнорировать их, и типа вывод автоматически заполняет их. Итак, чтобы ответить на один из ваших прямых вопросов напрямую, вы используете Haskell forall для представления System F ∀ и ничего для представления лямбда Λ системы System F.

Таким образом, вы дать определение первого выступа, как (переформатировать)

proj₁ = Λα.Λβ.λp: α × α β.p (Хх: α.λy: β.х)

Мы переводим это Haskell, игнорируя все Λs и их приложения (и eliding типа annotations²), и мы получаем

proj₁ = \p. p (\x y -> x) 

или

proj₁ p = p (\x _ -> x) 

Наша система F версия имеет тип

proj₁: ∀α.∀β. & alpha; × β → α

или расширен

proj₁: ∀α.∀β. (∀γ. Α → β → γ) → α

и действительно, наша версия Haskell имеет тип

proj₁ :: α ** β -> α 

который снова расширяется до

proj₁ :: (forall γ. α -> β -> γ) -> α 

или, чтобы сделать связывание α и β явным,

proj₁ :: forall α β. (forall γ. α -> β -> γ) -> α 

и для полноты , у нас также есть

proj₂: ∀α.∀β. α × β → β
proj₂ = Λα.Λβ.λp: α × β.p & beta; (Хх: α.λy: β.y)

, которая становится

proj₂ :: α ** β -> β 
proj₂ p = p (\_ y -> y) 

, который, вероятно, неудивительно, в эта точка :-)

---

¹ Relatedly, все Λs могут быть удалены во время компиляции - информация о типе нет в скомпилированный код Haskell!

² Тот факт, что мы elide Λs означает, что переменные типа не связаны в терминах. Ниже ошибка:

id :: a -> a 
id x = x :: a 

, потому что он рассматривается, как если бы мы написали

id :: forall a. a -> a 
id x = x :: forall b. b 

, который, конечно, не работает. Чтобы обойти это, мы можем включить расширение языка ScopedTypeVariables; то переменные типа, связанные в явном forall, входят в сферу действия этого термина. Таким образом, первый пример все еще ломается, но

id :: forall a. a -> a 
id x = x :: a 

работает нормально.

Answer 2

Вы писали

Λα.Λβ.λp:α×β.p α (λx:α.λy:β.x) 

Просто удалите все аргументы типа, как в применении и абстракции:

λp:α×β.p (λx:α.λy:β.x) 

В Haskell без аннотации типа:

\p -> p (\x y -> x)