Mocna kontrola typów, cz.1


Po co są typy?
Co to jest system typów?
Typy a schematy baz danych
Strukturalna zgodność typów
Nazwowa zgodność typów
Pojęcie typu
Reguły wnioskowania o typie
Po co są typy?
Istotnym składnikiem języka programowania jest system kontroli typologicznej.
Chroni on programistów przed ich własnymi błędami, stąd jest kluczowym czynnikiem podwyższenia niezawodności oprogramowania.
Istnieją szacunki pokazujące, że system kontroli typologicznej jest w stanie wykryć 80% błędów semantycznych i koncepcyjnych.
Dało to podstawę do ukucia pojęcia bezpieczeństwo typologiczne (typing safety) jako podstawowej zasady języków programowania.
System typów ma również znaczenie dla modelowania pojęciowego, gdyż typy pełnią rolę semantyczną w dziedzinie przedmiotowej.
Np. typ Student przypisany do obiektu zdradza nam jego intencję i biznesową semantykę.
Typy przenoszą także informację o metodzie reprezentacji danych wewnątrz pamięci komputera (ważne dla standardów, np. CORBA).
Języki bez mocnej kontroli typów są uważane za niebezpieczne, prowadzące do niskiej jakości oprogramowania.
Dlaczego typy nie zawsze są doceniane? (1)
Jakość i niezawodność oprogramowania nie zawsze jest priorytetem działania firm komercyjnych.
Wprowadzenie typów do języka wymaga odpowiedniej kompetencji w tym zakresie, która często nie jest właściwa decydentom i twórcom języków wywodzącym się z tych kręgów.
Nieliczne uczelnie prowadzą w tym zakresie wykłady i ćwiczenia.
Niektóre z nich traktują typy jako okazję do prezentowania (wyrafinowanych, lecz niepraktycznych) teorii matematycznych w zakresie typów, a nie do objaśniania rzeczywistych problemów i rozwiązań.
Przełożenie tych teorii na efektywną implementację jest zwykle trudne lub niemożliwe, a najczęściej (z powodu ograniczeń teorii) bezsensowne.
Implementacja kontroli typologicznej jest dodatkowym obciążeniem dla twórców języka lub systemu, zwiększającym koszt i czas wytworzenia odpowiedniego oprogramowania.
Programy uwzględniające kontrolę typologiczną są dłuższe (chociaż zwykle bardziej czytelne, ze względu na modelowanie pojęciowe).
Dlaczego typy nie zawsze są doceniane? (1)
Język z mocną kontrolą typów traci część elastyczności.
Zwykle oznacza bardziej sztywne struktury danych, co może być nieakceptowalne dla rozluźnionych formatów, np. dla XML.
W Pascalu zbyt mocna kontrola typologiczna uniemożliwia m.in. napisanie procedury mnożącej dwie macierze o dowolnych wymiarach.
Język z mocną kontrolą typów bardzo utrudnia programowanie generyczne, przy którym docelowy typ przetwarzanego obiektu nie jest znany w czasie kompilacji.
Programowanie generyczne wymaga odzyskania informacji o strukturze/typie obiektu podczas wykonania programu i zastosowanie do niego przetwarzania.
Ten aspekt zaowocował rodziną języków programowania tzw. polimorficznych, których najwybitniejszym przykładem jest SML.
Ta linia języków programowania nie sprawdziła się jak dotąd w powszechnym programowaniu.
Podstawową metodą programowania generycznego jest refleksja (znana m.in. z dynamicznego SQL i DII CORBA), która w istocie bardzo utrudnia lub wręcz uniemożliwia mocną statyczną kontrolę typów.
Co to jest system typów?
Typ jest formalnym ograniczeniem narzuconym na budowę bytu programistycznego lub jest specyfikacją jego parametrów i wyniku.
Z drugiej strony, typ jest formalnym ograniczeniem kontekstu, w którym odwołanie do tego bytu może być użyte w programie.
System typów języka programowania polega na przypisywaniu wyrażeń oznaczających typy bytom występującym w programie (obiektom, funkcjom, procedurom, metodom itd.), oraz sprawdzanie zgodności użycia danego bytu w programie z jego zadeklarowanym typem.
Typów używa się także do dynamicznej kontroli poprawności budowy obiektów
Patrz np. DTD lub XMLSchema dla plików XML.
Jest to istotna, ale raczej drugorzędna rola systemu typów, która w klasycznych językach programowania i językach baz danych nie występuje.
Typy a schematy baz danych (1)
Tradycyjnie typy są własnością programów.
W związku z niezależnością danych nastąpiło przesunięcie typów na stronę danych.
W ten sposób pojawiło się pojęcie schematu bazy danych.
Schemat pełni dwie role.
Informuje programistę o tym, co baza danych zawiera i jak jest zorganizowana.
Jest wykorzystywany przez SZBD do kontroli danych zapamiętanych w bazie danych.
Schemat bazy danych zwalnia języki programowania z obowiązku trzymania informacji typologicznej.
Kompilator języka powinien odczytać typ ze schematu zapamiętanego w bazie danych.
Typy przyjmują postać niezależną od konkretnego języka programowania.
Patrz np. system typów standardu OMG CORBA oraz standardu ODMG.
W ramach platformy .NET powstaje zunifikowany system typów dla wszystkich języków programowania.
Typy a schematy baz danych (2)
Często podkreśla się podobieństwo typów znanych z języków programowania do schematów znanych z baz danych.
Schematy bazy danych nie definiują jednak wyłącznie typów, gdyż ich podstawową funkcją jest modelowanie pojęciowe.
Schematy są tym, co w języku programowania nazywa się deklaracją.
Schematy łączą deklarowanie zmiennych, obiektów, tabel lub innych bytów bazy danych z określaniem ich typu.
Przykładowo, możemy mieć następującą definicję typu TypPrac:
typedef TypPrac -> struct{NrPrac:int, Nazwisko:string, Zar:int};
Tę definicję można wykorzystać do deklaracji zmiennej MójPrac:
MójPrac : TypPrac;
W schematach baz danych konstrukcją semantycznie równoważną jest wyrażenie, w którym nazwę typu tekstowo zastąpiliśmy prawą stroną definicji typu:
MójPrac : struct{ NrPrac:int, Nazwisko:string, Zar:int};
W schemacie konstrukcje typedef mogą występować lub nie.
Przykładowo, w schematach zapisanych w SQL-92 nie występują.
Strukturalna zgodność typów
Z powodu lepszego modelowania pojęciowego, krótszego kodu oraz zwiększenia potencjału dla ponownego użycia definicje typów określające ich nazwy (po lewej stronie) oraz wyrażenie definiujące (po prawej stronie) są cechą większości znanych języków i systemów.
O takich konstrukcjach mówi się niekiedy jako o typach definiowanych przez użytkownika (user-defined types).
Z powodu semantycznej równoważności typy definiowane przez użytkownika nie są składnikiem formalnej semantyki schematu (abstrahującej od modelowania pojęciowego).
Nazwy typów występujące w deklaracjach są tekstowo rozwijane do pełnej postaci, z użyciem prawych stron definicji typów.
Takie podejście jest określane jako strukturalna zgodność typów.
W strukturalnej zgodności typów ich nazwy nie mają znaczenia.
Liczy się tylko czy definiowane struktury danych są takie same.
Nazwowa zgodność typów
Większość języków programowania przyjmuje zgodność typów, określaną jako zgodność nazwową (często kombinowaną z elementami zgodności strukturalnej).
Przy zgodności nazwowej nazwa typu jest nośnikiem semantyki formalnej i nie może być zastąpiona przez prawą stronę definicji nazwy typu.
Przykładowo, jeżeli mamy dwie definicje typów:
typedef TypOsoba -> struct { Imię : string , Wiek: int };
typedef TypPies -> struct { Imię : string , Wiek: int };
to przy zgodności strukturalnej deklaracja zmiennej Florek:
Florek : TypOsoba;
jest dla kompilatora równoważna deklaracji
Florek : TypPies;
W niektórych sytuacjach przyjęcie zgodności strukturalnej może prowadzić do osłabienia kontroli typologicznej
Np. zmienna typu TypPies może być użyta w kontekstach, w których oczekiwana jest zmienna typu TypOsoba.
Nazwowa zgodność typów rozróżnia deklaracje bytów programistycznych wykorzystując nazwy typów.
Statyczna i dynamiczna kontrola typologiczna
Statyczna kontrola typów zachodzi w trakcie kompilacji programu, zaś dynamiczna - w czasie jego wykonania.
Kontrola dynamiczna może także dotyczyć obiektów zapamiętanych w składzie.
Języki takie jak DTD i XML Schema służą głównie do dynamicznej kontroli obiektów (plików) XML.
Nie jest jasne, czy i jak mogą być zastosowane do statycznej kontroli typów zapytań lub programów.
Uważa się, że prawdziwa, mocna kontrola typów jest kontrolą statyczną.
Kontrola dynamiczna jest również skuteczna, gdyż umożliwia wykrycie błędu typologicznego podczas testowania programu.
Wadą kontroli dynamicznej jest dodatkowe obciążenie tą kontrolą czasów wykonania.
Kontrola ta może być również niepełna, gdyż niemożliwe jest przetestowanie programu na wszystkie przyszłe sytuacje, w których może on się znaleźć.
Dynamiczna kontrola obiektów
Często jest głoszony pogląd, że dobra, "szczelna" statyczna kontrola typologiczna eliminuje potrzebę dynamicznej kontroli typologicznej obiektów, gdyż przy szczelnym systemie typów nie jest możliwe wytworzenie obiektu typologicznie niepoprawnego.
Jest to prawda pod warunkiem, że obiekty są przetwarzane wyłącznie przez jeden język programowania.
W klasycznych językach programowania, takich jak C lub Pascal, obiekty (zmienne) są upakowane oszczędnie, w postaci sekwencji bitów, zaś cała informacja o reprezentacji wartości jest składnikiem jego typu.
Typ z kolei jest drugiej kategorii programistycznej, czyli jest niedostępny podczas czasu wykonania.
Przy tym założeniu dynamiczna kontrola typu obiektu jest oczywiście niemożliwa.
To założenie nie jest spełnione dla obiektów bazy danych, które z reguły są obsługiwane przez wiele języków i interfejsów, zazwyczaj z odmiennymi systemami typologicznymi lub nie posiadające kontroli typologicznej.
Niektóre opcje w językach programowania (np. warianty, wartości zerowe, elipsy, automatyczne koercje) stwarzają nieszczelności w systemie typów, W takiej sytuacji kontrola dynamiczna typów obiektów jest równie ważna jak typologiczna kontrola programów.
Typy w językach zapytań (1)
Teoria i praktyka typów jest w dużej mierze niezależna w stosunku do języków zapytań.
Na temat typów napisano tak wiele, że z pozoru wniesienie tu istotnego wkładu jest zadaniem niemożliwym.
W takich sytuacjach pada najczęściej sugestia zaadaptowania jednego z istniejących systemów typów spośród propozycji przedstawionych w rozlicznych językach, systemach, standardach lub literaturze.
Istnieją jednak cechy języka zapytań, które wprowadzają nowe problemy i potencjalnie nowe rozwiązania:
Nazwa obiektu jako jego inwariant.
  • Obiekty w językach programowania nie mają przypisanej im nazwy.
  • Tymczasem jest to reguła dla obiektów zapamiętanych w bazie danych.
  • Nazwa jako inwariant obiektu powinna być sprawdzana typologicznie.
