Ścisła pozytywność

Z tego odniesienia: Ścisła pozytywność

Surowy warunek dodatni wyklucza deklaracje takie jak

data Bad : Set where
 bad : (Bad → Bad) → Bad
         A      B       C
 -- A is in a negative position, B and C are OK

Dlaczego A jest ujemne? Również dlaczego B jest dozwolone? Rozumiem, dlaczego C jest dozwolone.

Najpierw wyjaśnienie terminologiczne: pozycje negatywne i pozytywne pochodzą z logiki. Są o asymetrii w zdaniotwórczych logiczne: w zachowuje się inaczej B . Podobnie dzieje się w teorii kategorii, gdzie mówimy kontrawariantny i kowariantna zamiast negatywnych i pozytywnych, odpowiednio. W fizyce mówią o wielkościach, które zachowują się „kowariantnie” i „również przeciwnie”. Jest to więc bardzo ogólne zjawisko. Programista może myśleć o nich jako o „danych wejściowych” i „danych wyjściowych”.$A \Rightarrow B$$A$$B$

Teraz na indukcyjne typy danych.

$T$$T$$T$

W algebrze zwyczajowo operacja pobiera skończoną liczbę argumentów, aw większości przypadków przyjmuje zero (stała), jeden (unary) lub dwa (binarne) argumenty. Uogólnienie jest wygodne dla konstruktorów typów danych. Załóżmy, że cjest konstruktorem typu danych T:

• jeśli cjest stałą, możemy myśleć o niej jako o funkcji unit -> Tlub równoważnie (empty -> T) -> T,
• jeśli cjest jednoargumentowy, możemy myśleć o tym jako o funkcji T -> Tlub równoważnie (unit -> T) -> T,
• jeśli cjest binarny, możemy myśleć o nim jako o funkcji T -> T -> Tlub równoważnie T * T -> Tlub równoważnie (bool -> T) -> T,
• gdybyśmy chcieli konstruktora, cktóry przyjmuje siedem argumentów, moglibyśmy postrzegać go jako funkcję, w (seven -> T) -> Tktórej sevenjest jakiś wcześniej zdefiniowany typ z siedmioma elementami.
• możemy również mieć konstruktor, cktóry przyjmuje niezliczoną liczbę argumentów, co byłoby funkcją (nat -> T) -> T.

Te przykłady pokazują, że ogólna forma konstruktora powinna być

c : (A -> T) -> T

gdzie my nazywamy Aten arity się ci myślimy cjako konstruktor, że trwa Ato wiele argumentów typu Tprodukować element T.

Oto coś bardzo ważnego: arie muszą zostać zdefiniowane przed zdefiniowaniem T, w przeciwnym razie nie będziemy w stanie powiedzieć, co powinni robić konstruktorzy. Jeśli ktoś próbuje mieć konstruktora

broken: (T -> T) -> T

następnie pytanie „ile argumentów brokenpotrzeba?” nie ma dobrej odpowiedzi. Możesz spróbować odpowiedzieć na to „potrzeba Twielu argumentów”, ale to nie zadziała, ponieważ Tnie zostało jeszcze zdefiniowane. Możemy próbować wydostać się z trybuny, stosując fantazyjną teorię punktu stałego, aby znaleźć typ Ti funkcję iniekcyjną (T -> T) -> T, i to się udałoby, ale po drodze złamalibyśmy zasadę indukcji T. Tak więc to po prostu zły pomysł, aby spróbować czegoś takiego.

$\lambda$$v$$\lambda \cdot v$cB

c : B * (A -> T) -> T

Rzeczywiście, wiele konstruktorów można przepisać w ten sposób, ale nie wszyscy, potrzebujemy jeszcze jednego kroku, a mianowicie powinniśmy pozwolić Ana poleganie na B:

c : (∑ (x : B), A x -> T) -> T

Jest to ostateczna forma konstruktora typu indukcyjnego. Dokładnie takie są też typy W. Forma jest tak ogólna, że ​​zawsze potrzebujemy tylko jednego konstruktora c! Rzeczywiście, jeśli mamy dwa z nich

d' : (∑ (x : B'), A' x -> T) -> T
d'' : (∑ (x : B''), A'' x -> T) -> T

wtedy możemy połączyć je w jedno

d : (∑ (x : B), A x -> T) -> T

gdzie

B := B' + B''
A(inl x) := A' x
A(inr x) := A'' x

