Súčtové typy

Uvažujme funkciu, ktorá podľa identifikátora tovaru vyhľadá počet kusov na sklade. Pri existujúcom zázname má výsledok obsahovať prirodzené číslo; ak záznam neexistuje, potrebuje oznámiť neprítomnosť údaja. Číslo $0$ nemôžeme použiť ako jednoznačné označenie nenájdeného záznamu, pretože je aj platným počtom kusov.

Tieto dva výsledky môžeme reprezentovať súčtovým typom $\mathsf{Nat}+\mathsf{Unit}$. Jedna alternatíva obsahuje nájdený počet kusov, druhá oznamuje neprítomnosť záznamu. Už zavedený typ $\mathsf{Unit}$ má jedinú hodnotu, takže v druhej alternatíve nepotrebujeme prenášať ďalší údaj. Rozhodujúce je označenie alternatívy: prítomná nula a neprítomný záznam sú odlišné hodnoty výsledného typu.

Nech $\Gamma\vdash t_1:\mathsf{Nat}$ a $\Gamma\vdash t_2:\mathsf{Bool}$. Potom môžeme odvodiť:

$$ \Gamma\vdash\mathsf{inl}\ t_1:\mathsf{Nat}+\mathsf{Bool}, \qquad \Gamma\vdash\mathsf{inr}\ t_2:\mathsf{Nat}+\mathsf{Bool}. $$

Ide o termy súčtového typu, nie o samotné termy typov $\mathsf{Nat}$ a $\mathsf{Bool}$. Zatiaľ používame neanotované injekcie; problém určenia druhej zložky typu vysvetlíme nižšie.

Zátvorky doplníme podľa priority a pravej asociativity šípky. Znak $=$ tu porovnáva dva zápisy toho istého syntaktického typu:

$$ \begin{aligned} A\to B\to C&=A\to(B\to C),\\ A\times B+C&=(A\times B)+C,\\ A\times B+C\to D&=((A\times B)+C)\to D,\\ A\times B\to C+D&=(A\times B)\to(C+D). \end{aligned} $$

Naproti tomu pri zmene vnorenia píšeme iba izomorfizmus:

$$ A\times(B\times C)\cong(A\times B)\times C, \qquad A+(B+C)\cong(A+B)+C. $$

Napríklad prevod

$$\lambda p:A\times(B\times C).\langle\langle p.1,(p.2).1\rangle,(p.2).2\rangle$$

zmení pravé vnorenie dvojíc na ľavé. Zátvorky teda menia štruktúru typu, hoci množstvo prenášaných údajov zostáva rovnaké.

Funkcia $\mathsf{getnat}:(\mathsf{Nat}+\mathsf{Bool})\to\mathsf{Nat}$ rozlišuje dve alternatívy vstupu. Pri ľavej injekcii vráti uložené číslo; pri pravej vráti $1$ pre $\mathsf{true}$ a $0$ pre $\mathsf{false}$.

Overte typovú korektnosť a vyhodnoťte aplikáciu

$$\mathsf{getnat}\;(\mathsf{inr}\ \mathsf{true}\ \mathsf{as}\ (\mathsf{Nat}+\mathsf{Bool})), $$

kde

$$ \begin{array}{rll} \mathsf{getnat}=\lambda x:\mathsf{Nat}+\mathsf{Bool}. &\mathsf{case}\ x\ \mathsf{of}&\\ &\mathsf{inl}\ n&\Rightarrow n\\ \mid&\mathsf{inr}\ b&\Rightarrow\mathsf{if}\ b\ \mathsf{then}\ 1\ \mathsf{else}\ 0. \end{array} $$

Riešenie – typová kontrola:

Vyhodnotenie. Argument je už hodnotou, preto najprv dosadíme za $x$, potom vyberieme pravú vetvu a dosadíme $\mathsf{true}$ za $b$:

