Súčtové typy

Úvod

V teórii typov rozlišujeme dve základné kategórie kombinácií typov: súčinové typy a súčtové typy.

Zatiaľ čo súčinové typy (ako sme videli na predchádzajúcej prednáške) kombinujú hodnoty naraz (dvojica, n-tica, záznam), súčtové typy umožňujú, aby hodnota patrila k jednému z viacerých typov — teda predstavuje alternatívu medzi možnosťami.

Binárny súčtový typ

Základné pojmy súčtových typov zavedieme na príklade binárneho súčtového typu, ktorý je konštruovaný pomocou typového konštruktora ''$+$'': $$T_1 + T_2.$$

Formálne, nech $T_1$ a $T_2$ sú typy. Súčtový typ $T_1 + T_2$ je typ, ktorého termy sú buď typu $T_1$, alebo typu $T_2$, spolu s informáciou (návestím), ktorého typu je daný term.

Injekcie binárneho súčtového typu

Pre súčtový typ $T_1 + T_2$ zavádzame dve operácie ako konštruovať termy:

• $Inl$ – ľavá injekcia - vloženie hodnoty typu $T_1$.
• $Inr$ – pravá injekcia - vloženie hodnoty typu $T_2$.

Každý term typu $T_1 + T_2$ je jednoznačne identifikovaný, či patrí do $Inl$ alebo $Inr$.

Injekcie sú termové konštruktory, pomocou nich z termov typov $T_{1}$ a $T_{2}$ je možné konštruovať term súčtového typu $T_{1}+T_{2}$:

$$ \begin{array} ~ \mathtt{inl}:\ T_1 \to T_{1}+T_{2}\\ \mathtt{inr}:\ T_2 \to T_{1}+T_{2}\\ \end{array} $$

Selektor $\mathtt{case}$

Jedinou operáciou nad termami súčtového typu je selektor: $$ \begin{array}{l} \mathtt{case}\ t\ \mathtt{of} \\ \qquad ~~~ \mathtt{inl}\ x_1 \Rightarrow t_1\\ \qquad ||\ \mathtt{inr}\ x_2 \Rightarrow t_2 \end{array} $$ kde:

• $t$ je term binárneho súčtového typu $T_1 + T_2$,
• $x_1:T_1$ a $x_2:T_2$ sú lokálne premenné, ktoré sa môžu nachádzať voľne v $t_1$ resp. $t_2$.

Pri vyhodnotení:

• Najprv sa term $t$ redukuje na hodnotu.
• Na základe toho, či je hodnota konštruovaná prostredníctvom $inl$ alebo $inr$, zvolí sa príslušná vetva.
• Všetky výskyty lokálnej premennej ($x_1$ alebo $x_2$) sa substituujú vo vetve hodnotou, ktorú viaže daný konštruktor.

Súčinové a súčtové typy sú navzájom duálne:

Rozšírenie syntaxe jednoducho typovaného $\lambda$-kalkulu o binárny súčtový typ

Syntax jednoducho typovaného $\lambda$-kalkulu rozšírime o nové tvary termov, hodnôt a typu pre binárny súčtový typ:

$$ \begin{array}{ll} t::= & \ldots~|~\mathtt{inl}~t~|~\mathtt{inr}~t~|~\mathtt{case}~t~\mathtt{of~inl}~x\Rightarrow t ~ ||~\mathtt{inr}~ x\Rightarrow t \\ v::= & \ldots~|~\mathtt{inl}~v~|~\mathtt{inr}~v \\ T::= & \ldots~|~T + T \end{array} $$

Priorita a asociativita typových konštruktorov

Aktuálne máme v jazyku zavedené 3 binárne typové konštruktory. Pre jednoznačnosť je potrebné uviesť ich prioritu (kde 1 znamená najvyššiu prioritu) a asociativitu:

Sumy a jednoznačnosť typov

Väčšina vlastností relácie typovania, ktoré platia pre jednoducho typovaný $\lambda$-kalkul, platia aj pre súčtové typy, s výnimkou vety o jednoznačnosti typov.

Veta o jednoznačnosti typov hovorí, že v danom typovom kontexte $\Gamma$ má term $t$ najviac jeden typ, čo pre súčtové typy to neplatí.

Majme term $t$ typu $Nat$. Po aplikácii ľubovoľného z termových konštruktorov $\mathtt{inl}$ resp. $\mathtt{inr}$ na term $t$ vznikne nasledujúci problém: $$ \begin{array} \quad \mathtt{inl}\ t:\ Nat\ +\ ? \\ \mathtt{inr}\ t:\ ?\ +\ Nat \end{array} $$