Nawiasem mówiąc, jeśli curry ogólną formę, zobaczymy, że jest ona równoważna

c : ∏ (x : B), ((A x -> T) -> T)

co jest bliższe temu, co ludzie zapisują w asystentach dowodowych. Asystenci dowodu pozwalają nam zapisać konstruktory w wygodny sposób, ale są one równoważne z powyższą ogólną formą (ćwiczenie!).

Pierwsze wystąpienie Badnazywa się „negatywne”, ponieważ reprezentuje argument funkcji, tj. Znajduje się po lewej stronie strzałki funkcji (patrz typy rekurencyjne za darmo przez Philipa Wadlera). Myślę, że pochodzenie terminu „pozycja negatywna” wynika z pojęcia kontrowariancji („contra” oznacza przeciwieństwo).

Niedopuszczalne jest definiowanie typu w pozycji ujemnej, ponieważ można w nim pisać programy nie kończące się, tzn. Silna normalizacja zawodzi w jego obecności (więcej na ten temat poniżej). Nawiasem mówiąc, jest to przyczyną nazwy reguły „ścisła pozytywność”: nie dopuszczamy pozycji negatywnych.

Dopuszczamy drugie wystąpienie, Badponieważ nie powoduje to braku zakończenia i chcemy użyć typu zdefiniowanego ( Bad) w pewnym momencie w rekurencyjnym typie danych ( przed ostatnią strzałką jego konstruktora).

Ważne jest, aby zrozumieć, że poniższa definicja nie narusza ścisłej zasady pozytywności.

data Good : Set where
  good : Good → Good → Good

Reguła dotyczy tylko argumentów konstruktora (które są oba Goodw tym przypadku), a nie samego konstruktora (patrz także „ Certyfikowane programowanie z typami zależnymi ” Adama Chlipali ).

Kolejny przykład naruszający ścisłą pozytywność:

data Strange : Set where
  strange : ((Bool → Strange) → (ℕ → Strange)) → Strange
                       ^^     ^
            this Strange is   ...this arrow
            to the left of... 

Możesz także sprawdzić tę odpowiedź na temat negatywnych pozycji.

Deklaracje, które nie są ściśle dodatnie, są odrzucane, ponieważ można na ich podstawie napisać funkcję nie kończącą się. Aby zobaczyć, jak można napisać definicję zapętlenia przy użyciu typu danych Bad z góry, zobacz BadInHaskell .

Oto analogiczny przykład w Ocaml, który pokazuje, jak zaimplementować zachowanie rekurencyjne bez (!) Bezpośredniego użycia rekurencji:

type boxed_fun =
  | Box of (boxed_fun -> boxed_fun)

(* (!) in Ocaml the 'let' construct does not permit recursion;
   one have to use the 'let rec' construct to bring 
   the name of the function under definition into scope
*)
let nonTerminating (bf:boxed_fun) : boxed_fun =
  match bf with
    Box f -> f bf

let loop = nonTerminating (Box nonTerminating)

W nonTerminatingfunkcji „rozpakowuje” funkcja z jego argumentów i jabłka do oryginalnego argumentu. Ważne jest tutaj to, że większość systemów typów nie zezwala na przekazywanie funkcji do siebie, więc termin typu „ f fnie będzie sprawdzania typów”, ponieważ nie ma typu, fktóry mógłby zaspokoić funkcję sprawdzania typu. Jednym z powodów, dla których wprowadzono systemy typu, jest wyłączenie samowystarczalności (patrz tutaj ).

Zawijanie typów danych, takich jak ten, który wprowadziliśmy powyżej, można wykorzystać do obejścia tej blokady na drodze do niespójności.

Chcę dodać, że obliczenia nie kończące się wprowadzają niespójności do systemów logicznych. W przypadku Agdy i Coq Falseindukcyjny typ danych nie ma żadnych konstruktorów, więc nigdy nie można zbudować terminu próbnego typu False. Ale jeśli dozwolone byłyby obliczenia nie kończące się, można to zrobić na przykład w ten sposób (w Coq):

Fixpoint loop (n : nat) : False = loop n

Następnie loop 0sprawdzanie typu loop 0 : False, więc w korespondencji Curry-Howarda oznaczałoby to, że okazaliśmy się fałszywą propozycją.

Wynik : ścisła reguła pozytywności dla definicji indukcyjnych zapobiega niekończącym się obliczeniom, które są katastrofalne dla logiki.