DEV Community: Betelgeuse

Ty cloudy

Betelgeuse — Sun, 19 Jun 2022 09:50:53 +0000

Cloud computing, jak jej známe dnes, je s námi již dvě dekády a dávno nejde o buzzword. Metaforu mraku vnesl do distribuovaných systémů Apple na počátku devadesátých let, ale teprve s rozvojem internetu tento přístup k tvorbě softwarových systémů zpopularizoval Amazon se svým AWS (a následně se přidali další, například Microsoft s Azure). Zde se zaměříme na současný stav, především tedy monolity vs. mikroslužby, moderní úložiště a dnes nejlepší programovací jazyky pro tuto oblast.

Co nás čeká

Cloudová služba sestává z vlastní aplikace (napsané například v Javě nebo nyní populárním Go), ideálně bezstavové, která musí někde běžet, typicky v kontejneru (Docker apod.) v nějakém shluku serverů.

Data žijí v úložišti, ke kterému aplikace přistupuje a data vhodným způsobem prezentuje (buď přímo na webové stránce nebo pomocí API například pro mobilní aplikace). Dříve byly značně populární specializované objektové databáze, ovšem dnešní relační databáze nabízejí různá rozšíření pro práci s objektovými daty (například JSONB v PostgreSQL), jejichž nasazení je téměř vždy výhodnější. Případně se může použít nějaká NoSQL databáze, protože ty jsou oproti relačním podstatně výkonnější v distribuovaném prostředí. Příkladem je například Datastore v Google App Engine, ke které se záhy dostaneme.

Monolity a mikroslužby

Monolitická aplikace je jedna velká binárka, jejíž instance běží na několika serverech a zpracovávají požadavky klientů. Taková aplikace se snáze píše, překládá, nasazuje a, popravdě, pro většinu projektů je tato architektura plně postačující.

U velkých projektů se vyplácí rozsekání aplikace do samostatných celků, které se implementují a nasazují zvlášť a komunikují mezi sebou po síti. Nejpopulárnější jsou v současnosti v tomto ohledu mikroslužby, což jsou malé, funkčně omezené aplikace, každá ve svém vlastním kontejneru, které dohromady tvoří vysoce škálovatelnou aplikaci.

Mikroslužby mezi sebou potřebují komunikovat rychle, k čemuž slouží specializované protokoly a knihovny, například gRPC. Každá má také svou databázi, v dobrém návrhu se nepoužívá jedna sdílená. Jednou z výhod mikroslužeb je, že každá může být napsaná v jiném jazyku (Java, C++, Go, Rust apod.) a používat jinou databázi (relační, dokumentovou, grafovou atd.)

Google App Engine (GAE)

GAE je prostředí a sada knihoven od Googlu pro tvorbu cloudových aplikací, které lze psát v několika jazycích, z nichž je nejefektivnější Go (při použití tzv. "custom runtimes" lze použít libovolný jazyk, za tu námahu to ale nestojí). Později se podíváme i na neméně efektivní Rust.

V GAE se typicky nasazují monolity (je ale možné aplikaci rozdělit do samostatných služeb), které mají přístup k rychlému objektovému úložišti, memcache (pro zrychlení zpracování požadavků) nebo třeba frontám úloh. Nasazení a správa jsou plně automatické, Google aplikaci přeloží, zabalí do kontejneru a bezpečně spustí na svých serverech. Nové instance jsou spouštěny automaticky s rostoucí zátěží.

Datastore v GAE nemá žádné datové schéma, jde o poměrně jednoduchou NoSQL databázi. V Go lze ukládat přímo objekty, například:

type User struct {
  ID       uuid.UUID
  UserName string
  Email    string
  FullName string         `datastore:",noindex"`
  Key      *datastore.Key `datastore:"-"`
}

func InsertUser(ctx context.Context, u *User) error {
  key := datastore.NewIncompleteKey(ctx, "User", nil)
  key, err := datastore.Put(ctx, key, u)
  if err != nil {
    return err
  }
  u.Key = key
  return nil
}

Jednotlivé položky odpovídají sloupcům v relační databázi a automaticky se indexují, pokud není přítomen tag noindex.

Příště si ukážeme jednoduchou aplikaci pro GAE a práci s databází.

Rovnostní typy a negace typů

Betelgeuse — Wed, 23 Feb 2022 11:15:59 +0000

Předchozí článek byl úvodem do závislostních typů a jejich použití v bezpečnostně kritických aplikacích. V tomto zavedeme rovnostní typy a vylepšíme původní kód.

Nejprve definice typu pro ilustrační příklad:

data DayOfWeek = Mon | Tue | Wed | Thu | Fri | Sat | Sun

Jednoduchá funkce ověří, že zadaný den je pondělí:

isMonday : DayOfWeek -> Bool
isMonday Mon = True
isMonday _ = False

V kontraktech se často používají porovnání hodnot. Každé porovnání a = b hodnot stejného typu je možné považovat za typ. Pokud rovnost platí, tento typ má hodnotu Refl, kterou je možné použít ve funkcích. Následující funkce je v podstatě náhradou příslušného jednotkového testu, korektnost se ale ověřuje již v době překladu v rámci typové kontroly, ne až za běhu.

aProof : (d : DayOfWeek) -> d = Mon -> isMonday d = True

Tato funkce dostane dva argumenty a ověří, že funkce isMonday vrátí správnou hodnotu. Její definice je

aProof _ prf = rewrite prf in Refl

Typ návratové hodnoty je rovnostní, proto se musí jednat o nějaké Refl. Tuto hodnotu získáme tak, že pomocí rewrite přepíšeme d na Mon v typu isMonday d, což se vyhodnotí jako True.