To znamená, že nie je jednoznačné akého typu je $\mathtt{inl}\ t$ resp. $\mathtt{inr}\ t$. Z tohto dôvodu algoritmus pre kontrolu typov nemožno konštruovať len aplikovaním typovacích pravidiel zdola nahor, ako to bolo doteraz.

Metódy kontroly typov pre súčtové typy

Aby bolo vykonať kontrolu typov v prípade súčtových typov, existujú rôzne prístupy. Najčastejšie sú to nasledujúce tri metódy:

• Upravíme algoritmus kontroly typov tak, že bude bude odhadovať, aký je typ $T_2$. Znamená to, že ponecháme $T_2$ ako neurčený typ a neskôr sa pokúšame zistiť, aká by mala byť jeho hodnota. Táto metóda sa používa pri rekonštrukcii typov (odvodení typov).
• Zjemníme jazyk typov tak, aby povoľoval všetky možné hodnoty pre typ $T_2$ a aby bol jednotne reprezentovaný. Táto metóda sa používa aj pri podtypoch;
• Požadujeme od programátora, aby poskytol explicitnú typovú anotáciu, ktorá indikuje, aký typ pre $T_2$ zamýšľa. Táto metóda je najjednoduchšia a je praktická: v úplnom návrhu jazyka sú tieto explicitné anotácie často umiestnené na iných jazykových konštrukciách, čím sa stanú neviditeľnými.

Pre zaručenie jednoznačnej kontroly typov teda rozšírime zápis termov binárneho súčtového typu o explicitnú typovú anotáciu, na ktorú použijeme odvodený tvar pripísanie.

Rozšírenú syntax pre termy a hodnoty modifikujeme nasledovne:

$$ \begin{array}{ll} t::= & \ldots~|~\mathtt{inl}~t~\mathtt{as}~T~|~\mathtt{inr}~t~\mathtt{as}~T \\ \\ v::= & \ldots~|~\mathtt{inl}~v~\mathtt{as}~T~|~\mathtt{inr}~v~\mathtt{as}~T \end{array} $$

Typovacie pravidlá

Vyhodnocovacie pravidlá

(* definícia "súčtového" typu Nat + Bool *)
type nat_or_bool = Inl of int | Inr of bool

(* getnat : nat_or_bool -> int *)
let getnat (x : nat_or_bool) : int =
  match x with
  | Inl n -> n
  | Inr b -> if b then 1 else 0

(* príklady použitia *)
utop # getnat (Inr true);;
- : int = 1

utop # getnat (Inr false);;
- : int = 0

utop # getnat (Inl 5);;
- : int = 5

Varianty

Binárne súčty možno zovšeobecniť súčty $n$ typov, podobné ako bol rozšírený súčinový typ dvojica na typ n-tica a neskôr na záznam. Takto zovšeobecnené súčtové typy sa nazývajú varianty s návestiami.

Namiesto typu $ T_1 + T_2 $ je použitá notácia:

$$ [ lab_1: T_1, lab_2: T_2 ], $$

pričom $ lab_1, lab_2 $ sú návestia položiek variantu. Prostredníctvom návestí sú konštruované typy daného variantového typu.

Namiesto toho, aby vetvy termu case boli označené návesťami inl, inr, je možné použiť ľubovoľne pomenované návestia:

$$ \begin{array}{ll} \mathtt{inl}~t~\mathtt{as}~T_1 + T_2 & \text{používame}~~~[ lab_1 = t]~\mathtt{as}~[ lab_1: T_1, lab_2: T_2] \\ \mathtt{inr}~t~\mathtt{as}~T_1 + T_2 & \text{používame}~~~[ lab_2 = t]~\mathtt{as}~[ lab_1: T_1, lab_2: T_2] \end{array} $$

Rozdiel medzi zápisom záznamu a variantu je v zátvorkách:

• pre záznamy používame zátvorky ⟨ a ⟩;
• pre varianty používame zátvorky [ a ].

Syntax jednoducho typovaného $\lambda$-kalkulu rozšírená o variantové typy

Formálna definícia rozšírenia jednoducho typovaného $\lambda$-kalkulu o variantové typy, zároveň zovšeobecňuje binárne súčtové typy na súčet $n$ typov.

Syntax je rozšírená o dva nové tvary termov a nový tvar pre variantový typ:

$$ \begin{array}{ll} t::= \ldots~|~~ [ lab = t]~\mathtt{as}~T ~~| ~~\mathtt{case}~t~\mathtt{of}~[ lab_i = x_i] \Rightarrow t_i^{~i\in 1..n} \\ T::= \ldots ~|~ [ lab_i: T_i^{~i\in 1..n}] \end{array} $$

