i
i
“Koprivec” — 2017/9/21 — 9:24 — page 81 — #1 i
i
i
i
i
i
TIPI V PROGRAMSKIH JEZIKIH IN IZREKI O
VARNOSTI PROGRAMOV
FILIP KOPRIVEC
Fakulteta za matematiko in fiziko
Univerza v Ljubljani
Math. Subj. Class. (2010): 68Q55, 68Q60, 68N18
Eno izmed pomembneǰsih orodij v programiranju so zagotovo tipi, saj nam omogočajo,
da že pred zagonom programa preprečimo določeno vrsto napak. V članku si na primeru
preprostega programskega jezika najprej ogledamo pravila sintakse in izvajanja, nato pa
zanj dokažemo izrek o varnosti, ki nam s pomočjo tipov zagotavlja, da bo med izvajanjem
programa njegovo stanje vedno smiselno. Na kratko predstavimo tudi lambda račun z
enostavnimi tipi in njemu pripadajoči izrek o varnosti.
TYPES IN PROGRAMMING LANGUAGES AND CORRESPONDING
SAFETY THEOREMS
One of the most important tools in programming is definitely the type system, which
allows us to eliminate a whole class of errors before the actual evaluation of the program
even takes place. This article presents a simple programming language which is used to
examine syntax and evaluation rules, and proceeds with proving a safety theorem which
uses types to ensure that the program state will stay sound during the execution. Simply
typed lambda calculus and the corresponding safety theorem are presented at the end.
Uvod
Najpomembneǰsa lastnost večine programov je zagotovo pravilnost. Da bi
zagotovili pravilnost programa, si pomagamo z mnogo različnimi pristopi in
orodji, ki imajo različne prednosti in slabosti. Eno izmed preprosteǰsih, a
vseeno zelo močnih orodij, so tipi. S pomočjo tipov lahko vnaprej preprečimo
nekatera stanja, ki bi utegnila privesti do napake v izvajanju.
Teoretično osnovo pri delu s tipi nam daje izrek o varnosti, ki zagotovi,
da med izvajanjem programa s tipi ne bo prǐslo do napake. Izrek o varnosti
si bomo ogledali na preprostem programskem jeziku, na koncu pa bomo na
kratko omenili, kako lahko to posplošimo tudi na funkcije.
Sintaksa
Običajno jezike podamo z različico Backus-Naurove (BNF) oblike zapisa.
Jezik oziroma množico izrazov, ki jih označujemo s sintaktično spremen-
ljivko t, definiramo tako, da naštejemo vse možne oblike izrazov, ki jih med
Obzornik mat. fiz. 64 (2017) 3 81
i
i
“Koprivec” — 2017/9/21 — 9:24 — page 82 — #2 i
i
i
i
i
i
Filip Koprivec
seboj ločimo z »|«. Če v zapisu nastopa t (ali t1, t2, t3), to pomeni, da na-
mesto t lahko vstavimo poljuben veljaven izraz, kar nam omogoči, da nove
izraze dobimo s kombiniranjem že obstoječih. Sintaksa jezika je prikazana
v tabeli 1.
izraz t ::= true
∣∣ false ∣∣ n ∣∣ succ t ∣∣ pred t ∣∣ iszero t∣∣ if t1 then t2 else t3
Tabela 1. Osnovna sintaksa.
Po pravilih sintakse naš jezik vsebuje: logični konstanti za resnico in
neresnico ter konstanto za vsako celo število n. S črto pod številom ozna-
čimo, da gre za izraz, ki pomeni to število (0 je izraz, ki pomeni število 0).
Obstoječe izraze pa uporabimo pri gradnji novih izrazov. Jezik vsebuje še
funkciji, ki vrneta naslednika in predhodnika poljubnega drugega izraza t,
in predikat, ki pove, ali je izraz t enak izrazu, ki pomeni število 0. Vsebuje
pa tudi pogojni stavek, ki je sestavljen iz treh delov: pogoja, rezultata, če
je pogoj izpolnjen, in rezultata, če pogoj ni izpolnjen.
Primer 1. Intuitivno idejo jezika si je najlažje ogledati kar na primeru.
Definirani jezik je sicer zelo šibak, a vseeno lahko sestavimo izraz, ki preveri,
ali izraz t pomeni število 0 ali 1.
if (iszero t) then true else (iszero (pred t)) (1)
Definiramo preprost pogojni stavek, ki bo tedaj, ko je pogoj izpolnjen (če
izraz t pomeni število 0), vrnil logično konstanto za resnico, če pogoj ne bo
izpolnjen, pa vrednost funkcije iszero (pred t), torej logično konstanto, ki
pove, ali predhodnik izraza t pomeni število 0 ali ne.
Izvajanje
Pravila izvajanja za naš jezik so podana v tabeli 2. Njihova imena se začno
s črko E (za angl. »Execution«).
Pravila podamo z dvomestno relacijo med izrazi. Pǐsemo t  t′ in be-
remo: t se pretvori v t′. Rečemo, da je semantika malih korakov najmanǰsa
dvomestna relacija na izrazih, ki ustreza pravilom za izvajanje. Relacija za-
došča pravilu za izvajanje, če za vsak primer tega pravila velja, da je bodisi
izpolnjen zaključek tega pravila bodisi predpostavke niso izpolnjene. Pred-
stavljena pravila pa potrebujejo kraǰso razlago. Najprej si oglejmo prvo,
82 Obzornik mat. fiz. 64 (2017) 3
i
i
“Koprivec” — 2017/9/21 — 9:24 — page 83 — #3 i
i
i
i
i
i
Tipi v programskih jezikih in izreki o varnosti programov
zelo preprosto pravilo:
E-IsZeroZero
iszero 0 true
.
Pravila za izvajanje so sestavljena iz dveh delov: iz dela nad vodoravno
črto (predpostavk) in dela pod črto (zaključka), ki pove, v kaj se izraz pre-
tvori. V našem primeru imamo preprosto pravilo, ki pravi, da lahko vedno
(brez dodatnih predpostavk) zaključimo, da se izraz oblike iszero 0 pre-
tvori v true. Ime pravila služi lažjemu sklicevanju na pravilo. Sestavljena
pravila, kot na primer E-Succ, razumemo tako: »Če se izraz t pretvori v
t′, potem lahko sklepamo, da se izraz oblike succ t pretvori v succ t′«.
Primer 2. V izraz (1) iz primera 1 vstavimo t = 0 in pogledamo potek
izvajanja. Pri izpeljavi izvajanja si pomagamo z drevesom izvajanja, saj
izraz razdelimo na manǰse koščke, dokler ne pridemo do pravil za izvajanje.
Za izraz (1) najprej uporabimo pravilo E-If, za katero moramo izvesti izraz
iszero 0, zanj pa velja pravilo E-IsZeroZero. Začetni izraz se pretvori v
if true then true else (iszero (pred 0)). Če bi zanj izvedli še en korak,
E-IsZeroZero
iszero 0 true
E-IsZeroNonZero
(n 6= 0)
iszero n false
E-IsZero
t t′
iszero t iszero t′
E-PredNum
pred n n− 1
E-Pred
t t′
pred t pred t′
E-SuccNum
succ n n+ 1
E-Succ
t t′
succ t succ t′
E-IfTrue
if true then t2 else t3  t2
E-IfFalse
if false then t2 else t3  t3
E-If
t1  t
′
1
if t1 then t2 else t3  if t
′
1 then t2 else t3
Tabela 2. Pravila za izvajanje.
81–90 83
i
i
“Koprivec” — 2017/9/21 — 9:24 — page 84 — #4 i
i
i
i
i
i
Filip Koprivec
bi se po pravilu E-IfTrue izvedel v vrednost true. Izpeljavi ustreza drevo
spodaj:
E-If
E-IsZeroZero
iszero 0 true
if (iszero 0) then true else (iszero (pred 0)) 
 if true then true else (iszero (pred 0)) .