$$ \begin{aligned} &\mathsf{getnat}\;(\mathsf{inr}\ \mathsf{true}\ \mathsf{as}\ (\mathsf{Nat}+\mathsf{Bool}))\\ &\to\mathsf{case}\ (\mathsf{inr}\ \mathsf{true}\ \mathsf{as}\ (\mathsf{Nat}+\mathsf{Bool}))\ \mathsf{of}\\ &\qquad\mathsf{inl}\ n\Rightarrow n \mid\mathsf{inr}\ b\Rightarrow\mathsf{if}\ b\ \mathsf{then}\ 1\ \mathsf{else}\ 0 &&{\scriptstyle(\text{E-AppAbs})}\\ &\to\mathsf{if}\ \mathsf{true}\ \mathsf{then}\ 1\ \mathsf{else}\ 0 &&{\scriptstyle(\text{E-CaseInr})}\\ &\to1&&{\scriptstyle(\text{E-IfTrue})}. \end{aligned} $$

V každom kroku zostáva typ $\mathsf{Nat}$. Anotácia je súčasťou injekčnej hodnoty; pri výbere vetvy sa spotrebuje celá injekcia.

V OCamli použijeme konštruktory Inl, Inr a výraz match:

type nat_or_bool = Inl of int | Inr of bool

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

# getnat (Inr true);;
- : int = 1
# getnat (Inr false);;
- : int = 0
# getnat (Inl 5);;
- : int = 5

Typ int nie je doslovne formálny typ $\mathsf{Nat}$: pripúšťa aj záporné čísla a má obmedzený rozsah. Pri tomto príklade ho používame ako praktickú reprezentáciu nezáporných čísel. OCaml navyše poskytuje vlastné pravidlá deklarácií a odvodzovania typov; explicitné as z nášho kalkulu preto neprepisujeme do jeho syntaxe.

Pre $n=3$ a term $t:[a:T_1,b:T_2,c:T_3]$ sa indexová schéma rozvinie na tri vetvy:

$$ \begin{alignedat}{2} &\mathsf{case}\ t\ \mathsf{of}\\ &\quad\phantom{\mid}\;[a=x]&\;&\Rightarrow t_1\\ &\quad\mathord{\mid}\;[b=y]&\;&\Rightarrow t_2\\ &\quad\mathord{\mid}\;[c=z]&\;&\Rightarrow t_3. \end{alignedat} $$

Ide o konkrétnu inštanciu všeobecnej schémy, nie o nový druh selektora. V príslušných vetvách majú viazané premenné typy $x:T_1$, $y:T_2$ a $z:T_3$; všetky tri telá musia mať rovnaký výsledný typ.

Variantový typ použijeme na reprezentáciu geometrických tvarov: bodu, kruhu a obdĺžnika. Pre tento príklad predpokladáme rozšírenie $\mathcal{B}$ o vstavaný typ $\mathsf{Float}$, jeho číselné hodnoty, porovnávanie a aritmetické operácie. Čísla zapisujeme s desatinnou bodkou. Symbol $\pi_{\mathsf{Float}}$ označuje aproximáciu $\pi$ v tomto type, zodpovedajúcu Float.pi v OCamli.

Typové skratky sú:

$$ \begin{aligned} \mathsf{Suradnica}&=\mathsf{Float}\times\mathsf{Float},\\ \mathsf{Tvar}&=\begin{alignedat}[t]{2} &[\mathsf{bod}&\;&:\mathsf{Suradnica},\\ &\phantom{[}\mathsf{kruh}&\;&:\mathsf{Suradnica}\times\mathsf{Float},\\ &\phantom{[}\mathsf{obdl}&\;&:\mathsf{Suradnica}\times\mathsf{Suradnica}]. \end{alignedat} \end{aligned} $$

Bod nesie súradnice. Kruh nesie dvojicu stredu a nezáporného polomeru. Obdĺžnik je určený dvojicou protiľahlých rohov; obvykle uvádzame dolný ľavý a horný pravý roh. Samotný typ podmienku nezáporného polomeru ani poradie rohov nevynucuje.

Zložky sú vnorené binárne súčiny. Pre $o:\mathsf{Suradnica}\times\mathsf{Suradnica}$ sú $o.1$ a $o.2$ súradnice rohov; $(o.1).1$ je prvá súradnica prvého rohu. Pre $k:\mathsf{Suradnica}\times\mathsf{Float}$ je $k.1$ stred a $k.2$ polomer.

Funkcia pre výpočet obsahu. Najprv definujeme absolútnu hodnotu:

$$ \begin{aligned} \mathsf{abs}&:\mathsf{Float}\to\mathsf{Float},\\ \mathsf{abs}&=\lambda x:\mathsf{Float}.\ \mathsf{if}\ x<0.0\ \mathsf{then}\ 0.0-x\ \mathsf{else}\ x. \end{aligned} $$

Potom definujeme obsah pomocou úplného rozboru troch alternatív:

$$ \begin{aligned} \mathsf{obsah}&:\mathsf{Tvar}\to\mathsf{Float},\\ \mathsf{obsah}&=\lambda x:\mathsf{Tvar}.\mathsf{case}\ x\ \mathsf{of}\\ &\quad\begin{alignedat}[t]{2} &\phantom{\mid}\;[\mathsf{bod}=b]&\;&\Rightarrow0.0\\ &\mathord{\mid}\;[\mathsf{kruh}=k]&\;&\Rightarrow\pi_{\mathsf{Float}}\cdot k.2\cdot k.2\\ &\mathord{\mid}\;[\mathsf{obdl}=o]&\;&\Rightarrow \begin{aligned}[t] &\mathsf{abs}\;((o.1).1-(o.2).1)\\ &\quad\cdot\mathsf{abs}\;((o.1).2-(o.2).2). \end{aligned} \end{alignedat} \end{aligned} $$

Bod má nulový obsah, kruh obsah $\pi r^2$ a obdĺžnik súčin dĺžok strán. Všetky tri vetvy majú typ $\mathsf{Float}$. Absolútne hodnoty pri obdĺžniku umožňujú zadať protiľahlé rohy aj v opačnom poradí.

Funkcia pre výpočet stredu:

$$ \begin{aligned} \mathsf{stred}&:\mathsf{Tvar}\to\mathsf{Suradnica},\\ \mathsf{stred}&=\lambda x:\mathsf{Tvar}.\mathsf{case}\ x\ \mathsf{of}\\ &\quad\begin{alignedat}[t]{2} &\phantom{\mid}\;[\mathsf{bod}=b]&\;&\Rightarrow b\\ &\mathord{\mid}\;[\mathsf{kruh}=k]&\;&\Rightarrow k.1\\ &\mathord{\mid}\;[\mathsf{obdl}=o]&\;&\Rightarrow \left\langle\frac{(o.1).1+(o.2).1}{2.0}, \frac{(o.1).2+(o.2).2}{2.0}\right\rangle. \end{alignedat} \end{aligned} $$

Pre bod vraciame jeho súradnice, pre kruh uložený stred. Stred obdĺžnika získame priemerom zodpovedajúcich súradníc rohov. Každá vetva má typ $\mathsf{Suradnica}$. Znamienko $=$ zavádza definíciu funkcie, zatiaľ čo dvojbodka uvádza jej typ.

OCaml implementácia používa rovnaké alternatívy a vzorce:

type suradnica = float * float
type tvar =
  | Bod of suradnica
  | Kruh of suradnica * float
  | Obdl of suradnica * suradnica

let obsah : tvar -> float = function
  | Bod _ -> 0.0
  | Kruh (_, r) -> Float.pi *. r *. r
  | Obdl ((x1, y1), (x2, y2)) ->
      let w = abs_float (x2 -. x1) in
      let h = abs_float (y2 -. y1) in
      w *. h

let stred : tvar -> suradnica = function
  | Bod p -> p
  | Kruh (p, _) -> p
  | Obdl ((x1, y1), (x2, y2)) ->
      ((x1 +. x2) /. 2.0, (y1 +. y2) /. 2.0)

# obsah (Kruh ((0.0, 0.0), 2.0));;
- : float = 12.5663706143591725
# obsah (Obdl ((0.0, 0.0), (3.0, 4.0)));;
- : float = 12.
# stred (Obdl ((0.0, 0.0), (3.0, 4.0)));;
- : suradnica = (1.5, 2.)

Číselný výstup pri kruhu je aproximácia. V OCamli používame operátory *., -., +. a /. pre float; vo formálnom príklade im zodpovedajú predpokladané operácie na $\mathsf{Float}$. Varianty umožňujú spojiť rôzne reprezentácie tvarov do jedného typu a pre každú alternatívu bezpečne sprístupniť jej údaje.

Typ reprezentujúci dni v týždni je možné definovať ako enumeračný typ:

$$ \begin{aligned} \mathsf{Week}=[\;&monday:\mathsf{Unit},\\ &tuesday:\mathsf{Unit},\\ &wednesday:\mathsf{Unit},\\ &thursday:\mathsf{Unit},\\ &friday:\mathsf{Unit},\\ &saturday:\mathsf{Unit},\\ &sunday:\mathsf{Unit}\;]. \end{aligned} $$

Napríklad pondelok reprezentuje hodnota:

$$ [ monday = \mathsf{unit}]~\mathsf{as}\ \mathsf{Week} $$

Keďže typ $\mathsf{Unit}$ má jedinú hodnotu unit, typ $\mathsf{Week}$ má presne 7 hodnôt, zodpovedajúcich dňom v týždni.

Obsahom každej alternatívy je jediná hodnota $\mathsf{unit}$; jednotlivé dni rozlišuje návestie.

K termom enumeračného typu $\mathsf{Week}$ je možné pristupovať prostredníctvom selektora case.

Majme funkciu, ktorá pre argument $ w : \mathsf{Week} $ vráti nasledujúci pracovný deň v týždni:

$$ \begin{aligned} \mathsf{nextWorkDay}&:\mathsf{Week}\to\mathsf{Week},\\ \mathsf{nextWorkDay} &= \lambda w: \mathsf{Week}. \\ &\quad \mathsf{case}~w~\mathsf{of} \\ &\quad\quad ~~~[monday = x] \Rightarrow [tuesday = \mathsf{unit}]~\mathsf{as}\ \mathsf{Week} \\ &\quad\quad \mid~[tuesday = x] \Rightarrow [wednesday = \mathsf{unit}]~\mathsf{as}\ \mathsf{Week} \\ &\quad\quad \mid~[wednesday = x] \Rightarrow [thursday = \mathsf{unit}]~\mathsf{as}\ \mathsf{Week} \\ &\quad\quad \mid~[thursday = x] \Rightarrow [friday = \mathsf{unit}]~\mathsf{as}\ \mathsf{Week} \\ &\quad\quad \mid~[friday = x] \Rightarrow [monday = \mathsf{unit}]~\mathsf{as}\ \mathsf{Week} \\ &\quad\quad \mid~[saturday = x] \Rightarrow [monday = \mathsf{unit}]~\mathsf{as}\ \mathsf{Week} \\ &\quad\quad \mid~[sunday = x] \Rightarrow [monday = \mathsf{unit}]~\mathsf{as}\ \mathsf{Week} \end{aligned} $$

Príklad použitia:

$$ \mathsf{nextWorkDay}\;([saturday = \mathsf{unit}]~\mathsf{as}\ \mathsf{Week}) \to^* [monday = \mathsf{unit}]~\mathsf{as}\ \mathsf{Week} $$

V každej vetve má $x$ typ $\mathsf{Unit}$ a nepoužije sa. Rozbor pokrýva všetkých sedem dní a všetky vetvy vracajú $\mathsf{Week}$.

Predchádzajúci príklad v jazyku OCaml:

(* 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

OCaml má pre alternatívy bez ďalšieho údaja priamo bezargumentové konštruktory Monday, …, Sunday. Na rozdiel od formálneho modelu preto nepíšeme explicitné unit.

# next_work_day Saturday;;
- : week = Monday

Pri konverzii medzi dolármi a eurami chceme zabrániť zámene dvoch súm s rovnakou číselnou reprezentáciou. Pre tento príklad predpokladáme ilustračné rozšírenie $\mathcal{B}$ o $\mathsf{Real}$ s číselnými hodnotami a aritmetikou. Operácia

$$\mathsf{times}:\mathsf{Real}\to\mathsf{Real}\to\mathsf{Real}$$

je tu primitívne násobenie reálnych čísel, nie Churchovo násobenie z druhej prednášky. Použijeme pevné ilustračné kurzy $0.8$ a $1.25$, ktoré sú navzájom prevrátené.

Najprv bez obalových typov. Ak obe meny reprezentujeme priamo typom $\mathsf{Real}$, môžeme napísať:

$$ \begin{aligned} \mathsf{dollartoeuro}&:\mathsf{Real}\to\mathsf{Real},\\ \mathsf{dollartoeuro}&=\lambda d:\mathsf{Real}.\mathsf{times}\ d\ 0.8,\\ \mathsf{eurotodollar}&:\mathsf{Real}\to\mathsf{Real},\\ \mathsf{eurotodollar}&=\lambda e:\mathsf{Real}.\mathsf{times}\ e\ 1.25,\\ \mathsf{mybalance}&=39.50. \end{aligned} $$

Po dosadení týchto definícií platí:

$$ \begin{aligned} \mathsf{eurotodollar}\;(\mathsf{dollartoeuro}\ \mathsf{mybalance})&\to^*39.50,\\ \mathsf{dollartoeuro}\;(\mathsf{dollartoeuro}\ \mathsf{mybalance})&\to^*25.28. \end{aligned} $$

Aj druhý výraz je dobre typovaný ako $\mathsf{Real}$, hoci omylom konvertuje už prepočítanú sumu znova tým istým smerom. Samotná číselná reprezentácia nerozlišuje meny.

Bezpečná verzia s obalmi. Predchádzajúce definície nahradíme funkciami pracujúcimi s dvoma rôznymi variantovými typmi:

$$ \begin{aligned} \mathsf{DollarAmount}&=[dollars:\mathsf{Real}],\\ \mathsf{EuroAmount}&=[euros:\mathsf{Real}]. \end{aligned} $$

$\mathsf{Real}$ je vnútorný číselný typ; $\mathsf{DollarAmount}$ a $\mathsf{EuroAmount}$ sú odlišné obalové typy. Ich odlišnosť v našom štrukturálnom modeli vyplýva z rôznych návestí, nie iba z rôznych názvov typových skratiek.

Bezpečné konverzie hodnotu rozbalia, prepočítajú a opäť zabalia do správnej alternatívy:

$$ \begin{aligned} \mathsf{dollartoeuro}&=\lambda d:\mathsf{DollarAmount}.\ \mathsf{case}\ d\ \mathsf{of}\\ &\qquad[dollars=x]\Rightarrow [euros=\mathsf{times}\ x\ 0.8]\ \mathsf{as}\ \mathsf{EuroAmount},\\ \mathsf{eurotodollar}&=\lambda e:\mathsf{EuroAmount}.\ \mathsf{case}\ e\ \mathsf{of}\\ &\qquad[euros=x]\Rightarrow [dollars=\mathsf{times}\ x\ 1.25]\ \mathsf{as}\ \mathsf{DollarAmount}. \end{aligned} $$

Majú typy:

$$ \begin{aligned} \mathsf{dollartoeuro}&:\mathsf{DollarAmount}\to\mathsf{EuroAmount},\\ \mathsf{eurotodollar}&:\mathsf{EuroAmount}\to\mathsf{DollarAmount}. \end{aligned} $$

V oboch rozboroch má $x$ typ $\mathsf{Real}$. Injekcia výsledku určuje príslušný obalový typ. Pre

$$\mathsf{mybalance}=[dollars=39.50]\ \mathsf{as}\ \mathsf{DollarAmount}$$

dostaneme tieto výpočty:

$$ \begin{aligned} \mathsf{dollartoeuro}\ \mathsf{mybalance} &\to^*[euros=31.60]\ \mathsf{as}\ \mathsf{EuroAmount},\\ \mathsf{eurotodollar}\;(\mathsf{dollartoeuro}\ \mathsf{mybalance}) &\to^*[dollars=39.50]\ \mathsf{as}\ \mathsf{DollarAmount}. \end{aligned} $$

Výsledok spätnej konverzie má typ $\mathsf{DollarAmount}$ a zostáva zabalený, nie je neobaleným číslom typu $\mathsf{Real}$. Pri volaní hodnotou sa po výbere vetvy najprv vypočíta násobenie v obsahu variantu; až potom vznikne variantová hodnota.

Výraz

$$\mathsf{dollartoeuro}\;(\mathsf{dollartoeuro}\ \mathsf{mybalance})$$

neprejde typovou kontrolou. Vnútorná aplikácia má typ $\mathsf{EuroAmount}$, ale vonkajšia očakáva $\mathsf{DollarAmount}$, takže nemožno použiť T-App. Typová chyba je neúspech statickej kontroly; nepíšeme ju ako výsledok vyhodnocovacej relácie $\to$.

OCaml implementácia:

type dollar_amount = Dollar of float
type euro_amount = Euro of float

let times x y = x *. y

let dollartoeuro (Dollar d) =
  Euro (times d 0.8)

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

let mybalance = Dollar 39.50

# dollartoeuro mybalance;;
- : euro_amount = Euro 31.6
# eurotodollar (dollartoeuro mybalance);;
- : dollar_amount = Dollar 39.5
# dollartoeuro (dollartoeuro mybalance);;
Error: This expression has type euro_amount
       but an expression was expected of type dollar_amount

OCaml rozlišuje deklarované typy dollar_amount a euro_amount a odmietne rovnakú zámenu. Typ float je iba konečná aproximácia formálneho $\mathsf{Real}$; presnosť finančných výpočtov je samostatná otázka. Obaly tu ilustrujú ochranu pred zámenou mien, nie spôsob reprezentácie presnej peňažnej aritmetiky.

Ak chceme v OCamli verne reprezentovať prirodzené čísla pomocou nuly a nasledovníka, môžeme použiť tieto deklarácie:

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

Typ natoption zodpovedá konkrétnemu $\mathsf{OptionNat}$. Some (S Zero) obsahuje prirodzenú jednotku, None označuje neprítomnosť údaja. Ide o OCaml reprezentáciu; deklaráciou rekurzívneho typu nat nemeníme formálnu syntax nášho kalkulu. V bežnom OCaml programe môžeme namiesto vlastného natoption použiť vstavaný typ nat option.

Tabuľku s číselnými indexmi môžeme reprezentovať funkciou:

$$\mathsf{Table}=\mathsf{Nat}\to\mathsf{OptionNat}.$$

Je definovaná pre každý index. Výsledok má jednu z foriem

$$ [some=n]\ \mathsf{as}\ \mathsf{OptionNat} \quad\text{alebo}\quad [none=\mathsf{unit}]\ \mathsf{as}\ \mathsf{OptionNat}. $$

Anotácia patrí typu výsledku $\mathsf{OptionNat}$, nie funkčnému typu $\mathsf{Table}$. Z typu $\mathsf{Table}$ nevyplýva konečný počet prítomných záznamov: napríklad $\lambda k:\mathsf{Nat}.[some=k]\ \mathsf{as}\ \mathsf{OptionNat}$ má hodnotu na každom indexe.

Ak chceme modelovať konečnú tabuľku, požadujeme konečnú podporu, teda iba konečne veľa indexov s výsledkom some. Konkrétna tabuľka s jediným záznamom $0\mapsto7$ je:

$$ \begin{aligned} \mathsf{table}&:\mathsf{Table},\\ \mathsf{table}&=\lambda k:\mathsf{Nat}.\ \mathsf{if}\ \mathsf{iszero}\ k\\ &\quad\mathsf{then}\ [some=7]\ \mathsf{as}\ \mathsf{OptionNat}\\ &\quad\mathsf{else}\ [none=\mathsf{unit}]\ \mathsf{as}\ \mathsf{OptionNat}. \end{aligned} $$

Vyhľadávanie je iba aplikáciou tabuľky na index:

$$ \begin{aligned} \mathsf{lookup}&:\mathsf{Nat}\to\mathsf{Table}\to\mathsf{OptionNat},\\ \mathsf{lookup}&=\lambda k:\mathsf{Nat}.\lambda t:\mathsf{Table}.t\ k. \end{aligned} $$

V tele platí podľa T-App:

$$k:\mathsf{Nat},t:\mathsf{Nat}\to\mathsf{OptionNat}\vdash t\ k:\mathsf{OptionNat}.$$

Dve použitia T-Abs dajú uvedený typ. Po rozvinutí skratiek a vyhodnotení podmienky dostaneme:

$$ \begin{aligned} \mathsf{lookup}\ 0\ \mathsf{table} &\to^*[some=7]\ \mathsf{as}\ \mathsf{OptionNat},\\ \mathsf{lookup}\ 1\ \mathsf{table} &\to^*[none=\mathsf{unit}]\ \mathsf{as}\ \mathsf{OptionNat}. \end{aligned} $$

Prítomnosť údaja môžeme rozlíšiť pomocou case; tu pri chýbajúcom zázname zvolíme náhradnú hodnotu $0$:

$$ \begin{aligned} &\mathsf{case}\ (\mathsf{lookup}\ 0\ \mathsf{table})\ \mathsf{of}\\ &\qquad[none=u]\Rightarrow0\mid[some=n]\Rightarrow n\\ &\to^*\mathsf{case}\ ([some=7]\ \mathsf{as}\ \mathsf{OptionNat})\ \mathsf{of}\\ &\qquad[none=u]\Rightarrow0\mid[some=n]\Rightarrow n\\ &\to7. \end{aligned} $$

Pre index $1$ analogicky vyberieme vetvu none a dostaneme $0$. V každom rozbore má $u$ typ $\mathsf{Unit}$, $n$ typ $\mathsf{Nat}$ a obe telá typ $\mathsf{Nat}$.

V nasledujúcej OCaml verzii použijeme pre stručnosť int a vstavaný int option. Indexy a uložené čísla budeme používať iba nezáporné; obmedzenie na prirodzené čísla samotný int nevynucuje.

type table = int -> int option

let table : table = fun k ->
  if k = 0 then Some 7 else None

let lookup (k : int) (t : table) : int option = t k

let value_or_zero (result : int option) : int =
  match result with
  | None -> 0
  | Some n -> n

# lookup 0 table;;
- : int option = Some 7
# lookup 1 table;;
- : int option = None
# value_or_zero (lookup 0 table);;
- : int = 7
# value_or_zero (lookup 1 table);;
- : int = 0

Výsledok Some 0 by bol prítomným záznamom s hodnotou nula; None je chýbajúci záznam. Až funkcia value_or_zero ich zámerne prevedie na rovnakú náhradnú číselnú hodnotu. Samotný typ option tieto prípady rozlišuje.