Typovacie pravidlá

Vyhodnocovacie pravidlá

Špeciálne variantové typy

Varianty môžeme využiť aj na definovanie niekoľkých špeciálnych, no veľmi užitočných typov.
Medzi ne patria:

• Voliteľné hodnoty — reprezentujú možnosť, že hodnota môže alebo nemusí existovať
  (napr. Maybe, Option v programovacích jazykoch).
• Enumeračné typy — umožňujú vymenovať pevne danú množinu možností
  (napr. Color = [ red, green, blue ]).
• Jednopoložkové variantové typy — používajú sa na označenie špecifického prípadu alebo obalu hodnoty.

Enumeračné typy

Enumeračné typy sú variantové typy, kde každá položka má:

• návestie lab, a
• typ Unit.

(* Definícia typu Week *)
type week =
  | Monday
  | Tuesday
  | Wednesday
  | Thursday
  | Friday
  | Saturday
  | Sunday

(* Funkcia, ktorá vracia nasledujúci pracovný deň *)
let next_work_day w =
  match w with
  | Monday -> Tuesday
  | Tuesday -> Wednesday
  | Wednesday -> Thursday
  | Thursday -> Friday
  | Friday -> Monday
  | Saturday -> Monday
  | Sunday -> Monday

(* Príklad použitia *)
utop # next_work_day Saturday;;
- : week = Monday

Variantové typy s jednou položkou

Sú variantové typy, ktoré majú práve jedno návestie $lab$ a sú tvaru:

$$ V = [ lab: T ] $$

Prvky typu $V$ sú zapúzdrené a pomenované prvky typu $T$, každý prvok typu $V$ má tvar:

$$ [lab = t]~\mathtt{as}~V, \quad \text{pre } t:T $$

Na prvý pohľad nie je jasné, na čo by takýto typ mohol byť užitočný.

Často sa používa, aby sa zabránilo priamemu používaniu operácií typu $T$ na hodnoty typu $V$. Operácie typu $T$ nemôžu byť aplikované na prvky typu $V$ bez predchádzajúceho rozbalenia z variantu pomocou selektora case.

Teda hodnoty typu $V$ nemôžeme náhodne zameniť za hodnoty typu $T$.

(* Jednopoložkové varianty pre bezpečné meny *)

(* Definícia typov pre meny *)
type dollar_amount = Dollar of float
type euro_amount   = Euro of float

(* Funkcia násobenia *)
let times x y = x *. y

(* Bezpečné konverzie medzi menami *)
let dollartoeuro (Dollar d) =
  Euro (times d 0.8)

let eurotodollar (Euro e) =
  Dollar (times e 1.25)

let mybalance = Dollar 39.50

(* Príklad použitia *)

utop # dollartoeuro mybalance;;
- : euro_amount = Euro 31.6

utop # eurotodollar (dollartoeuro mybalance);;
- : dollar_amount = Dollar 39.5

utop # dollartoeuro (dollartoeuro mybalance);;
Error: This expression has type euro_amount
       but an expression was expected of type dollar_amount

Voliteľné hodnoty

Variantové typy umožňujú reprezentovať voliteľné hodnoty (optional values),
teda hodnoty, ktoré nemusia byť vždy prítomné.

Formálne je možné voliteľnú hodnotu pre ľubovoľný typ $T$ definovať ako variantový typ:

$$ \mathtt{Option}\;T = [\, none: \mathtt{Unit},\; some: T \,] $$

Tento typ vyjadruje, že hodnota typu $ \mathtt{Optional}\;T $ môže byť jednou z dvoch možností:

• $ [\, none = \mathtt{unit} \,] $ — prázdna hodnota, označujúca neprítomnosť hodnoty typu $ T $;
• $ [\, some = t \,] $ — hodnota typu $ T $, ktorá je prítomná.

Takto definovaný typ je analógiou známych konštrukcií v rôznych programovacích jazykoch:

type nat = Zero | S of nat
type natoption = None | Some of nat

V jednoducho typovanom $\lambda$-kalkule typ $Option$ umožňuje pracovať s čiastočnými funkciami alebo neúplnými dátami bez potreby špeciálnych chýb či výnimiek.

• Je možné jednoducho vyjadriť, že funkcia nemusí vždy vrátiť výsledok (napr. find, lookup).
• Typová kontrola musí ošetriť aj prípad, keď výsledok neexistuje.
• Jazyk zostáva čisto funkcionálny – žiadne vedľajšie účinky ani výnimky.