Nowy wstęp do rozdziału o W-typach (TODO)

W-typy (TODO)

W-typy (ang. W-types) to typy dobrze ufundowanych drzew (ang. well-founded trees - W to skrót od well-founded), tzn. skończonych drzew o niemal dowolnych kształtach wyznaczanych przez parametry A i B. Nie są one zbyt przydatne w praktyce, gdyż wszystko, co można za ich pomocą osiągnąć, można też osiągnąć bez nich zwykłymi typami induktywnymi i będzie to dużo bardziej czytelne oraz prostsze w implementacji. Ba! W-typy są nawet nieco słabsze, gdyż go udowodnienia reguły indukcji wymagają aksjomatu ekstensjonalności dla funkcji. Jednak z tego samego powodu są bardzo ciekawe pod względem teoretycznym - wszystko, co można zrobić za pomocą parametryzowanych typów induktywnych, można też zrobić za pomocą samych W-typów. Dzięki temu możemy badanie parametryzowanych typów induktywnych, których jest mniej więcej nieskończoność i jeszcze trochę, sprowadzić do badania jednego tylko W (o ile godzimy się na aksjomat ekstensjonalności dla funkcji). Zanim jednak zobaczymy przykłady ich wykorzystania, zastanówmy się przez kilka chwil, dlaczego są one tak ogólne. Sprawa jest dość prosta. Rozważmy typ induktywny T i dowolny z jego konstruktorów c : X1 -> ... -> Xn -> T. Argumenty Xi możemy podzielić na dwie grupy: argumenty nieindukcyjne (oznaczmy je literą A) oraz indukcyjne (które są postaci T). Wobec tego typ c możemy zapisać jako c : A1 -> ... -> Ak -> T -> ... -> T -> T. W kolejnym kroku łączymy argumenty za pomocą produktu: niech A := A1 * ... * Ak. Wtedy typ c wygląda tak: c : A -> T * ... * T -> T. Zauważmy, że T * ... * T możemy zapisać równoważnie jako B -> T, gdzie B to typ mający tyle elementów, ile razy T występuje w produkcie T * ... * T. Zatem typ c przedstawia się tak: c : A -> (B -> T) -> T. Teraz poczynimy kilka uogólnień. Po pierwsze, na początku założyliśmy, że c ma skończenie wiele argumentów indukcyjnych, ale postać B -> T uwzględnia także przypadek, gdy jest ich nieskończenie wiele (tzn. gdy c miał oryginalnie jakiś argument postaci Y -> T dla nieskończonego Y). Po drugie, założyliśmy, że c jest funkcją niezależną. Przypadek, gdy c jest funkcją zależną możemy pokryć, pozwalając naszemu B zależeć od A, tzn. B : A -> Type. Typ konstruktora c zyskuje wtedy postać sumy zależnej {x : A & B x -> T} -> T. W ostatnim kroku odpakowujemy sumę i c zyskuje postać c : forall x : A, B x -> T. Jak więc widać, typ każdego konstruktora można przekształcić tak, żeby móc zapisać go jako forall x : A, B x -> T. Zauważmy też, że jeżeli mamy dwa konstruktory c1 : forall x : A1, B1 x -> T oraz c2 : forall x : A2, B2 x -> T, to możemy równie dobrze zapisać je za pomocą jednego konstruktora c: niech A := A1 + A2 i niech B (inl a1) := B1 a1, B (inl a2) := B2 a2. Wtedy konstruktory c1 i c2 są równoważne konstruktorowi c. Stosując powyższe przekształcenia możemy sprowadzić każdy typ induktywny do równoważnej postaci z jednym konstruktorem o typie forall x : A, B x -> T. Skoro tak, to definiujemy nowy typ, w którym A i B są parametrami... i bum, tak właśnie powstało W! Podejrzewam, że powyższy opis przyprawia cię o niemały ból głowy. Rzućmy więc okiem na przykład, który powinien być wystarczająco ogólny, żeby wszystko stało się jasne.

