Uwaga: To jest część serii „Composing Software” (teraz książka!) na temat nauki programowania funkcyjnego i technik kompozycji oprogramowania w JavaScriptES6+ od podstaw. Bądźcie czujni. Będzie tego o wiele więcej!
Kup książkę | Indeks | < Previous | Next >
Nie mylić z:
Algebraicznymi typami danych (czasami określanymi skrótem ADT lub AlgDT). Algebraiczne typy danych odnoszą się do złożonych typów w językach programowania (np. Rust, Haskell, F#), które wykazują pewne właściwości określonych struktur algebraicznych. np. typy sumy i typy iloczynu.
Struktury algebraiczne. Struktury algebraiczne są badane i stosowane z algebry abstrakcyjnej, które, podobnie jak ADT, są również powszechnie określone w kategoriach algebraicznych opisów aksjomatów, ale mają zastosowanie daleko poza światem komputerów i kodu. Może istnieć struktura algebraiczna, która jest niemożliwa do całkowitego zamodelowania w oprogramowaniu. Dla kontrastu, Abstrakcyjne Typy Danych służą jako specyfikacja i przewodnik do formalnej weryfikacji działającego oprogramowania.
An Abstrakcyjny Typ Danych (ADT) jest abstrakcyjną koncepcją zdefiniowaną przez aksjomaty, które reprezentują pewne dane i operacje na tych danych. ADT nie są zdefiniowane w kategoriach konkretnych instancji i nie określają konkretnych typów danych, struktur lub algorytmów używanych w implementacjach. Zamiast tego, ADT definiują typy danych tylko w kategoriach ich operacji i aksjomatów, do których te operacje muszą się stosować.
Wspólne przykłady ADT
- List
- Stack
- Queue
- Set
- Map
- Stream
ADT mogą reprezentować dowolny zestaw operacji na dowolnym rodzaju danych. Innymi słowy, wyczerpująca lista wszystkich możliwych ADT jest nieskończona z tego samego powodu, dla którego wyczerpująca lista wszystkich możliwych zdań angielskich jest nieskończona. ADT są abstrakcyjną koncepcją zestawu operacji na nieokreślonych danych, a nie konkretnym zestawem konkretnych typów danych. Powszechnym błędnym przekonaniem jest to, że konkretne przykłady ADT nauczane w wielu kursach uniwersyteckich i podręcznikach dotyczących struktur danych są tym, czym są ADT. Wiele takich tekstów etykietuje struktury danych „ADT”, a następnie pomija ADT i zamiast tego opisuje struktury danych w konkretnych terminach, nigdy nie narażając studenta na rzeczywistą abstrakcyjną reprezentację typu danych. Oops!
ADT mogą wyrażać wiele użytecznych struktur algebraicznych, w tym semigrupy, monoidy, funktory, monady itp. Specyfikacja Fantasyland jest użytecznym katalogiem struktur algebraicznych opisanych przez ADT, aby zachęcić do interoperacyjnych implementacji w JavaScript. Konstruktorzy bibliotek mogą weryfikować swoje implementacje używając dostarczonych aksjomatów.
Dlaczego ADT?
Abstrakcyjne typy danych są użyteczne ponieważ dostarczają nam sposobu na formalne zdefiniowanie modułów wielokrotnego użytku w sposób, który jest matematycznie uzasadniony, precyzyjny i jednoznaczny. To pozwala nam dzielić wspólny język, aby odnosić się do obszernego słownika użytecznych bloków konstrukcyjnych oprogramowania: Idei, które są przydatne do nauki i noszenia ze sobą, gdy poruszamy się pomiędzy domenami, frameworkami, a nawet językami programowania.
Historia ADT
W latach 60-tych i wczesnych 70-tych, wielu programistów i badaczy informatyki interesowało się kryzysem oprogramowania. Jak ujął to Edsger Dijkstra w swoim wykładzie o nagrodzie Turinga:
„Główną przyczyną kryzysu oprogramowania jest to, że maszyny stały się o kilka rzędów wielkości potężniejsze! Mówiąc wprost: dopóki nie było maszyn, programowanie nie stanowiło żadnego problemu; gdy mieliśmy kilka słabych komputerów, programowanie stało się łagodnym problemem, a teraz, gdy mamy gigantyczne komputery, programowanie stało się równie gigantycznym problemem.”
Problem, do którego się odnosi, polega na tym, że oprogramowanie jest bardzo skomplikowane. Wydrukowana wersja modułu księżycowego Apollo i systemu naprowadzania dla NASA jest mniej więcej wysokości szafki na akta. To bardzo dużo kodu. Wyobraź sobie, że próbujesz przeczytać i zrozumieć każdą linię tego kodu.
Nowoczesne oprogramowanie jest o rząd wielkości bardziej skomplikowane. Facebook był z grubsza 62 miliony linii kodu w 2015 roku. Gdybyś wydrukował 50 linii na stronę, wypełniłbyś 1,24 miliona stron. Gdybyś ułożył te strony w stos, otrzymałbyś około 1800 stron na stopę, czyli 688 stóp. To więcej niż Millenium Tower w San Francisco, najwyższy budynek mieszkalny w San Francisco w czasie pisania tego tekstu.
Zarządzanie złożonością oprogramowania jest jednym z podstawowych wyzwań, przed którymi stoi praktycznie każdy twórca oprogramowania. W latach 60. i 70. nie mieli oni języków, wzorców ani narzędzi, które dziś uważamy za oczywiste. Rzeczy takie jak lintery, intellisense, a nawet narzędzia do analizy statycznej nie zostały jeszcze wynalezione.
Wielu inżynierów oprogramowania zauważyło, że sprzęt, na którym budowali rzeczy, w większości działał. Ale oprogramowanie, częściej niż nie, było skomplikowane, poplątane i kruche. Oprogramowanie było powszechnie:
- Przekraczało budżet
- Opóźnione
- Buggy
- Brakujące wymagania
- Trudne do utrzymania
Gdybyście tylko mogli myśleć o oprogramowaniu w modułowych kawałkach, nie musielibyście rozumieć całego systemu, żeby zrozumieć, jak sprawić, by część systemu działała. Ta zasada projektowania oprogramowania znana jest jako lokalność. Aby uzyskać lokalność, potrzebne są moduły, które można zrozumieć w oderwaniu od reszty systemu. Powinieneś być w stanie jednoznacznie opisać moduł bez nadmiernego precyzowania jego implementacji. To jest problem, który rozwiązują ADT.
Od lat 60-tych prawie do dnia dzisiejszego, postęp w zakresie modularności oprogramowania był głównym problemem. To właśnie z myślą o tych problemach ludzie tacy jak Barbara Liskov (ta sama Liskov, o której mowa w Liskov Substitution Principle z zasad projektowania SOLID OO), Alan Kay, Bertrand Meyer i inne legendy informatyki pracowali nad opisem i specyfikacją różnych narzędzi umożliwiających tworzenie modularnego oprogramowania, w tym ADT, programowania obiektowego i projektowania przez umowę, odpowiednio.
ADT wyłoniły się z pracy Liskov i jej studentów nad językiem programowania CLU w latach 1974-1975. Przyczyniły się one znacząco do stanu wiedzy na temat specyfikacji modułów oprogramowania – języka, którego używamy do opisywania interfejsów pozwalających modułom oprogramowania na interakcję. Formalnie udowodniona zgodność interfejsów znacznie przybliża nas do modularności i interoperacyjności oprogramowania.
Liskov otrzymała w 2008 roku nagrodę Turinga za swoją pracę nad abstrakcją danych, odpornością na błędy i obliczeniami rozproszonymi. ADT odegrały znaczącą rolę w tym osiągnięciu, a obecnie praktycznie każdy uniwersytecki kurs informatyki zawiera ADT w programie nauczania.
Kryzys oprogramowania nigdy nie został całkowicie rozwiązany, a wiele z opisanych powyżej problemów powinno być znanych każdemu profesjonalnemu programiście, ale nauka korzystania z narzędzi takich jak obiekty, moduły i ADT z pewnością pomaga.
Specyfikacje dla ADT
Szczególne kryteria mogą być użyte do oceny przydatności specyfikacji ADT. Ja nazywam te kryteria FAMED, ale tylko wymyśliłem ten mnemonik. Oryginalne kryteria zostały opublikowane przez Liskova i Zillesa w ich słynnej pracy z 1975 roku, „Specification Techniques for Data Abstractions.”
- Formalne. Specyfikacje muszą być formalne. Znaczenie każdego elementu w specyfikacji musi być zdefiniowane na tyle szczegółowo, że docelowi odbiorcy powinni mieć dość duże szanse na skonstruowanie zgodnej implementacji ze specyfikacji. Musi istnieć możliwość zaimplementowania w kodzie dowodu algebraicznego dla każdego aksjomatu w specyfikacji.
- Applicable. ADT powinny mieć szerokie zastosowanie. ADT powinno być ogólnie wielokrotnego użytku dla wielu różnych konkretnych przypadków użycia. ADT, który opisuje konkretną implementację w konkretnym języku w konkretnej części kodu, jest prawdopodobnie nadspecyfikacją rzeczy. Zamiast tego, ADT najlepiej nadają się do opisywania zachowania wspólnych struktur danych, komponentów biblioteki, modułów, cech języka programowania itp. Na przykład, ADT opisujące operacje na stosie, lub ADT opisujące zachowanie obietnicy.
- Minimalne. Specyfikacje ADT powinny być minimalne. Specyfikacja powinna zawierać interesujące i mające szerokie zastosowanie części zachowania i nic więcej. Każde zachowanie powinno być opisane dokładnie i jednoznacznie, ale z jak najmniejszą ilością specyficznych lub konkretnych szczegółów. Większość specyfikacji ADT powinna być możliwa do udowodnienia za pomocą kilku aksjomatów.
- Rozszerzalność. ADT powinny być rozszerzalne. Mała zmiana w wymaganiu powinna prowadzić tylko do małej zmiany w specyfikacji.
- Deklaratywna. Deklaratywne specyfikacje opisują co, a nie jak. ADT powinny być opisane w kategoriach tego, czym są rzeczy oraz mapowania relacji pomiędzy wejściami i wyjściami, a nie kroków tworzenia struktur danych lub konkretnych kroków, które musi wykonać każda operacja.
Dobre ADT powinno zawierać:
- Opis czytelny dla człowieka. ADT mogą być dość lakoniczne, jeśli nie towarzyszy im opis czytelny dla człowieka. Opis w języku naturalnym, w połączeniu z definicjami algebraicznymi, może działać jak wzajemna kontrola, aby wyjaśnić wszelkie błędy w specyfikacji lub niejednoznaczności w jej zrozumieniu przez czytelnika.
- Definicje. Wyraźnie zdefiniuj wszelkie terminy użyte w specyfikacji, aby uniknąć jakichkolwiek niejasności.
- Abstrakcyjne sygnatury. Opisują oczekiwane wejścia i wyjścia bez powiązania ich z konkretnymi typami lub strukturami danych.
- Aksjomaty. Algebraic definitions of the axiom invariants used to prove that an implementation has satisfied the requirements of the specification.
Stack ADT Example
A stack is a Last In, First Out (LIFO) pile of items which allows users to interact with the stack by pushing a new item to the top of the stack, or popping the most recently pushed item from the top of the stack.
Stacks are commonly used in parsing, sorting, and data collation algorithms.
Definitions
-
a
: Any type -
b
: Any type -
item
: Any type -
stack()
: an empty stack -
stack(a)
: a stack ofa
-
: a pair of
item
andstack
Abstract Signatures
The stack
operation takes any number of items and returns a stack of those items. Typically, the abstract signature for a constructor is defined in terms of itself. Please don’t confuse this with a recursive function.
stack(...items) => stack(...items)
Stack Operations (operations which return a stack)
push(item, stack()) => stack(item)
pop(stack) =>
Axioms
The stack axioms deal primarily with stack and item identity, the sequence of the stack items, and the behavior of pop when the stack is empty.
Identity
Pushing and popping have no side-effects. If you push to a stack and immediately pop from the same stack, the stack should be in the state it was before you pushed.
pop(push(a, stack())) =
- Given: push
a
to the stack and immediately pop from the stack - Should: return a pair of
a
andstack()
.
Sequence
Popping from the stack should respect the sequence: Last In, First Out (LIFO).
pop(push(b, push(a, stack())) =
- Given: push
a
to the stack, then pushb
to the stack, then pop from the stack - Should: return a pair of
b
andstack(a)
.
Empty
Popping from an empty stack results in an undefined item value. In concrete terms, this could be defined with a Maybe(item), Nothing, or Either. In JavaScript, it’s customary to use undefined
. Popping from an empty stack should not change the stack.
pop(stack()) =
- Given: pop from an empty stack
- Should: return a pair of undefined and
stack()
.
Concrete Implementations
An abstract data type could have many concrete implementations, in different languages, libraries, frameworks, etc. Here is one implementation of the above stack ADT, using an encapsulated object, and pure functions over that object:
const stack = (...items) => ({
push: item => stack(...items, item),
pop: () => {
// create a item list
const newItems = ; // remove the last item from the list and
// assign it to a variable
const = newItems.splice(-1); // return the pair
return ;
},
// So we can compare stacks in our assert function
toString: () => `stack(${ items.join(',') })`
});const push = (item, stack) => stack.push(item);
const pop = stack => stack.pop();
And another that implements the stack operations in terms of pure functions over JavaScript’s existing Array
type:
const stack = (...elements) => ;const push = (a, stack) => stack.concat();const pop = stack => {
const newStack = stack.slice(0);
const item = newStack.pop();
return ;
};
Both versions satisfy the following axiom proofs:
// A simple assert function which will display the results
// of the axiom tests, or throw a descriptive error if an
// implementation fails to satisfy an axiom.
const assert = ({given, should, actual, expected}) => {
const stringify = value => Array.isArray(value) ?
`` :
`${ value }`;
const actualString = stringify(actual);
const expectedString = stringify(expected);
if (actualString === expectedString) {
console.log(`OK:
given: ${ given }
should: ${ should }
actual: ${ actualString }
expected: ${ expectedString }
`);
} else {
throw new Error(`NOT OK:
given ${ given }
should ${ should }
actual: ${ actualString }
expected: ${ expectedString }
`);
}
};// Concrete values to pass to the functions:
const a = 'a';
const b = 'b';// Proofs
assert({
given: 'push `a` to the stack and immediately pop from the stack',
should: 'return a pair of `a` and `stack()`',
actual: pop(push(a, stack())),
expected:
})assert({
given: 'push `a` to the stack, then push `b` to the stack, then pop from the stack',
should: 'return a pair of `b` and `stack(a)`.',
actual: pop(push(b, push(a, stack()))),
expected:
});assert({
given: 'pop from an empty stack',
should: 'return a pair of undefined, stack()',
actual: pop(stack()),
expected:
});
Conclusion
- An Abstract Data Type (ADT) is an abstract concept defined by axioms which represent some data and operations on that data.
- Abstrakcyjne Typy Danych skupiają się na tym co, a nie jak (są ujęte deklaratywnie i nie określają algorytmów ani struktur danych).
- Typowe przykłady to listy, stosy, zbiory, itp.
- ADT zapewniają nam sposób na formalne zdefiniowanie modułów wielokrotnego użytku w sposób, który jest matematycznie uzasadniony, precyzyjny i jednoznaczny.
- ADT powstały w wyniku pracy Liskova i studentów nad językiem programowania CLU w latach 70-tych.
- ADT powinny być FAMED. Formal, widely Applicable, Minimal, Extensible, and Declarative.
- ADT powinny zawierać czytelny dla człowieka opis, definicje, abstrakcyjne podpisy i formalnie weryfikowalne aksjomaty.
Porada bonusowa: Jeśli nie jesteś pewien, czy powinieneś enkapsulować daną funkcję, zadaj sobie pytanie, czy umieściłbyś ją w ADT dla swojego komponentu. Pamiętaj, że ADT powinny być minimalne, więc jeśli funkcja nie jest niezbędna, nie jest spójna z innymi operacjami lub jej specyfikacja może się zmienić, enkapsuluj ją.
Glossary
- Aksjomaty są matematycznie uzasadnionymi stwierdzeniami, które muszą być prawdziwe.
- Matematycznie uzasadnione oznacza, że każde pojęcie jest dobrze zdefiniowane matematycznie, tak że można napisać jednoznaczne i możliwe do udowodnienia twierdzenia o faktach na ich podstawie.
Następne kroki
EricElliottJS.com zawiera wiele godzin lekcji wideo i interaktywnych ćwiczeń na tematy takie jak ten. Jeśli podoba Ci się ta zawartość, rozważ dołączenie do nas.