Znaczenie „pozycji dodatniej” i „pozycji ujemnej” w teorii typów?

Co oznacza „w pozycji dodatniej” i „w pozycji ujemnej” w kontekście teorii typów?

Jedyne, co zrozumiałem z postu na blogu Boba Harpera na ten temat , to istnienie związku między biegunowością w tym sensie w teorii typów a biegunowością w logice, ale nie wiem, co to za połączenie.

Niestety „biegunowość” jest nieco przeciążoną koncepcją teorii typów. „Pozycja dodatnia” i „pozycja ujemna” odnoszą się do innego pojęcia polaryzacji niż to, o czym mówi Bob z ogniskowaniem / polaryzacją.

Twoje znaczenie

Podczas definiowania typu indukcyjnego podajesz szereg reguł odpowiadających operacjom dla zdefiniowanego typu. Na przykład możesz powiedzieć, że a Natjest czymś

• wartość zero : Nat
• funkcja suc : Nat -> Nat

A potem oczekuj, że Natzawiera wszystkie wartości, które można wygenerować po wielokrotnym zastosowaniu sucdo innych Nats i obejmuje zero. Zgodnie z tą konstrukcją indukcyjną otrzymujemy zasadę rekurencji między Nats, która działa w oparciu o fakt, że dowolna Natjest generowana przez tych konstruktorów.

rec : A -> (A -> A) -> Nat -> A

po to aby

rec Z S zero = zero
rec Z S (suc n) = S (rec Z S n)

Istnieją jednak pewne ograniczenia dotyczące tego, co możemy napisać jako reguły. W przeciwnym razie możemy zapisać szereg zasad, dla których nie można uzasadnić zasady rekurencji. Rozważ „typ indukcyjny” Dz jednym konstruktorem

• d : (D -> D) -> D

Tutaj nie ma rozsądnej zasady rekurencji. i nie bez powodu! Gdybyśmy mieli jakąś zasadę rekurencji, moglibyśmy użyć jej do zakodowania wersji aplikacji własnej, a wraz z nią nieterminacji. Oznacza to, Dże nie można go nazwać „indukcyjnym”, ponieważ typy indukcyjne są konstrukcjami skończonymi generowanymi przez wielokrotne stosowanie konstruktorów!

Aby sobie z tym poradzić, ograniczamy możliwość rekurencji typów indukcyjnych w teorii typów. W szczególności zapobiegamy ich pojawianiu się w „negatywnych miejscach”. Jest to pojęcie polaryzacji, o którym mówiłeś. Tak więc biegunowość pozycji jest ustalana,

1. Argument zaczyna się od pozytywnej pozycji
2. Za każdym razem, gdy idziemy w lewo, strzałka zmienia biegunowość

Więc Xjest dodatni w pierwszych dwóch i ujemny w dwóch drugich

X
Int -> X
X -> Int
(Unit -> X) -> Int

Ta idea jest uzasadniona odwoływaniem się do teorii kategorii, w której typ indukcyjny, którego jedyne nawroty są dodatnie, powoduje funktor kowariantny. Szczegóły tego, jak to działa i dlaczego jest to interesujące, trochę długie.

Znaczenie Boba Harpera

Na swoim blogu Harper mówił o innym znaczeniu polaryzacji. Ta biegunowość odnosi się do tego, jak różne łączniki w logice mają znaczenie. W szczególności możemy klasyfikować łączniki na dwa sposoby

• Pozytywne łączniki można zdefiniować, definiując sposób ich wprowadzenia (ich zasady wprowadzania)
• Negatywne łączniki można zdefiniować, definiując sposób ich użycia (zasady ich eliminacji)

W języku programowania ładnie oddaje to rozróżnienie między typami leniwymi i surowymi. Typ ścisły jest definiowany przez jego wartości. Leniwy jest zdefiniowany przez to, jak można dopasować wzór na nich. Aby poradzić sobie z tym poprawnie, definiujemy język z 2 głównymi konstrukcjami, sposobami budowania typów pozytywnych i „kolcami” do rozkładania typów negatywnych. Możemy to wykorzystać do włączenia zarówno ścisłego, jak i leniwego obliczenia do jednego języka.

Aby to lepiej zrozumieć, odsyłam do rozdziału 38 Boba Harpera książki .