Spróbujmy zastosować powyższe przekształcenia na typie list X, żeby otrzymać reprezentację list za pomocą W. Zajmijmy się najpierw konstruktorem nil. Nie ma on ani argumentów indukcyjnych, ani nieindukcyjnych, co zdaje się nie pasować do naszej ogólnej metody. Jest to jednak jedynie złudzenie: brak argumentów nieindukcyjnych możemy zareprezentować za pomocą argumenu o typie unit, zaś brak argumentów indukcyjnych możemy zareprezentować argumentem o typie False -> list X. Wobec tego typ konstruktora nil możemy zapisać jako unit -> (False -> list X) -> list X. Dla consa jest już prościej: argument nieindukcyjny to po prostu X, zaś jeden argument indukcyjny możemy przedstawić jako unit -> list X. Nowy typ consa możemy zapisać jako X -> (unit -> list X) -> list X. Pozostaje nam skleić obydwa konstruktory w jeden. Niech A := unit + X i niech B (inl tt) := False, B (inr x) := unit. W ten sposób dostajemy poniższe kodowanie list za pomocą W (oczywiście nie jest to jedyne możliwe kodowanie - równie dobrze zamiast unit + X moglibyśmy użyć typu option X).

Wartą zauważenia różnicą konceptualną jest to, że jeżeli myślimy Coqowymi typami induktywnymi, to list ma dwa konstruktory - nil i cons, ale gdy myślimy za pomocą W, to sprawa ma się inaczej. Formalnie listW ma jeden konstruktor sup, ale w praktyce jest aż 1 + |X| konstruktorów, gdzie |X| oznacza liczbę elementów typu X. Jeden z nich opdowiada nil, a każdy z pozostałych |X| konstruktorów odpowiada cons x dla pewnego x : X. Jedyną pozostałością po oryginalnej liczbie konstruktorów jest liczba składników, które pojawiają się w sumie unit + X. Oczywiście posługiwanie się nil i cons jest dużo wygodniejsze niż używanie sup, więc czas odzyskać utracone konstruktory!

Zauważ, że consW jest jedynie jednym z wielu możliwych kodowań konstruktora cons. Inaczej możemy go zakodować np. tak:

Kodowania te nie są konwertowalne, ale jeżeli użyjemy aksjomatu ekstensjonalności dla funkcji, to możemy pokazać, że są równe.

Podobnym mykiem musimy posłużyć się, żeby udowodnić regułę indukcji. Dowód zaczynamy od indukcji po l (musimy pamiętać, że nasze W jest typem induktywnym, więc ma regułę indukcji), ale nie możemy bezpośrednio użyć hipotez PnilW ani PconsW, gdyż dotyczą one innych kodowań nil i cons niż te, które pojawiają się w celu. Żeby uporać się z problemem, używamy taktyki replace, a następnie dowodzimy, że obydwa kodowania są ekstensjoalnie równe.

Skoro mamy regułę indukcji, to bez problemu jesteśmy w stanie pokazać, że typy list X oraz listW X są izomorficzne, tzn. istnieją funkcje f : list X -> listW X oraz g : listW X -> list X, które są swoimi odwrotnościami.

Ćwiczenie

Napisałem we wstępie, że W-typy umożliwiają reprezentowanie dowolnych typów induktywnych, ale czy to prawda? Przekonajmy się! Zdefiniuj za pomocą W następujące typy i udowodnij, że są one izomorficzne z ich odpowiednikami:

• False (czyli Empty_set)
• unit
• bool
• typ o n elementach
• liczby naturalne
• produkt
• sumę

Załóżmy teraz, że żyjemy w świecie, w którym nie ma typów induktywnych. Jakich typów, oprócz W, potrzebujemy, by móc zdefiniować wszystkie powyższe typy?

Indeksowane W-typy (TODO)

Jak głosi pewna stara książka z Palestyny, nie samymi W-typami żyje człowiek. W szczególności, W-typy mogą uchwycić jedynie dość proste typy induktywne, czyli takie, które wspierają jedynie parametry oraz argumenty indukcyjne. Na chwilę obecną wydaje mi się też, że W nie jest w stanie reprezentować typów wzajemnie induktywnych, lecz pewny nie jest jestem. Trochę to smutne, gdyż naszą główną motywacją ku poznawaniu W-typów jest teoretyczne zrozumienie mechanizmu działania typów induktywnych, a skoro W jest biedne, to nie możemy za jego pomocą zrozumieć wszystkich typów induktywnych. Jednak uszy do góry, gdyż na ratunek w naszej misji przychodzą nam indeksowane W-typy! Co to za zwierzę, te indeksowane W-typy? Ano coś prawie jak oryginalne W, ale trochę na sterydach. Definicja wygląda tak:

Prawdopodobnie odczuwasz w tej chwili wielką grozę, co najmniej jakbyś zobaczył samego Cthulhu. Nie martw się - zaraz dokładnie wyjasnimy, co tu się dzieje, a potem rozpracujemy indeksowane W typy na przykładach rodzin typów induktywnych, które powinieneś już dobrze znać. Objaśnienia:

• I : Type to typ indeksów
• S i to typ kształtów o indeksie i. Kształt to konstruktor wraz ze swoimi argumentami nieindukcyjnymi.
• P s to typ mówiący, ile jest argumentów indukcyjnych o kształcie s.
• r p mówi, jak jest indeks argumentu indukcyjnego p.

Konstruktor isup mówi, że jeżeli mamy indeks i kształt dla tego indeksu, to jeżeli uda nam się zapchać wszystkie argumenty indukcyjne rzeczami o odpowiednim indeksie, to dostajemy element IW ... o takim indeksie jak chcieliśmy. Czas na przykład:

Na pierwszy ogień idzie Vec, czyli listy indeksowane długością. Jak wygląda jego reprezentacja za pomocą IW?

Przede wszystkim musimy zauważyć, że typem indeksów I jest nat.

Typ kształtów definiujemy przez dopasowanie indeksu do wzorca, bo dla różnych indeksów mamy różne możliwe kształty. Konstruktor vnil jest jedynym konstruktorem o indeksie 0 i nie bierze on żadnych argumentów nieindukcyjnych, stąd w powyższej definicji klauzula | 0 => unit. Konstruktor vcons jest jedynym konstruktorem o indeksie niezerowym i niezależnie od indeksu bierze on jeden argument nieindukcyjny typu A, stąd klauzula | S _ => A.

Typ pozycji różwnież definiujemy przez dopasowanie indeksu do wzorca, bo różne kształty będą miały różne pozycje, a przecież kształty też są zdefiniowane przez dopasowanie indeksu. Konstruktor vnil nie bierze argumentów indukcyjnych i stąd klauzula | 0 => False. Konstruktor vcons bierze jeden argument indukcyjny i stąd klauzula | S _ => unit. Zauważmy, że niebranie argumentu nieindukcyjnego reprezentujemy inaczej niż niebranie argumentu indukcyjnego. vnil nie bierze argumentów nieindukcyjnych, co w typie kształtów S_Vec reprezentujemy za pomocą typu unit. Możemy myśleć o tym tak, że vnil bierze jeden argument typu unit. Ponieważ unit ma tylko jeden element, to i tak z góry wiadomo, że będziemy musieli jako ten argument wstawić tt. vnil nie bierze też argumentów indukcyjnych, co w typue pozycji P_Vec reprezentujemy za pomocą typu False. Możemy myśleć o tym tak, że jest tyle samo argumentów indukcyjnych, co dowodów False, czyli zero. Podsumowując, różnica jest taka, że dla argumentów nieindukcyjnych typ X oznacza "weź element typu X", zaś dla argumentów indukcyjnych typ X oznacza "weź tyle elementów typu, który właśnie definiujemy, ile jest elementów typu X".