Če pa se lotimo izvajanja izraza if 0 then 0 else (iszero 0), naletimo
na težavo, saj za izvajanje izraza if 0 then t1 else t2 nimamo pravila.
Definicija 3 (normalna oblika). Izrazom, ki nimajo ustreznega pravila
za izvajanje, rečemo, da so v normalni obliki.
Očitno so v normalni obliki vse konstante oblike true, false, n.
Definicija 4 (vrednost). Konstantam true, false in n rečemo vrednosti
in jih označimo s sintaktično spremenljivko v:
vrednost v ::= true
∣∣ false ∣∣ n.
Preostali izrazi v normalni obliki so nezaželeni in jih razglasimo za na-
pačne.
Definicija 5 (zataknjen izraz). Za izraz, ki je v normalni obliki, a ni
vrednost, pravimo, da je zataknjen.
Primer 6. Zelo preprost zataknjen izraz je tudi iszero true.
Tipi
Kot smo videli, lahko zapǐsemo sintaktično pravilne izraze, ki se zataknejo.
Zanima nas, ali lahko že vnaprej ugotovimo, kateri izrazi se med izvajanjem
ne morejo zatakniti, pri tem pa si bomo pomagali s tipi.
Najprej v tabeli 3 definiramo dva osnovna tipa, celo število (Int) in Boo-
leovo vrednost (Bool), nato v tabeli 4 predstavimo pravila za dodeljevanje
tipov.
Rečemo, da ima izraz t tip T , če obstaja tak T , da je par (t, T ) v relaciji
ima tip; po pravilih sintakse pǐsemo t : T . Relacijo imeti tip formalno
predstavimo kot najmanǰso binarno relacijo med izrazi in tipi, ki zadošča
vsem pravilom za tipe.
Pravila za izpeljavo tipov beremo podobno kot pravila za izvajanje. Za
primer delovanja si oglejmo pravilo za T-IsZero. Če velja, da je t tipa Int,
potem je iszero t tipa Bool; z oznako: iszero t : Bool.
84 Obzornik mat. fiz. 64 (2017) 3
i
i
“Koprivec” — 2017/9/21 — 9:24 — page 85 — #5 i
i
i
i
i
i
Tipi v programskih jezikih in izreki o varnosti programov
tip T ::= Int
∣∣ Bool
Tabela 3. Osnovni tipi.
T-True
true : Bool
T-False
false : Bool
T-Num
n : Int
T-Succ
t : Int
succ t : Int
T-Pred
t : Int
pred t : Int
T-IsZero
t : Int
iszero t : Bool
T-If
t1 : Bool t2 : T t3 : T
if t1 then t2 else t3 : T
.
Tabela 4. Pravila za tipe.
Oglejmo si še pogojni stavek. Za izpeljavo tipa pogojnega stavka potre-
bujemo tri predpostavke: pogoj mora imeti tip Bool, rezultata t2 in t3 pa
morata imeti isti tip T . Iz teh predpostavk lahko sklepamo, da ima izraz
tip T (enak tipu obeh rezultatov).
Primer 7. Oglejmo si še primer izpeljave tipa nekoliko večjega izraza. Če
želimo izpeljati, da ima celoten izraz pod črto tip Int, moramo najprej
ugotoviti, kakšne tipe imajo posamezni izrazi v pogojnem stavku. V pogoju
imamo izraz iszero 0, katerega tip lahko izpeljemo, če vemo, kakšen je tip
0. To je konstanta, po pravilu T-Num velja 0 : Int, iz česar po T-IsZero
velja iszero 0 : Bool, kar izpolni prvi pogoj za izpeljavo tipa po pravilu
T-If. Podobno izpeljemo tudi, da velja succ 0 : Int in 0 : Int, potem pa
uporabimo pravilo T-If in dobimo, da ima celoten izraz tip Int.
T-If
T-IsZero
T-Num
0 : Int
iszero 0 : Bool
T-Succ
T-Num
0 : Int
succ 0 : Int 0 : Int
T-Num
if (iszero 0) then (succ 0) else 0 : Int .
Izreki o varnosti
Ena izmed osnovnih lastnosti programov, ki jo zagotavljajo tipi, je varnost.
Za izraz, ki ima tip, lahko zagotovimo, da se med izvajanjem ne bo zataknil.
Formalno to predstavimo (in dokažemo) z dvema izrekoma: z izrekom o
napredku in izrekom o ohranitvi.
81–90 85
i
i
“Koprivec” — 2017/9/21 — 9:24 — page 86 — #6 i
i
i
i
i
i
Filip Koprivec
Izrek 8 (izrek o napredku). Izraz t, ki ima tip, ni zataknjen. Torej je t
vrednost ali pa obstaja tak izraz t′, ki ima tip in zanj velja t t′.
Dokaz. Naj bo t izraz, ki ima tip T (t : T ). Glede na zadnje uporabljeno
pravilo za izpeljavo tipa izraza bomo obravnavali več možnosti. Uporabili
bomo strukturno indukcijo, ki deluje podobno kot matematična indukcija,
le da na vsakem koraku predpostavimo veljavnost indukcijske predpostavke
za vse prave podizraze izraza t. Pogledali bomo zgolj nekaj primerov, saj se
preostale dokaže podobno.
• Možnosti T-True, T-False, T-Num:
Dokaz lahko dokončamo takoj, saj so izrazi kar vrednosti.
• Možnost T-Pred:
Po predpostavki izreka imamo izraz oblike t = pred t1, za katerega
velja t1 : Int. Po indukcijski predpostavki je t1 ali vrednost ali pa se
lahko izvede v t′1.
Poglejmo najprej primer, ko je t1 vrednost. Ker velja t1 : Int, je torej
t1 numerična vrednost in je oblike n za neko celo število n (v primeru
t1 = true ali t1 = false bi bilo to v nasprotju z dejstvom, da velja
t1 : Int). Izraz t v tem primeru lahko opravi korak v izvajanju, saj se
po E-PredNum pretvori v n− 1.
Če pa t1 ni vrednost, po indukcijski predpostavki obstaja tak t
′
1, da
velja t1  t′1, v tem primeru pa za t velja pravilo E-Pred in dobimo:
pred t1  pred t
′
1
oziroma
t t′,
kjer je t′ = pred t′1.
• Možnosti T-Succ in T-IsZero:
Dokaz je zelo podoben dokazu za T-Pred in ga ne bomo ponavljali.
• Možnost T-If:
Po predpostavki izreka imamo izraz oblike
t = if t1 then t2 else t3, za katerega velja: t1 : Bool, t2 : T, t3 : T .
Po indukcijski predpostavki je torej t1 ali vrednost ali pa se lahko pre-
tvori v t′1. Če je t1 vrednost, in ker velja t1 : Bool, je t1 lahko zgolj
true ali false. Sledi, da za celoten izraz t obstaja pravilo za izvajanje
(v prvem primeru E-IfTrue, v drugem pa E-IfFalse). Če pa t1 ni
86 Obzornik mat. fiz. 64 (2017) 3
i
i
“Koprivec” — 2017/9/21 — 9:24 — page 87 — #7 i
i
i
i
i
i
Tipi v programskih jezikih in izreki o varnosti programov
vrednost, po indukcijski predpostavki obstaja tak t′1, da velja t1  t
′
1,
v tem primeru pa se izraz t po pravilu E-If izvede v:
if t1 then t2 else t3  if t
′
1 then t2 else t3.
Izrek 9 (izrek o ohranitvi). Če izraz tipa T lahko opravi korak v izvaja-
nju, je tudi rezultat izvajanja tipa T . Torej iz t : T in t t′ sledi t′ : T .
Dokaz. Kot izrek o napredku bomo tudi izrek o ohranitvi dokazali induk-
tivno glede na izpeljavo tipov z upoštevanjem možnosti, ki nastopajo v
pravilih za tipe.
• Možnost T-True:
Po predpostavki izreka imamo izraz oblike true : Bool.
Ker se true ne more več izvesti, je pogoj izreka izpolnjen na prazno.
• Možnosti T-False in T-Num:
Dokaz je analogen dokazu za T-True.
• Možnost T-Pred:
Po predpostavki izreka imamo izraz oblike t = pred t1, za katerega
velja t1 : Int.
Izraz pred t1 se v izvajanju pojavi v natanko dveh primerih: E-PredNum
in E-Pred.
– Primer E-PredNum:
Velja t1 = n za neko celo število n. Izraz pred n se po E-PredNum
pretvori v vrednost n− 1, ki ima tip Int, torej izraz pri izvajanju
ohrani tip.
– Primer E-Pred:
Vemo, da velja t1  t′1, iz indukcijske predpostavke pa sledi, da
velja tudi t′1 : Int. Izraz t se pretvori v pred t
′
1, za kar pa po
pravilu T-Pred velja pred t′1 : Int, torej izraz ohrani tip.
• Možnosti T-Succ in T-IsZero:
Dokaz je zelo podoben dokazu za T-Pred in ga ne bomo ponavljali.
• Možnost T-If:
Po predpostavki izreka imamo izraz oblike if t1 then t2 else t3, za
katerega velja: t1 : Bool, t2 : T, t3 : T .
Pogledamo vse možnosti v izvajanju t  t′, kjer se pojavi pogojni
stavek. Temu zadoščajo tri pravila: E-IfTrue, E-IfFalse, E-If, ki
jih obravnavamo vsako posebej.
81–90 87
i
i
“Koprivec” — 2017/9/21 — 9:24 — page 88 — #8 i
i
i
i
i
i
Filip Koprivec
– Primer E-IfTrue:
Vemo, da velja t1 = true in t
′ = t2.
Ker je t′ = t2 in ker po indukcijski predpostavki velja t2 : T ,
rezultat izvajanja ohrani tip.
– Primer E-IfFalse:
Dokažemo podobno kot E-IfTrue.
– Primer E-If:
Vemo, da velja t1  t′1 in t
′ = if t′1 then t2 else t3.
Ker tokrat vemo, da ima izraz t1 tip Bool, lahko uporabimo in-
dukcijsko predpostavko in iz t1  t′1 dobimo t
′
1 : Bool. Sku-
paj s predpostavkami, da velja t2 : T in t3 : T , lahko na izrazu
if t′1 then t2 else t3 uporabimo pravilo za tipe T-If. Sledi, da
velja t′ : T , torej med izvajanjem izraz ohrani tip.
Funkcije
Za preprost programski jezik smo pokazali, kako lahko s tipi zagotovimo
varnost. Jezik pa bi radi razširili s funkcijami in si ogledali, kako lahko
sestavimo jezik, ki je sicer znan kot lambda račun z enostavnimi tipi :
izraz t ::= · · ·
∣∣ x ∣∣ λx. t ∣∣ t1 t2.
Sintakso jezika dopolnimo, da omogoča definicijo in uporabo funkcij.
Izraz je sedaj lahko poljuben že prej veljaven izraz, lahko pa je tudi spre-
menljivka. Še pomembneǰsi pa sta zadnji dve možnosti. S prvo definiramo
funkcijo (abstrakcijo), ki spremenljivki x priredi izraz t (tu pravimo, da je
x vezan v tej abstrakciji), z drugo pa uporabo prvega izraza (funkcije) na
drugem izrazu. Vzemimo npr. izraz
λx. iszero x. (2)
V izrazu (2) definiramo preprosto abstrakcijo, ki spremenljivki x priredi
izraz iszero x. Ideja je popolnoma enaka definiciji funkcije v matematiki,
le da uporabimo nekoliko drugačen zapis. Enako je z uporabo funkcije na
izrazu.
Primer 10.
(λx. iszero x) 0. (3)
V izrazu (3) abstrakcijo iz izraza (2) uporabimo na izrazu, ki pomeni šte-
vilo 0. V izvajanju bi, kot pri običajni funkciji, vse nastope x v prvotnem
izrazu zamenjali z 0 in dobili izraz iszero 0. Substitucijo spremenjivke x z
izrazom y v izrazu t zapǐsemo kot: [x 7→ y]t, pri substituciji pa pazimo, da
88 Obzornik mat. fiz. 64 (2017) 3
i
i
“Koprivec” — 2017/9/21 — 9:24 — page 89 — #9 i
i
i
i
i
i
Tipi v programskih jezikih in izreki o varnosti programov
ne zamenjamo nastopov spremenljivke x, ki je vezana v kateri izmed bolj
notranjih abstrakcij izraza t.
Funkcije pa lahko vračajo tudi nove funkcije. Izraz (4) dani funkciji
priredi novo funkcijo, ki prvo funkcijo uporabi dvakrat:
λx1. (λx2. x1 (x1 x2)). (4)
Pravilom za izvajanje zato dodamo še tri pravila: prvo pove, kako se
pretvori prvi izraz, ki nastopa v uporabi funkcije; drugo, kako se pretvori
argument abstrakcije; tretje pa, kako uporabimo abstrakcijo. Ustrezno po-
sodobimo tudi vrednosti, ki jim dodamo še abstrakcijo:
vrednost v ::= · · ·
∣∣ λx. t.
E-App1
t1  t
′
1
t1 t2  t
′
1 t2
E-App2
t2  t
′
2
v t2  v t
′
2
E-AppAbs
(λx. t)(v) [x 7→ v]t
Tabela 5. Pravila za izvajanje lambda računa.
Kot pri preǰsnjem jeziku bi tudi tu radi s pomočjo tipov prǐsli do izreka
o varnosti. Da to storimo, moramo tipe funkcij najprej definirati. Tako
kot v matematiki funkcijo karakteriziramo z domeno (tipom argumenta) in
kodomeno (tipom rezultata).
Poglejmo abstrakcijo iz izraza (2): λx. (iszero x), ki bi, če bi jo po
uporabi na izrazu 0 izvedli do konca, vrnila rezultat true. Vidimo, da ima
rezultat izvajanja tip Bool. Ustaljenim tipom dodamo še tip funkcije, ki
vsebuje tip argumenta in tip rezultata:
tip T ::= · · ·
∣∣ T1 → T2.
Za splošno funkcijo λx. t torej ob predpostavki x : T1 velja t : T2.
Drugače od prej pa za tip izraza ni več odgovorna samo oblika izraza, ampak
tudi tipi spremenljivk (natančneje predpostavke o teh tipih), ki v njem
nastopajo. Zato definiramo kontekst, ki ima informacije o predpostavkah
glede tipov prostih (nevezanih) spremenljivk v izrazu t. Formalno relacijo
imeti tip razširimo na tri elemente: kontekst, izraz in tip: (Γ, t, T ) in pǐsemo
Γ ` t : T .
Z dodatnimi pravili za tipe, ki jih vidimo v tabeli 6, lambda račun po-
stane tipiziran, potreben je le kratek komentar. Tip spremenljivke (T-Var)
je po novih pravilih kar tip, ki smo ga za to spremenljivko predpostavili v
kontekstu Γ. Pri tipu funkcije (T-Abs) razširimo kontekst. Pravilo beremo
81–90 89
i
i
“Koprivec” — 2017/9/21 — 9:24 — page 90 — #10 i
i
i
i
i
i
Filip Koprivec
T-Var
x : T ∈ Γ
Γ ` x : T
T-Abs
Γ, x : T1 ` t2 : T2
Γ ` λx. t2 : T1 → T2
T-App
Γ ` t1 : T1 → T2 Γ ` t2 : T1
Γ ` t1 t2 : T2
Tabela 6. Pravila za tipe lambda računa z enostavnimi tipi.
takole: Če v kontekstu Γ, razširjenem s predpostavko x : T1, velja t2 : T2,
potem lahko sklenemo, da ima funkcija λx. t2 v kontekstu Γ tip T1 → T2.
Pravilo T-App pa podaja tip vrednosti uporabe funkcije ob predpostavki,
da ima glede na kontekst funkcija t1 tip T1 → T2 in izraz t2 tip T1.
Primer 11. S pomočjo izraza iz primera 1 sestavimo funkcijo, ki preveri,
ali je argument funkcije enak izrazu za 0 ali 1:
λx. if (iszero x) then true else (iszero (pred x)).
Poglejmo še izpeljavo tipa:
T-Abs
T-If
T-IsZero
T-Var
x : Int ∈ x : Int
x : Int ` x : Int
x : Int ` iszero x : Bool
...
x : Int ∈ x : Int
x : Int ` x : Int
T-Var
x : Int ` pred x : Int
T-Pred
x : Int ` iszero (pred x) : Bool
T-IsZero
x : Int ` if (iszero x) then true else (iszero (pred x)) : Bool
∅ ` λx. if (iszero x) then true else (iszero (pred x)) : Int → Bool .
Izrek o varnosti lahko posplošimo tudi na lambda račun z enostavnimi
tipi. Izrek enako kot prej zagotovi, da se izraz, ki ima tip, med izvajanjem ne
bo zataknil. Dokažemo ga s strukturno indukcijo, le da je treba obravnavati
več primerov zaradi dodanih pravil za izpeljavo tipov. Tipi nam tudi v
lambda računu zagotavljajo varnost. Pomembno dejstvo je, da nam izrek
o varnosti jamči zgolj to, da je izraz, ki ima tip, že končal z izvajanjem,
ali pa lahko naredi še (vsaj) en korak, nikakor pa nam ne zagotavlja, da se
bo izvajanje končalo. V lambda računu z enostavnimi tipi sicer vsi izrazi
s tipom končajo z izvajanjem, medtem ko to za druge programske jezike v
splošnem ne velja.
LITERATURA
[1] B. C. Pierce, Types and Programming Languages, The MIT Press, Cambridge Mas-
sachusetts, 2002.
[2] P. Wadler, Propositions as Types, dostopno na homepages.inf.ed.ac.uk/wadler/
papers/propositions-as-types/propositions-as-types.pdf, ogled 5. 11. 2016.
90 Obzornik mat. fiz. 64 (2017) 3