Struktury, których składniki nie posiadają przypisanych im nazw.
  • Budowana konsekwentnie semantyka języka zapytań prowadzi do konieczności wprowadzenia takich struktur.
  • Natomiast najbardziej znane systemy typologiczne zakładają, że w ramach struktur każdy element musi mieć przypisaną mu nazwę.
Typy w językach zapytań (2) - dalsze odstępstwa
W naszym przypadku (i w przypadku XML) pojęcie kolekcji nie zostało wprowadzone na poziomie składu obiektów, gdyż takie potraktowanie go prowadzi do złamania zasad obiektowości.
  • Natomiast wprowadziliśmy kolekcje (bagi i sekwencje) na poziomie rezultatów zwracanych przez zapytanie.
Automatyczne koercje i elipsy. W językach zapytań nabierają większego znaczenia.
Nieregularności w danych. Dotychczasowe systemy statycznej kontroli typologicznej ustalały nie tylko sztywny format danych, ale również reprezentację danych.
Dynamiczne role w modelu M2 stwarzają nieco inną sytuację dla mocnej kontroli typu.
Konieczność uwzględnienia w systemie wnioskowania o typie całej sytuacji na stosie środowiskowym, tak jak ona została opisana w poprzednich rozdziałach.
Przykładowo, zapytanie
Osoba.(Dział where Nazwa = Nazwisko)
ma sens koncepcyjny.
Czy takie zapytanie będziemy uważać za typologicznie poprawne?
Wady istniejących systemów typologicznych
Poza wymienionymi osobliwościami baz danych i ich języków zapytań, mamy wiele zastrzeżeń do stosowanych w systemach obiektowych rozwiązań typologicznych i ich teorii.
Przykładowo, zarówno CORBA, jak i Java nie zajmują się asocjacjami, mają też ograniczenia w zakresie definicji kolekcji.
Próbą stworzenia systemu typów dla obiektowych baz danych był Object Definition Language (ODL) standardu ODMG.
Jednakże przyjęty tam polimorfizm inkluzyjny jest krytykowany jako niespójny.
Alternatywą miał być pomysł teoretyczny określany jako F-bounded polymorphism.
Ta koncepcja nie wydaje się jednak na tyle dojrzała, aby traktować ją jako implementowalną i skuteczną w praktycznych językach.
Polimorfizm parametryczny (parametric polymorphism), znany z SML i innych języków tzw. polimorficznych, pozostaje koncepcją akademicką nie znajdującą potwierdzenia w powszechnej praktyce.
Pojęcie typu
Istnieje sporo poglądów i nieporozumień dookoła pojęć takich jak:
typ, klasa, interfejs,
abstrakcyjny typ danych,
dziedziczenie,
dynamiczne role obiektów.
...
Splątanie tych pojęć w literaturze języków programowania, mnogość definicji i różne wypowiedzi na temat ich wzajemnego stosunku spowodowały znaczny chaos.
Paradoksalnie, w opisie metod mocnej kontroli typu najtrudniejsze jest wyjaśnienie, co to jest "typ".
Na ten temat napisano ogromną liczbę książek i artykułów.
Ich podmiotem jest pojęcie typu zdefiniowane jako matematyczna abstrakcja.
Sprowokowało ono teoretyków do potraktowanie typu jako pojęcia matematycznego oraz kontroli typologicznej jako systemu formalnego działającego na bytach matematycznych.
Efektem jest nie uporządkowanie pojęć, lecz jeszcze większy chaos.
Moje podejście do typów
Będę starać się objaśnić mocną kontrolę typologiczną na gruncie praktycznym, bez nawiązywania do niepraktycznych teorii.
Nie będę starać się definiować pojęcia typu "jako takiego".
Pojęcie typu będzie więc wyjaśnione implicite, poprzez abstrakcyjną implementację mechanizmu kontroli typologicznej.
Nieadekwatność teorii typów polega na traktowaniu semantyki typu jako zbioru wartości.
W odróżnieniu przyjmiemy, że typy są tylko napisami kwalifikującymi schemat bazy danych i inne byty.
Kontrola typów polega na ustaleniu i zaimplementowaniu reguł przekształcania specyfikacji (sygnatur) zawierających te napisy.
Wyjaśnienie mocnej kontroli typologicznej sprowadza się do wykorzystania funkcji static_type_check bardzo podobnej do wprowadzonej w poprzednich wykładach funkcji static_eval.
Zachowanie się funkcji static_type_check jest uzależnione od definicji funkcji static_nested, konstrukcji metabazy, konstrukcji stosów S_ENVS i S_QRES oraz pewnych reguł i metareguł wnioskowania o typie.
Zewnętrzny i wewnętrzny system typów
Zewnętrzny system typów jest określony przez zbiór napisów, których intuicyjną semantyką jest wyróżnienie niezmienników budowy danego bytu programistycznego, np. bazy danych, obiektu lub modułu.
Przykładem jest napis integer przypisany do deklaracji pewnego obiektu.
Zewnętrzny system typów często jest uwikłany w definicje innych abstrakcji, np. w definicje interfejsów, klas, modułów, funkcji, metod itd.
Często, np. w języku Pascal lub C, typ przybiera postać samodzielnego nazwanego fragmentu tekstu programu.
Będziemy przyjmować (w odróżnieniu od większości systemów typologicznych), że taki nazwany fragment tekstu nie ma samodzielnej formalnej semantyki.
Istnieje wyłącznie jako makrodefinicja, czyli pewien nazwany napis.
To wyklucza typy rekurencyjne, ale ich znaczenie w praktyce jest marginalne.
Dowolna nazwa typu (poza int, float, string, bool, date, itd.) jest tylko skrótem dla tego napisu, który ostatecznie powinien być tekstowo rozwinięty do pełnej postaci, w której występują tylko typy atomowe.
Reguły wnioskowania o typie
Nie będziemy także zajmować się semantyką napisów, takich jak int, float, string, bool, date itd.
Matematycy widzą w takich napisach oznaczenia pewnych zbiorów, ale będzie to dla nas nieistotne.
Istotna będzie dla nas "arytmetyka" operatorów działających na takich napisach, np.

graf
pokaż animację

Są to tzw. monomorficzne reguły wnioskowania o typie.
Lewa strona takiej reguły przedstawia pewną sytuację podczas działania procedury static_type_check, natomiast prawa strona - wynik tego działania.
Elementami tej arytmetyki są sygnatury (wprowadzone  poprzednio).
Dla dowolnego operatora należy przypisać zestaw takich reguł.