Typy zależne, czyli typowanie statyczne na sterydach

Uniwersum (TODO)

Funkcje zależne (TODO)

Pary zależne i podtypy (TODO)

W Coqu, w przeciwieństwie do wielu języków imperatywnych, nie ma mechanizmu podtypowania, a każde dwa typy są ze sobą rozłączne. Nie jest to problemem, gdyż podtypowanie możemy zasymulować za pomocą sum zależnych, a te zdefiniować możemy induktywnie.

Typ sigT reprezentuje sumę zależną, której elementami są pary zależne. Pierwszym elementem pary jest x, który jest typu A, zaś drugim elementem pary jest term typu P x. Suma zależna jest wobec tego pewnym uogólnieniem produktu. Niech cię nie zmyli nazewnictwo:

• Suma jest reprezentowana przez typ sum A B. Jej elementami są elementy A zawinięte w konstruktor inl oraz elementy B zawinięte w konstruktor inr. Reprezentuje ideę "lub/albo". Typ B nie może zależeć od typu A.
• Produkt jest reprezentowany przez typ prod A B. Jego elementami są pary elementów A i B. Reprezentuje on ideę "i/oraz". Typ B nie może zależeć od typu A.
• Uogólnieniem produktu jest suma zależna. Jest ona reprezentowana przez typ sigT A P. Jej elementami są pary zależne elementów A i P x, gdzie x : A jest pierwszym elementem pary. Reprezentuje ona ideę "i/oraz", gdzie typ P x może zależeć od elementu x typu A.
• Typ funkcji jest reprezentowany przez A -> B. Jego elementami są termy postaci fun x : A => .... Reprezentują ideę "daj mi coś typu A, a ja oddam ci coś typu B". Typ B nie może zależeć od typu A.
• Uogólnieniem typu funkcji jest produkt zależny forall x : A, B x. Jego elementami są termu postaci fun x : A => .... Reprezentuje on ideę "daj mi x typu A, a ja oddam ci coś typu B x". Typ B x może zależeć od typu elementu x typu A.

sigT jest najogólniejszą postacią pary zależnej — A jest typem, a P rodziną typów. Mimo swej ogólności jest używany dość rzadko, gdyż najbardziej przydatną postacią sumy zależnej jest typ sig:

Typ sig A P można interpretować jako typ składający się z tych elementów A, które spełniają predykat P. Formalnie jest to para zależna, której pierwszym elementem jest term typu A, zaś drugim dowód na to, że spełnia on predykat P.

Typ big_nat reprezentuje liczby naturalne większe lub równe 100, zaś term big_100 to liczba 100 wraz z załączonym dowodem faktu, że jest ona większa lub równa 100. Interpretacja typu sig sprawia, że jest on wykorzystywany bardzo często do podawania specyfikacji programów — pozwala on dodać do wyniku zwracanego przez funkcję informację o jego właściwościach. W przypadku argumentów raczej nie jest używany, gdyż prościej jest po prostu wymagać dowodów żądanych właściwości w osobnych argumentach niż pakować je w sig po to, żeby i tak zostały później odpakowane.

Definiowanie wartości typu sig jest problematyczne, gdyż zawierają one dowody. Napisanie definicji "ręcznie", explicité podając proofterm, nie wchodzi w grę. Innym potencjalnym rozwiązaniem jest napisanie dowodu na boku, a następnie użycie go we właściwej definicji, ale jest ono dłuższe niż to konieczne. Przypomnijmy sobie, czym są taktyki. Dowody to termy, których typy są sortu Prop, a taktyki służą do konstruowania tych dowodów. Ponieważ dowody nie różnią się (prawie) niczym od programów, taktyk można użyć także do pisania programów. Taktyki to metaprogramy (napisane w jęzku Ltac), które piszą programy (w jęzku termów Coqa, zwanym Gallina). Wobec tego trybu dowodzenia oraz taktyk możemy używać nie tylko do dowodzenia, ale także do definiowania i to właśnie uczyniliśmy w powyższym przykładzie. Skonstruowanie termu typu big_nat, czyli parzystej liczby naturalnej, odbyło się w następujący sposób. Naszym celem jest początkowo big_nat, czyli typ, którego element chcemy skonstrować. Używamy konstruktora exist, który w naszym przypadku jest typu forall x : nat, 100 <= n -> big_nat. Wobec tego exist 101 jest typu 100 <= 101 -> big_nat, a jego zaaplikowanie skutkować będzie zamianą naszego celu na 100 <= 101. Następnie dowodzimy tego faktu, co kończy proces definiowania.

Ćwiczenie

Zdefiniuj predykat sorted, który jest spełniony, gdy jego argument jest listą posortowaną. Następnie zdefiniuj typ list liczb naturalnych posortowanych według relacji <= i skonstruuj term tego typu odpowiadający liście [42; 666; 1337].

Indeksowane enumeracje (TODO)

Ostatnią poznaną przez nas innowacją są typy indeksowane. Tutaj również definiujemy za jednym zamachem (ekhem...) dużo typów, ale nie są one niezależne jak w przypadku parametrów, lecz mogą od siebie wzajemnie zależeć. Słowem, tak naprawdę definiujemy przez indukcję funkcję typu A_1 -> ... -> A_n -> Type/Prop, gdzie A_i to indeksy.

Możliwych reguł analizy przypadków mamy tutaj trochę więcej niż w przypadku parametrów. W powyższej regule P nie zależy od indeksu n : nat...

... a w powyższej tak. Jako, że indeksy zmieniają się pomiędzy konstruktorami, każdy z nich musi kwantyfikować je osobno (co akurat nie jest potrzebne w naszym przykładzie, gdyż jest zbyt prosty).

Ogólnie reguła jest taka: reguła niezależna (pierwsza) nie zależy od niczego, a zależna (trzecia) zależy od wszystkiego. Reguła druga jest pośrednia - ot, take ciepłe kluchy.

Rekordy zależne

Kwantyfikacja egzystencjalna (TODO)

Znamy już pary zależne i wiemy, że mogą służyć do reprezentowania podtypów, których w Coqu brak. Czas zatem uświadomić sobie kolejny fragment korespondencji Curry'ego-Howarda, a mianowicie definicję kwantyfikacji egzystencjalnej:

ex to kolejne wcielenie sumy zależnej. Porównaj dokładnie tę definicję z definicją sigT oraz sig. ex jest niemal identyczne jak sig: jest to para zależna, której pierwszym elementem jest term x : A, a drugim dowód na to, że P x zachodzi. ex jednak, w przeciwieństwie do sig, żyje w Prop, czyli jest zdaniem — nie liczą się konkretne postaci jego termów ani ich ilość, a jedynie fakt ich istnienia. To sprawia, że ex jest doskonałym kandydatem do reprezentowania kwantyfikacji egzystencjalnej.

Ćwiczenie

Udowodnij, że dla każdej liczby naturalnej n istnieje liczba od niej większa. Następnie zastanów się, jak działa taktyka exists.

Równość (TODO)

Równość a ścieżki