Podobně bychom mohli mít analogický test, ale nyní chceme dokázat, že něco neplatí. Zavedeme proto negaci typů, Not T, což je v zásadě funkce typu T -> Void, kde Void je typ bez hodnot. Tuto funkci proto není možné zavolat, neboť není možné vrátit žádnou hodnotu. Příkladem budiž následující analogie jednotkového testu:

anotherProof : (d : DayOfWeek) -> d = Tue -> Not (isMonday d = True)

Definice této funkce je

anotherProof _ prf = rewrite prf in falseNotTrue

Zbývá definovat funkci falseNotTrue typu Not (False = True):

falseNotTrue : Not (False = True)
falseNotTrue _ impossible

Obecně platí, že dvě hodnoty stejného typu můžou být shodné ve smyslu výrokové rovnosti, pokud výslovně neřekneme, že se rovnat nemůžou.

Vraťme se nyní ke staré známé funkci safeDiv. Změníme typ kontraktu, že nelze dělit nulou:

safeDiv : Nat -> (n : Nat) -> {auto prf : Not (n = 0)} -> Nat

Budeme potřebovat pomocnou funkci říkající, že nula není následníkem žádného přirozeného čísla:

sucNonZero : (n : Nat) -> Not ((S n) = 0)
sucNonZero _ _ impossible

Původní funkce isNonZero nyní vypadá takto:

isNonZero : (n : Nat) -> Maybe (Not (n = 0))
isNonZero 0 = Nothing
isNonZero (S n) = Just (sucNonZero n)

Je potěšitelné, že na samotné funkci safeDiv se nic nemění.

Funkce isNonZero je ale stále poněkud problematická, protože sice někdy vrací důkaz nenulovosti, ale pokud je výsledkem Nothing, nevíme, jestli je argument funkce nulový nebo ne. Místo Nothing bychom chtěli důkaz n = 0. K tomu slouží typový operátor Dec, kterému se budeme věnovat příště.

Prolegomena k úvodu do základů závislostních typů

Betelgeuse — Mon, 21 Feb 2022 22:29:08 +0000

Funkce většinou pracují s hodnotami jako čísla, řetězce nebo záznamy, například 12 nebo Praha, jejichž typy jsou Nat a String. Matematické funkce mohou ale pracovat s libovolnými objekty, je proto smysluplné ptát se, jakého typu je ono Nat nebo String. Zadefinujme si jejich typ jako Type. To nám umožní definovat takovouto funkci:

getType : Bool -> Type
getType True = String
getType False = Nat

Funkce getType je sama o sobě k ničemu, ale co kdybychom ji použili v definici jiné funkce? Zkusme například

getValue : (b : Bool) -> getType b
getValue True = "abcd"
getValue False = 1234

Protože funkce getType vrací typ (hodnotu typu Type), můžeme ji použít pro výpočet typu návratové hodnoty funkce getValue, kterou můžeme použít takto:

putStrLn $ show $ getValue True
putStrLn $ show $ getValue False

Pokud vám tato funkce připadá divná, máte pravdu, ve většině jazyků by zapsat nešla, ale v jazycích s takzvanými závislostními typy jsou takovéto funkce běžné.

Představme si, že chceme napsat funkci pro dělení přirozených čísel, která funguje korektně (bez pádů nebo výjimek) na všech vstupech. Předpokládáme, že máme funkci typu

divNat : Nat -> Nat -> Nat

která ale při dělení nulou zkolabuje. Máme dvě možnosti: buď rozšíříme typ návratové hodnoty, abychom mohli při pokusu o dělení nulou sdělit, že výpočet nelze provést, nebo zúžíme definiční obor funkce pro dělení. V prvním případě dostaneme například:

safeDiv : Nat -> Nat -> Maybe Nat

a pří dělení nulou vrátíme místo číselného výsledku Nothing. Ve druhém případě musíme přidat k funkci argument, který zaručí, že dělitel je nenulový:

safeDiv : Nat -> (n : Nat) -> {auto prf : IsNonZero n} -> Nat
safeDiv m n {prf} = divNat m n

Všimněte si, že IsNonZero je generický typ, jehož parametrem je přirozené číslo. K definici tohoto typu využijeme úvahu, že přirozené číslo je nenulové, pokud má předchůdce (který je taktéž přirozeným číslem):

data IsNonZero : Nat -> Type where
    SucNonZero : (n : Nat) -> IsNonZero (S n)

Důkaz nenulovosti druhého argumentu není vždy možné automaticky odvodit, pokud jej například čteme na vstupu, uživateli nic nebrání zadat nulu. Potřebujeme proto funkci, která nám příslušný důkaz dodá, pokud existuje:

isNonZero : (n : Nat) -> Maybe (IsNonZero n)
isNonZero 0 = Nothing
isNonZero (S n) = Just (SucNonZero n)

Funkce isNonZero vrátí Nothing pro nulu a důkaz nenulovosti (dodá předchůdce čísla na vstupu) v ostatních případech. Pokud tedy v kódu není možné nenulovost dělitele odvodit automaticky (viz deklarace auto prf), použijeme funkci isNonZero, která příslušný důkaz umí dodat (jinak vrátí Nothing):

Just m <- readNat | Nothing => putStrLn "not a number"
Just n <- readNat | Nothing => putStrLn "not a number"
case isNonZero n of
    Just prf => putStrLn $ show $ safeDiv m n {prf=prf}
    _ => putStrLn "division by zero"

Přidaný třetí argument se tak dá považovat za kontrakt. Podobný přístup se používá i v jiných jazycích navržených pro bezpečnostně kritické aplikace, například v jazyce SPARK.

V pokračování dojde na typy, které vyjadřují rovnost a negaci.