Pozostaje nam tylko zdefiniować funkcję, która pozycjom argumentów indukcyjnym w poszczególnych kształtach przyporządkowuje ich indeksy. Definiujemy tę funkcję przez dowód, gdyż Coq dość słabo rodzi sobie z dopasowaniem do wzorca przy typach zależnych. Ponieważ kształty są zdefiniowane przez dopasowanie indeksu do wzorca, to zaczynamy od rozbicia indeksu na przypadki. Gdy indeks wynosi zero, to mamy do czynienia z reprezentacją konstruktora vnil, który nie bierze żadnych argumentów indukcyjnych, co ujawnia się pod postacią sprzeczności. Gdy indeks wynosi S i', mamy do czynienia z konstruktorem vcons i', który tworzy element typu Vec A (S i'), zaś bierze element typu Vec A i'. Wobec tego w tym przypadku zwracamy i'.

Tak wygląda ostateczna definicja Vec' - wrzucamy do IW odpowiednie indeksy, kształty, pozycje oraz funkcję przypisującą indeksy pozycjom. Spróbujmy przekonać się, że typy Vec A n oraz Vec' A n są izomorficzne. W tym celu musimy zdefiniować funkcje f : Vec A n -> Vec' A n oraz g : Vec' A n -> Vec A n, które są swoimi odwrotnościami.

Najłatwiej definiować nam będzie za pomocą taktyk. Definicja f idzie przez rekursję strukturalną po v. isup 0 tt to reprezentacja vnil, zaś @isup _ _ _ (@r_Vec A) (S n) a to reprezentacja vcons a. Dość nieczytelne, prawda? Dlatego właśnie nikt w praktyce nie używa indeksowanych W-typów.

W drugą stronę jest łatwiej. Definicja idzie oczywiście przez rekursję po v (pamiętajmy, że Vec' A n to tylko specjalny przypadek IW, zaś IW jest induktywne). Po rozbiciu v na komponenty sprawdzamy, jaki ma ono indeks. Jeżeli 0, zwracamy vnil. Jeżeli niezerowy, to zwracamy vcons z głową s rekurencyjnie obliczonym ogonem.

Dowód odwrotności w jedną stronę jest banalny - indukcja po v idzie gładko, bo v jest typu Vec A n.

W drugę stronę dowód jest nieco trudniejszy. Przede wszystkim, musimy posłużyć się aksjomatem ekstensjonalności dla funkcji. Wynika to z faktu, że w IW reprezentujemy argumenty indukcyjne wszystkie na raz za pomocą pojedynczej funkcji. Zaczynamy przez indukcję po v i rozbijamy indeks żeby sprawdzić, z którym kształtem mamy do czynienia. Kluczowym krokime jest odwinięcie definicji I_Vec - bez tego taktyka f_equal nie zadziała tak jak powinna. W obu przypadkach kończymy przez użycie ekstensjonalności do udowodnienia, że argumenty indukcyjne są równe.

Ćwiczenie

Zdefiniuj za pomocą IW następujące predykaty/relacje/rodziny typów:

• even i odd
• typ drzew binarnych trzymających wartości w węzłach, indeksowany wysokością
• to samo co wyżej, ale indeksowany ilością elementów
• porządek <= dla liczb naturalnych
• relację Perm : list A -> list A -> Prop mówiącą, że l1 i l2 są swoimi permutacjami

M-typy (TODO)

M-typy to to samo co W-typy, tylko że dualne. Pozdro dla kumatych.

Naszą motywacją do badania W-typów było to, że są one jedynym pierścieniem (w sensie Władcy Pierścieni, a nie algebry abstrakcyjnej), tj. pozwalają uchwycić wszystkie typy induktywne za pomocą jednego (oczywiście o ile mamy też False, unit, bool, prod i sum). Podobnie możemy postawić sobie zadanie zbadania wszystkich typów koinduktywnych. Rozwiązanie zadania jest (zupełnie nieprzypadkowo) analogiczne do tego dla typów induktywnych, a są nim M-typy. Skąd nazwa? Zauważ, że M to nic innego jak W postawione na głowie - podobnie esencja M-typów jest taka sama jak W-typów, ale interpretacja jest postawiona na głowie.

Zastanówmy się przez chwilę, dlaczego definicja M wygląda właśnie tak. W tym celu rozważmy dowolny typ koinduktywny C i przyjmijmy, że ma on pola f1 : X1, ..., fn : Xn. Argumenty możemy podzielić na dwie grupy: koindukcyjne (których typem jest C lub funkcje postaci B -> C) oraz niekoindukcyjne (oznaczmy ich typy przez A). Oczywiście wszystkie niekoindukcyjne pola o typach A1, ..., Ak możemy połączyć w jedno wielgachne pole o typie A1 * ... * Ak i tym właśnie jest występujące w M pole shape. Podobnie jak w przypadku W-typów, typ S będziemy nazywać typem kształtów. Pozostała nam jeszcze garść pól typu C (lub w nieco ogólniejszym przypadku, o typach B1 -> C, ..., Bn -> C. Nie trudno zauważyć, że można połączyć je w typ B1 + ... + Bn -> C. Nie tłumaczy to jednak tego, że typ pozycji zależy od konkretnego kształtu. Źródeł można doszukiwać się w jeszcze jednej, nieco bardziej złożonej postaci destruktorów. Żeby za dużo nie mącić, rozważmy przykład. Niech C ma destruktor postaci nat -> C + nat. Jak dokodować ten destruktor do shape i position? Otóż dorzucamy do shape nowy komponent, czyli shape' := shape * nat -> option nat. A psu w dupę z tym wszystkim. TODO

Ciekawostka: koindukcja i bipodobieństwo

TODO: regułę koindukcji można rozłożyć na regułę korekursji oraz regułę unikalności, a reguła unikalności sama w sobie w zasadzie oznacza, że bipodobieństwo to równość.

Indeksowane M-typy? (TODO)

Nie dla psa kiełbajsa.