Mocna kontrola typów, cz.2


Metareguły
Wewnętrzny system typów
Atrybuty
Kontrola typologicza
Typy referencyjne
Metareguły wnioskowania o typie
Dla operatorów niealgebraicznych oraz niektórych algebraicznych, takich jak u, e itd. reguły przedstawione poprzednio muszą być uogólnione.
Operatory te działają na nieskończonej rodzinie sygnatur (są polimorficzne).
Przykładowo, dla operatorów where, kropka, join u odpowiednie metareguły mogą mieć postać:
rw
(T, T1, T2 są dowolnymi sygnaturami).
Takie metareguły mogą być bardzo zróżnicowane i ich opracowanie dla danego modelu składu, języka oraz systemu typów jest wyzwaniem.
W metaregułach może być wiele kombinacji sygnatur wejściowych, które warto wyróżnić, oraz wiele odpowiadających im wynikowych sygnatur.
Złożone metareguły
Metareguły wnioskowania o typie mogą przyjmować dość rozbudowaną postać.
Rozpatrzmy np. operator kropki w zapytaniu q1.q2.
Podane poprzednio wyjaśnienie semantyki ustala, że zarówno q1, jak i q2 muszą zwrócić bagi.
Tak oczywiście nie musi być, jeżeli nie chcemy zmuszać użytkownika do komplikowania zapytania poprzez wstawienie do niego explicite funkcji konwersji typów.
Typ wynikowy takiego zapytania zależy od wydedukowanych typów dla q1 oraz q2.
Zarówno q1, jak i q2 mogą zwrócić pojedynczy element, bag lub sekwencję.
Kombinacja tych przypadków daje 9 możliwości, które ułożymy w tabelę:
Metareguła - tabela wnioskowania o typie (dla .)
tabela
Komentarz do tabelki
W tabelce tej ustaliliśmy, że jeżeli q1 zwraca bag, zaś q2 zwraca sekwencję, to nie ma dobrego sposobu wyznaczenia ostatecznej sekwencji, zatem jest to błąd typologiczny.
Podobnie dla ustawienia sekwencja-bag.
To założenie można nieco złagodzić przyjmując przesunięcie kontroli typologicznej na czas wykonania.
Podobne tabelki można budować dla operatorów u, where, join, as, kwantyfikatorów itd.
Ich duża nieregularność, możliwość przesunięcia kontroli typologicznej na czas wykonania oraz arbitralność niektórych decyzji uzasadniają naszą niewiarę w skuteczność lub wręcz możliwość formalizacji mechanizmu mocnej kontroli typu.
W najlepszym razie system formalny byłby uwikłany w nużące szczegóły, które podważyłyby estetykę i elegancję, czyli cechy, które są podstawową przyczyną i bazą psychologiczną zainteresowania metodami formalnymi w informatyce.
Co to jest wewnętrzny system typów?
Wewnętrzny system typów jest to:
Graf schematu (podany uprzednio przy okazji optymalizacji)
Tabela reguł wnioskowania o typie dla operatorów monomorficznych (działających na jednym lub kilku typach), takich jak +;
Zestaw metareguł wnioskowania o typie dla operatorów polimorficznych (działających na nieskończonej rodzinie typów), takich jak  podana uprzednio tabela.
Na podstawie tych struktur oraz statycznych stosów S_ENVS i S_QRES procedura static_type_check, działając rekurencyjnie na drzewie syntaktycznym, jest w stanie wyprodukować listę błędów typologicznych.
Graf schematu - metabaza (przypomnienie)
graf
Procedura static_type_check
Z koncepcyjnego punktu widzenia jest prawie identyczna z procedurą static_eval prezentowanej poprzednio.
Obie działają na S_ENVS i S_QRES, identycznie zapełniają je sygnaturami i identycznie korzystają z reguł i metareguł wnioskowania o typie.
static_type_check wykonuje następujące operacje:
Kontroluje typologicznie drzewo syntaktyczne poprzez zasymulowanie na stosach S_ENVS i S_QRES działań mechanizmu ewaluacji zapytań.
Wyprowadza na zewnątrz komunikaty o błędach typologicznych.
Dokonuje zmian drzewa syntaktycznego w celu wprowadzenia tam operatorów automatycznej dereferencji oraz operatorów koercji.
Dokonuje zmian drzewa syntaktycznego w celu wprowadzenie do niego operatorów dynamicznej kontroli typologicznej.
Po wykryciu i zakomunikowaniu błędu typologicznego dokonuje naprawy drzewa syntaktycznego i/lub stosów statycznych, aby umożliwić wykrycie więcej niż jednego błędu typologicznego w ramach jednego przebiegu sprawdzania kodu.
Procedura static_type_check powinna być uruchomiona wcześniej niż static_eval.
Uruchomienie procedury static_type_check
Procedura działa na drzewie syntaktycznym zapytania i jest zdefiniowana w sposób rekurencyjny.
Przed uruchomieniem procedury stos S_ENVS musi posiadać statyczną sekcję bazową, zawierającą statyczne bindery do wszystkich startowych (korzeniowych) węzłów metabazy:
np. dla podanej metabazy sygnatury
syg
Jeżeli środowisko ewaluacyjne zawiera więcej sekcji bazowych, wówczas każde z nich musi być odwzorowane przez sekcję ze statycznymi binderami startowymi.
Postać procedury static_type_check (1)
procedura
Postać procedury static_type_check (2)
procedura
Postać procedury static_type_check (3)
procedura
Komentarz do static_type_check
Powyższy pseudokod należy traktować jako zgrubny sposób postępowania.
Konkretny algorytm zależy od przyjętego modelu składu obiektów, przyjętego zewnętrznego i wewnętrznego systemu typów, przyjętych założeń odnośnie do elips i automatycznych koercji itd.
W przypadku każdego operatora (algebraicznego lub niealgebraicznego) należy bardzo dokładnie:
rozpatrzyć możliwą postać jego argumentów (sygnatur),
ustalić poprawność lub niepoprawność typologiczną,
wyznaczyć wynikową sygnaturę,
wyznaczyć najbardziej odpowiedni sygnał błędu typologicznego
wyznaczyć sposób naprawy drzewa syntaktycznego i/lub wynikowej sygnatury.
Należy oczekiwać, że algorytm ten będzie uwikłany w dużą liczbę dość arbitralnych decyzji koncepcyjnych i implementacyjnych.
Uwzględnienie atrybutów sygnatur
Kontrola typologiczna może dotyczyć kilku cech, które nie zostały dotąd uwzględnione w konstrukcji sygnatur i regułach wnioskowania o typie.
Takie cechy będziemy nazywać atrybutami sygnatur.
Atrybuty sygnatur uczestniczą w procesie wnioskowania o typie:
Mutowalność (mutability) - atrybut określa, czy odpowiednia wartość czasu wykonania jest referencją do aktualizowalnego obiektu.
Liczność (cardinality) - atrybut określa, ilu wartości odpowiadających danej sygnaturze należy oczekiwać podczas czasu wykonania.
Przyjmuje wartość z 5-cio elementowej skali 0, 1, [0..1], [0..*], [1..*] .
Rodzaj kolekcji - atrybut może przyjmować wartość element, bag, sequence, array lub inny.
Nazwa typu - atrybut przyjmuje wartość będącą nazwą typu danego specyfikowanego bytu programistycznego.
Wartość atrybutu jest określona (niejawnie) w grafie schematu lub wynika z deklaracji parametru procedury.
Możliwe są dalsze atrybuty sygnatur.
Atrybut mutowalności
Ustala, czy byt o danej sygnaturze można zastosować w konstrukcjach, w których oczekiwana jest referencja.
Jest ona oczekiwana w zdaniach imperatywnych update (z lewej strony podstawienia) insert i delete oraz w przypadku parametru procedury, funkcji lub metody wołanego przez referencję.
Wartość atrybutu true oznacza więc automatycznie, że odpowiednia sygnatura ma postać identyfikatora węzła grafu schematu (i odwrotnie)..
Atrybut mutowalności przyjmuje wartość true w momencie wiązania nazwy do statycznego bindera wskazującego na węzeł grafu schematu.
Sygnatura zmienia atrybut mutowalności na false, po dereferencji.
Jeżeli dla sygnatury lewej strony operatora podstawienia (update) wartość atrybutu mutowalności jest false, to należy zasygnalizować błąd typologiczny.
Podobnie dla operatorów wstawiania i usuwania.
Atrybut mutowalności jest również podstawą wstawienia do drzewa syntaktycznego operatorów dereferencji.
Atrybut liczności
Pozwala ustalić w wystarczającym przybliżeniu, jaka będzie liczność wartości zwracanych przez dane zapytanie.
Dotychczas atrybut ten pojawiał się w podanych wyżej przykładach sygnatur w postaci słowa kluczowego bag. Taka kwalifikacja jest równoważna atrybutowi liczności [0..*] i może być zastąpiona przez tę liczność.
Inne wartości liczności mogą również służyć do wnioskowania o poprawności typologicznej, np. wartość [0..1].
Znajomość tego atrybutu może być niezbędna dla pewnych optymalizacji, np. usuwania martwych podzapytań.
Znajomość ta może być również konieczna dla prawidłowego przebiegu kontroli typologicznej.
W szczególności, umożliwia wstawienie do drzewa syntaktycznego operatorów koercji z bagu do pojedynczego elementu lub odwrotnie.
Dla dowolnych operatorów algebraicznych i niealgebraicznych należy przewidzieć wykorzystanie tego atrybutu do sygnalizacji błędu typologicznego, koercji i/lub dynamicznej kontroli typologicznej.
Atrybut rodzaju kolekcji
Atrybut rodzaju kolekcji był dotychczas zaznaczany przez nas w sygnaturach słowem bag lub sequence (lub brakiem tych kwalifikatorów).
Atrybut ten może ulegać zmianie w wyniku działania pewnych operatorów, np. operator order by zmienia bag na sekwencję.
Niektóre operatory są właściwe tylko dla sekwencji, np. konkatenacja lub odzyskanie i-tego elementu, wobec czego ten atrybut może być także podstawą sygnalizacji błędu typologicznego.
Atrybut nazwy typu
Atrybut nazwy typu jest istotny w przypadku, gdy decydujemy się na nazwową zgodność typu.
Atrybut pozwala przypisać nazwę typu do danej sygnatury, co umożliwia sprawdzenie, czy wyliczona sygnatura jest zgodna z oczekiwaną.
Np. jeżeli mamy definicję o postaci:
typedef TypPesel -> int;
wówczas deklaracja atrybutu obiektu w postaci:
NrPesel: TypPesel;
oznacza, że do sygnatury NrPesel(iNrPesel) zostaje przypisany atrybut nazwy typu TypPesel.
Atrybut ten może być sprawdzany w sytuacji, gdy procedura ma zadeklarowany parametr formalny x typu TypPesel, zaś przy wywołaniu na x podstawia się pewne zapytanie q.
Jeżeli wyliczona sygnatura q nie ma atrybutu nazwy typu TypPesel, wówczas jest to błąd typologiczny.
Trudności z nazwową zgodnością typu
Przyjęcie nazwowej zgodności typu wiąże się z trudnością dotyczącą operatorów jawnie lub niejawnie przypisanymi do typu.
Pascal przyjmuje, że w ten sposób nowo zdefiniowany typ dziedziczy wszystkie operatory z jego definicji, np. TypPesel dziedziczy z int.
W ten sposób na wartościach typu TypPesel można wykonywać operacje +, -, *, /, co nie ma sensu.
Jedynym sposobem usunięcia tej niedogodności jest specjalna składnia definicji typu, w której podaje się operatory dziedziczone do danego typu.
Użycie operatorów, które nie są odziedziczone, oznacza błąd typologiczny.
Nowe operatory dla nowo zdefiniowanego typu mogą być określone przez napisanie funkcji posiadających ten typ jako argument.
Zgodność nazwowa implikuje także problem z dziedziczeniem i zasadą zastępowania (substitutability). Podtrzymanie tej zasady można jednak łatwo uzyskać.
Czy mocna kontrola typów musi być taka mocna?
Wyznawcy ortodoksyjnej statycznej kontroli typologicznej twierdzą, że programista jest zobowiązany do takiego sformułowania programów, aby typy były zawsze zgodne.
Instrumentem do tego są różnorodne operatory zmiany typu, takie jak operatory rzutowania (cast).
Odstępstwa od tej reguły, polegające na automatycznym stosowaniu operatorów koercji, są uważane za własność marginalną nieco negatywną.
Ten stereotyp mocnej kontroli typów zdominował myślenie o typach jako o technice formalistycznego wymuszania bardzo regularnych formatów.
Przykładem takiego myślenia jest standard ODMG 3.0, który z nabożeństwem traktuje konieczność określania przez programistów operatorów zmiany typu, np. zmianę bagu na wartość będącą elementem tego bagu.
Podobnie, twórcy modeli danych określanych jako półstrukturalne (semi-structured), których przypadkiem jest XML, przyjmują niekiedy, że są to systemy beztypowe (typeless) lub bezschematowe (schemaless).
Dominuje pogląd, że skoro modele te operują na nieregularnych danych, to mocna statyczna kontrola typologiczna jest dla nich niemożliwa.
Wady formalistycznej kontroli typologicznej
Odmienne stanowisko zajmują twórcy języków nie posiadających mocnej kontroli typologicznej lub posiadające wyłącznie kontrolę dynamiczną, takich jak SQL.
W językach tych przyjmuje się koercje, czyli automatyczne zmiany typów jako oczywiste.
Np. "oficjalnie" zdanie select języka SQL zwraca tabelę, czyli kolekcję wartości, ale "nieoficjalnie" takie zdanie można zanurzyć w klauzulę where i wtedy takie zdanie zwraca nie tabelę, ale pojedynczą wartość.
Wadą formalistycznej kontroli typologicznej jest obciążenie kodu zapytania lub programu przez techniczny folklor utrudniający modelowanie pojęciowe i szybkie rozumienie semantyki zapytania.
Pewne znaczenie ma także ponowne użycie i ewolucja schematu bazy danych: niektóre zapytania nie muszą się zmieniać, mimo zmian typów uczestniczących w nich bytów programistycznych.
Koercje i dynamiczna kontrola typologiczna
Bardzo rygorystyczne i formalistyczne traktowanie mocnej kontroli typów, lub odwrotnie, całkowity brak kontroli typów nie są jedynymi stanami.
Mocną kontrolę typologiczną można stosować do bardzo rozluźnionych formatów, w których występują dane opcyjne (liczność [0..1]), dane powtarzalne (liczność [0..*] lub [1..*]) oraz warianty.
W takich przypadkach kontrola typologiczna powinna uwzględniać automatyczne koercje oraz dynamiczne kontrole typów,
Techniką implementacyjną dla automatycznych koercji i dynamicznych kontroli typów jest wstawianie do drzewa syntaktycznego węzłów, w efekcie których nastąpi zmiana typu i/lub dynamiczna kontrola typologicznej.
Mocna kontrola typologiczna nie polega więc na trzymaniu się rygorystycznych schematów formalnych.
Nie jest teoretyczną bądź estetyczną "sztuką dla sztuki".
Nie ma sensu z przyczyn formalnych komplikować życia programisty, jeżeli zagrożenie błędem jest minimalne i kiedy jawne koercje bardzo zamulają kod zapytania/programu.
Rozluźniona kontrola typologiczna
Dowolny formalnie wymyślony system kontroli typologicznej może nie spełnić swojej roli, o ile nie uwzględni faktu, że tylko programista, wraz z jego psychologią, przyzwyczajeniami i predyspozycjami, jest adresatem mocnej kontroli typów.
Znaczne usztywnienie systemu typów oznacza większą uciążliwość przy pisaniu programów oraz dłuższy i mniej czytelny kod.
Mocna kontrola typologiczna tak czy inaczej nie jest w stanie wykryć wszystkich błędów, które programista może popełnić.
Jeżeli nieco luźniejszy, ale przyjazny dla programisty mechanizm kontroli typologicznej wykryje np. 80% wszystkich popełnianych przez niego błędów, zaś bardzo sztywny i nieprzyjazny wykryje 81%, to ten drugi nie ma sensu.
Nie jest więc konieczne traktowanie np. zapytania o sygnaturze wejściowej string + int jako błędu typologicznego.
Jeżeli odpowiada to naszemu wyczuciu zachowania się programisty, możemy wstawić do drzewa syntaktycznego operator zmiany stringu na int i dynamicznie sprawdzać poprawności tej operacji.
Nie ma istotnych problemów technicznych lub koncepcyjnych z uwzględnieniem tego rodzaju własności w mechanizmie mocnej kontroli typologicznej.
Przykłady koercji
koercji
Kontrola operatorów imperatywnych
Przykładami takiej kontroli są operatory if oraz while, dla których wynikowa sygnatura zapytania będącego argumentem tego operatora powinna być bool.
Są to łatwe przypadki.
Trudniejszym przypadkiem jest operator podstawienia.
Dla niego sygnatura lewej strony powinna mieć atrybut mutowalności o wartości true.
Sygnatury prawej i lewej strony podstawienia powinny być zgodne.
W przypadku danych złożonych operacja podstawienia jest trudniejsza i może przyjmować wiele wariantów semantycznych.
Przykładowo, można przyjąć, że podstawienie jest możliwie tylko w przypadku, gdy sygnatury lewej i prawej strony podstawienia mają identyczny atrybut nazwy typu. -> Oznacza to zgodność nazwową.
Przy zastosowaniu zgodności strukturalnej problem jest prosty, o ile sygnatura prawej i lewej strony jest identyczna (co oznacza, że obie są referencjami do tego samego węzła grafu schematu).
W pozostałych przypadkach powstaje np. pytanie, czy na obiekt Prac można podstawiać obiekt Osoba, lub odwrotnie, i jakie miałoby to skutki?
Podobne problemy należy rozstrzygnąć dla innych operatorów imperatywnych.
Kontrola procedur - kontrola ciała
Kontrola typologiczna procedur (do których zaliczamy także funkcje, metody i perspektywy) występuje w dwóch postaciach: kontrola ciała procedur i kontrola wywołania procedur. Te kontrole są od siebie niezależne.
Kontrola ciała procedur odbywa się na podanych wcześniej zasadach.
Pierwszym krokiem jest zbudowanie grafu schematu dla lokalnych obiektów.
Różnicą w stosunku do poprzednio wyjaśnionego mechanizmu jest pojawienie się statycznych binderów nazwaParametru(nazwaTypu) lub nazwaParametru(idWęzła). Pierwszy binder pojawia się w przypadku wołania przez wartość, drugi w przypadku wołania przez referencję.
Nazwa nazwaParametru jest nazwą parametru umieszczoną w deklaracji procedury.
W przypadku strukturalnej zgodności typów pierwszy binder powinien być rozwinięty do pełnej postaci poprzez usunięcie nazw typów.
Drugi binder ustala identyfikator węzła grafu schematu. Może on jednak odnosić się do węzła dowolnego grafu schematu, np. bazy danych lub modułu.
Kontrola rozpoczyna się od wstawienia na wierzchołek S_ENVS nowej sekcji (statycznego zapisu aktywacyjnego) zawierającej wszystkie ww. statyczne bindery parametrów oraz bindery do wszystkich węzłów korzeniowych lokalnego grafu schematu.
Po zakończeniu sprawdzania danej procedury sekcja ta jest usuwana.
Kontrola procedur - kontrola parametrów
Kontrola parametrów procedury polega na porównaniu zadeklarowanej sygnatury parametru formalnego (z uwzględnieniem atrybutu mutowalności) z wyliczoną sygnaturą zapytania będącego aktualnym parametrem.
W przypadku zgodności nazwowej wystarczy porównać atrybuty nazwy typu na identyczność. Jeżeli nie są identyczne, należy sygnalizować błąd typu.
Porównanie wartości atrybutu nazwy typu może uwzględnić związki dziedziczenia .
W przypadku zgodności strukturalnej problem jest bardziej złożony.
Łatwy przypadek występuje wtedy, gdy obydwie sygnatury są tym samym typem elementarnym lub tym samym identyfikatorem węzła grafu schematu.
Trudniejszy przypadek dotyczy sytuacji, gdy porównywanie sygnatur musi być rekurencyjne, zgodnie z ich hierarchiczną budową.
Idea tej kontroli wydaje się jasna od strony koncepcyjnej, ale rozstrzygnięcie wszystkich szczegółów może być problemem.
Typy referencyjne
Rozważmy następującą deklarację typu:
typ
Jeżeli potraktujemy tę definicję z punktu widzenia logiki, to mamy do czynienia z dość podejrzaną rekurencją: TypOsoba jest definiowany poprzez TypOsoba.
W takich przypadkach logicy mówią, że mamy do czynienia nie z rekurencją, lecz z błędem logicznym ignotum per ignotum, czyli definiowanie nieznanego pojęcia przez nieznane pojęcia.
Z drugiej strony, okazuje się, że takie definicje są bardzo powszechne w językach obiektowych, całkowicie zrozumiałe z praktycznego punktu widzenia i w pełni implementowalne.
Czy może być implementowalne coś, co jest logicznie sprzeczne?
Wyjaśnienie sprzeczności
Nie ma żadnej sprzeczności.
Wymienione na poprzednim slajdzie typy takie jak
Dziecko: TypOsoba [0..*]
są po prostu typami referencyjnymi.
W takich deklaracjach obowiązują niepisane umowy:
Typ taki jak TypOsoba deklaruje nie obiekt typu Osoba, lecz referencję do obiektów typu Osoba
Dodatkowo przyjmuje się, że referencje takie muszą prowadzić do obiektów o nazwie Osoba.
Konsekwencja tych dwóch umów są takie, że deklaracja typedef, taka jak na poprzednim slajdzie, nie może mieć samodzielnego bytu semantycznego.
Jest tylko napisem.
Przy tych założeniach można zbudować normalny graf schematu, taki jak na następnym slajdzie.
Graf schematu powstały z deklaracji typu
Deklaracja:
Osoba: TypOsoba[0..*]

graf
pokaż animację