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 ,
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 i odpowiednie metareguły mogą mieć postać:
- (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 .)
-
- 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 , 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)
-
- 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
-
- 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)
-
- Postać procedury static_type_check (2)
-
- Postać procedury static_type_check (3)
-
- 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
-
- 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:
-
- 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..*]
-
pokaż animację