Eelmine Üles Järgmine

Peatükk 4  Formaalne Programmeerimine

4.1  Haskelli süntaks

Haskellist metoodiliselt aru saamiseks on mõistlik tutvuda keele süntaksiga. Järgnevad reeglid pole küll täielikud, aga katavad suure osa laialt kasutatavatest konstruktsioonidest.

Süntaksi kirjeldamiseks kasutame EBNF notatsiooni, milles moodustavad

Kommentaarid algavad semikooliniga. Väiketähega algav nimi on name, suurtähega algav nimi on Name ning nende ühisosa on name. Sümboliga algav nimi on ⊕ ja kooloniga algav nimi :name.

Avaldiste süntaks

     
Exp ::=  Const     ; konstant, nt. 5.4, ’x’, ”hello”        
|    name     ; konstruktor, muutuja, nt. f, Just        
|    Exp  Exp     ; funktsiooni rakendus, nt. f 5.4        
|    "−"  Exp     ; negatsioon, nt.  -x        
|    Exp  ⊕  Exp     ; op. infikne rakendus, nt. x*5.4        
|    "("⊕")"     ; op. prefiksne rakendus, nt. (*)        
|    Exp  "‵"   name   "‵"  Exp     ; nime infiksne kasutamine, nt. 5`f`2        
|    "if" Exp "then" Exp "else" Exp     ; tingimuslause        
|    "λ"  Pat+   "→"   Exp     ; anonüümne funktsioon        
|    "case"  Exp  "of"  (Pat  Gcases)+     ; mustrisobitus        
|    "("  Exp ","  … ","   Exp  ")"     ; ennikud, nt. (1,False,x)        
|    Exp  "::"  Type     ; tüübipiirang, nt. 5.4 :: Double       
|    …          
     
Gcases ::= "→"  Exp       ; ilma valvurita mustrisobitus         
|    ("|"   Exp    "→"    Exp)+       ; valvuritega mustrisobitus         
     
Pat ::= Const     ; konstant, nt. 5.4, ’x’, ”hello”        
|    name     ; muutuja, nt. a        
|    "_"     ; alakriips       
  |    Name Pat*     ; kontruktori rakendus, nt. Just a        
|    "("  Pat ","  … ","   Pat  ")"     ; ennikud, nt. (1,_,x)        
|    Pat  :name  Pat     ; infiksne k. rakendus, nt. 1:xs         

See grammatika on aga selgelt mitmene. Seega tuleb Haskelli avaldisi alati parsida vastavalt defineeritud operaatorite prioriteetidele (i.k precedence) ja assotsiatiivsusele. Alles jäänud mitmesused tuleb programmeerija poolt lahendada — kasutades selleks sulge!

Näide: Võime nii teha avaldise:
\ x (b,_) -> if b then f (4 + x :: Double) else Nothing

Listi süntaksid

Listide mugavamaks kasutamiseks mõeldud enumeratsioonisüntaks ja listikomprehensioon.

     
Exp ::= …          
|    "[" Exp [","  Exp] .. [Exp] "]"     ; enumeratsioon, nt. [1,3..x]        
|    "[" Exp "|"  Lcomp ("," Lcomp)* "]"     ; nt. [ a+b | a <- x, b <- [0..a]]        
|    …          
Lcomp ::=Pat ←  Exp     ; generaator, nt. x <- [1..]        
|    Exp     ; tingimuslause; nt. even x        
|    "let"   Pat   "="   Exp     ; nt. let n = f x         

Do süntaks

Monaadilise funktsiooni kirjutamiseks saab kasutada do-süntaksit.

     
Exp ::= …          
|    "do"  Stmt*  Exp     ; nt. do {x <- readLn; return (x+1)}        
           
Stmt ::=Exp     ; protseduur, nt. putStrLn "tere"        
|    Pat   ←  Exp     ; tagastusväärtuse sidumine; nt. x <- readLn        
|    "let"   Decl+     ; nt. let n = f x         

Lihttüüpide süntaks

Lihttüübid on ilma tüübiklasside kitsenduseta tüübid. Funktsiooni argumentidel peavad olema lihttüübid, kuna tüübiklasside kitsendused seotakse terve funktsiooniga, mitte üksikute argumentidega.

     
Type ::= Name     ; baastüüp, nt. Int, Char        
|    name     ; tüübimuutuja, nt. a, b        
|    Type  "→"  Type     ; funktsioon, nt. a -> Int        
|    "[" Type "]"     ; listitüüp, nt. [Int]        
|    "("  Type ","  … ","   Type  ")"     ; ennik, nt. (Int, Char, a)        
|    Name  Type  …  Type     ; tüübipere tüübid, nt. Either Int Char        
|    "forall"   name*   "."  Type     ; universaalne kvalifitseerimine        

Kõik tüübimuutujad tekivad universaalse kvalifitseerimine tagajärjel. Kõige välimise forall-konstruktsiooni ei pea eksplitsiivselt kirjutama ehk tüüp a -> a on tegelikult forall a. a -> a.

Pane Tähele! Automaatne tüübituletus võib jääda hätta kõrgemat järku tüüpide tuletamisel — ehk siis kui forall-e on mitu eristatavat taset. Seetõttu soovitame algajatel eksplitsiivset universaalset kvalifitseerimist mitte kasutada.

Deklaratsioonide süntaks

Mitteterminaliga Ftype, mis on Type täiendus, saame defineerida lihtsate deklaratsioonide süntaksi.

     
Decl’ ::= name ","   … ","   name  "::"   Ftype          
   ; nt. a, b :: Int -> Char          
|    name  Pat*   "="   Exp  ["where"  Decl’*]         
   ; nt. f (Just x) _ = x+1          
|    name  Pat*   Gexp+ ["where"  Decl’*]         
   ; nt. f x |  x < 10 = x+1 | otherwise = 10          
           
Gexp ::= "|"   Exp   "="   Exp         
   ; valvuriga avaldis nt. | x < 10 = x+1           

Avaldise sees saab kasutada (abi)-deklaratsioone

     
Exp ::= …          
|    let  Decl’+  in  e          

Tüübiklasside süntaks

Funktsioonide tüübid võivad sisaldada tüübiklassi kitsendusi — neid nimetatakse sel juhul kontekstiks.

     
Ftype ::= Type     ; tüübid, nt. a -> a -> Bool        
|    Context   "=>"   Type     ; nt. (Show a, Eq a) => a -> Int        
           
Context ::= Name name       ; nt. Eq a või Show b         
|    "("  Name name ","  … ","   Name name  ")"       ; nt. (Show a, Eq a)         

Siin on esitatud süntaks üheargumendiliste tüübiklasside jaoks. Mitme parameetriliga tüübiklasside tegemisekt tuleb GHC-s lülitada sisse vastav laiendus: MultiParamTypeClasses.

Nüüd saame deklareerida tüübiklasse (mis pole lubatud let-sees):

     
  Decl ::= Decl’  |   "class"   [Context   "=>"]  Name name  "where"  Decl’*           
Näide:
class Eq a where class Eq a => Ord a where comp :: a -> a -> Int

Ning ka tüübiklasside instantse:

     
  Decl ::= …  |   "instance"   [Context    "=>"]  Name Type  "where"  Decl’*           
Näide:
instance Eq Bool where eq True True = True eq _ _ = False instance (Eq a, Eq b) => Eq (a,b) where eq (x1, y1) (x2, y2) = eq x1 x2 && eq y1 y2

Andmetüüpide deklareerimise süntaks

Uusi andmetüüpe saab deklareerida järgnevalt.

     
Decl ::=  …          
|    "data"  Name name*  "="   Name name* ("|"   Name name*)*  [deriving  Names]         
|    "newtype"  Name name*  "="   Name name*  [deriving  Names]         
|    "type"  Name name*  "="   Type         
           
     
    Names ::= Name       ; üksik nimi, nt. Show        
|    "("  Name ","  … ","   Name  ")"       ; nt. (Show, Eq, Ord)        
               
Näide:
data Either a b = Left a | Right b deriving (Show, Eq, Ord) newtype Pikkus = Meeter Double deriving Show type String = [Char]

Fixity deklareerimise süntaks

Infikssete operaatorite defineerimiseks on vaja deklareerida nende prioriteet ja assotsiatiivs. Seda saab teha fixity deklaratsiooniga.

     
Decl ::=  …          
|    "infix"["r"|"l"]  Num  ⊕        ; nt. infixl 6 +        
|    "infix"["r"|"l"]  Num  "‵" name "‵"       ; nt. infixl 7 `div`         

4.2  Süntaktiline suhkur

Deklaratsioonid

Listidega programmeerimise peatükis kasutasime mustrisobituseks funktsiooni deklaratsiooni. Teooria mõttes on aga parem, kui need võimalused jagada kaheks. Formaalsel lähenemisel käib funktsioonide defineerimine ainult λ-ga ja mustrisobitus case-of süntaksiga.

f p1,1 ... pn,1 = b1 ... f p1,m ... pn,m = bm
   —→  
f = \ x1 ... xn = case (x1, ..., xn) of p1,1 ... pn,1 -> b1 ... f p1,m ... pn,m -> bm

Hea teada: Praktikas optimeeritakse vastupidises suunas, kuna siis saab mitme argumendi rakendamist teha vähemate operatsioonidega.

Let-avaldised

Formaalses λ-arvutuses pole deklaratsioone ning seda lünka täidab let-avaldis. Haskelli implementatsioonis on aga mindud vastupidist teed — let-avaldised tõlgitakse deklaratsioonideks.

Listidega programmeerimise peatükis kasutasime mustrisobituseks funktsiooni deklaratsiooni. Teooria mõttes on aga parem, kui need võimalused jagada kaheks. Formaalsel lähenemisel käib funktsioonide defineerimine ainult λ-ga ja mustrisobitus case-of süntaksiga.

Järgnevalt toome välja tõlkereegli ühe definitsiooniga let-i puhul.

f = \ x1 ... xn -> let y = d in e
  —→  
y = \ x1 ... xn -> d f = \ x1 ... xn -> e[y -> y x1 ... xn]

Kus e[y -> y x1 ... xn] tähistab avaldist e kus let-iga seotud nimi y on asendatud funktsioonikutsega uuele definitsioonile y x1 ... xn.

Enumeratsioonisüntaks

Enumeratsioonisüntaks tõlgitakse Enum tüübiklassi funktsioonikutseteks.

[x..]—→enumFrom x
[x,y..]—→enumFromThen x y
[x..y]—→enumFromTo x y
[x,y..z]—→enumFromThenTo x y z

Listikomprehensioon

Listikomprehensioon kirjutatakse ümber listimonaadi do-avaldiseks. Generaatori, tingimuslause või let-id tõlgitakse do-avaldise lauseteks:

p <- e—→p <- e
e—→guard e
let p = e—→let p = e

Funktsioon guard :: Bool -> [()] on defineeritud järgnevalt:

guard False = [] guard True = [()]

do avaldise viimase lausena tagastatakse väljastava lause väärtus.

Näide:
[a+b| a <- x, b <- [0..a], elem b x]—→
do a <- x b <- [0..a] guard (elem b x) return (a+b)

do-süntaks

Monaadilises koodis kasutatav do-süntaks kirjutatakse ümber tüübiklassi Monad funktsiooni (>>=) :: Monad m => m a -> (a -> m b) -> m b ja lambda-avaldiste kaudu.

4.3  Hindley-Milner tüübisüsteem

Tüüpimise reeglid

Haskell lähtub tüüpimisel Curry stiilist, mis tähendab et avaldised ei sisalda eksplitsiitselt tüübiinformatsiooni. Seega korrektsuse kontrollimiseks tuleb esmalt tüübid tuletada. Esmalt vaatame aga ikka tüüpide kontrollimist, mis on tuletamisest lihtsam ülesanne.

Tüübikontroll käib läbi nn. tuletusreeglite, millel igaühel on järgnev muster:

eeldus 1           …           eeldus  n   (reegli-nimi)
järeldus 
Näide: Loogika kohta võime kirjutada järgnevad tuletusreeglid.
     
 A 
 A ∨ B
    
 B 
 A ∨ B
    
(A ∨ C) ∨ B
(A ∨ B) ∨ C
    
A           A  B
B
    

Reegleid, millel eeldused puuduvad nimetame triviaalseteks. Enamasti me triviaalseid reegleid välja ei too — aga kõik lihtsad aritmeetika ja hulgateooria väited on meil kasutatavad.

Näide: Triviaalsed reeglid.
     
 
1+1 = 2
    
 
1 ∈ ℕ
    
 
{1,2}⋂{4,5} = {}
    
 
A ∨ ¬ A
    

Tuletusreegleid saab kokku kombineerida tuletuspuuks (i.k derivation tree). Kui ühe reegli eeldus on teise reegli järelduseks siis saame eelduse kohta käiva reegli kirjutada järelduse reegli peale. Niimoodi võib tuletamise käigus eelduste hulk kasvada ja kahaneda. Kui tuletuspuul eeldused puuduvad, võime lugeda kogu puud järelduse tõestuseks.

Näide: Väidet A (A ∨ B) saame tõestada kasutades eelnevalt antud reegleid.
     
 
 
 
A ∨ ¬ A
 (A ∨ ¬ A) ∨ B
 (A ∨ B) ∨ ¬ A   
A  (A ∨ B)
          

Tüübikontroll on väide kontrollimine, kui väide on kujul Γ  ⊢  e :: t — ehk tüübikontekstis Γ on avaldise e tüüp t. Tüübikontekstis hoiame programmi definitsioonide ja muude skoobis olevate muutujate tüüpe. Ruumi kokkuhoiu mõttes jätame standardteegi funktsioonide tüübid konteksti kirjutamata.

Näide: { x:: Int, y :: Bool } ⊢  4 + x :: Int

Pane Tähele! Tüübikontroll on väite Γ  ⊢  e :: t jaoks (ilma eeldusteta ja korrektse) tuletuspuu leidmine.

Pane Tähele! Tüübituletus on avaldise e (ja konteksti Γ) jaoks tüübi t leidmine, mille puhul saame tuletusreeglitest kombineerida ilma eeldusteta tuletamise puu.

Järgnevalt vaatame läbi kõik tüüpimise reeglid. Iga avaldise grammatika reegli kohta on üks reegel. Lisaks on reeglid I ja G, mida vaatame hiljem. Niisiis käib sobiva reegli valimine avaldise struktuuri järgi. Näiteks, kui avaldis on konstant, tuleb kasutada järgnevat reeglid.

konstant c on tüüpi α K
Γ  ⊢  c :: α 
Näide:
     
 
{}  ⊢  5 :: Int
    
 
{}  ⊢  7.98 :: Double
        

Järgnev reegel käib muutujate kohta. Muutuja on just nimelt seda tüüpi, mis tüübiga ta on kontekstis kirjas.

x :: α  ∈  Γ  M
Γ  ⊢  x :: α 
Näide:
     
 x :: Int  ∈  { x:: Int, d:: Double }  
{ x:: Int, d:: Double } ⊢  x :: Int 
    
 d :: Double  ∈  { x:: Int, d:: Double } 
{ x:: Int, d:: Double } ⊢  d :: Double 
        

Haskelli süntaksis on erinevaid viise märkimaks sisuliselt funktsiooni rakendust aga kõik need jagunevad kahte klassi: prefiks rakendused ja infiks rakendused.

Γ  ⊢  f  ::   α → β           Γ  ⊢  x  ::   α R
Γ  ⊢  f x  ::   β 
  
Γ  ⊢  e1  ::   α           Γ  ⊢  (⊕)  ::   α → β → γ           Γ  ⊢  e2  ::   β Ri
Γ  ⊢  e1⊕ e2  ::   γ 
  
Näide:
     
 { f :: Int → String  }  ⊢  f  ::   Int → String           { f :: Int → String  }  ⊢  5  ::   Int 
{ f :: Int → String  }  ⊢  f 5 :: String 
             

Tingimuslasue puhul saab kasutada järgnevat reeglit.

Γ  ⊢  e1  ::   Bool           Γ  ⊢  e2  ::   α           Γ  ⊢  e3  ::   α If
Γ  ⊢  if e1 then e2 else e3  ::   α 
  
Näide:
     
 {}  ⊢  True  ::   Bool            {}  ⊢  maxBound  ::   Int            {}  ⊢  0  ::   Int 
 {}  ⊢  (if True  then  maxBound  else  0)  ::   Int 
          
 {}  ⊢  True  ::   Bool            {}  ⊢  id  ::   Bool → Bool            {}  ⊢  not  ::   Bool → Bool 
 {}  ⊢  (if True  then  id  else  not)  ::   Bool → Bool 
          

Anonüümse funktsiooni ehk λ korral kasutada järgnevat reeglit.

Γx ⋃ {x :: α}  ⊢  e :: β L
Γ  ⊢  (λ x→ e)  ::   α → β 

See reegel kasutab süntaksit Xȳ, mis eemaldab hulgast X muutujaga y seotud kirje.

Näide:
     
 {x :: Int, y :: Int }  ⊢  x+y  ::   Int 
{ x:: Bool, y :: Int }  ⊢  (λ x→ x+y)  ::   Int → Int
          

Paaride ja ennikute korral kasutada järgnevat reeglit.

Γ  ⊢  e1 :: α1           …           Γ  ⊢  en :: αn  P
Γ  ⊢  (e1, …, en) ::   (α1, …, αn) 
Näide:
     
 {}  ⊢  5 :: Int            {}  ⊢  not  False :: Bool             {}  ⊢  "hei" :: String  
{}  ⊢  (5, not  False, "hei") ::   (Int, Bool, String) 
          

Tüübikitsenduse avaldise puhul kasutada järgnevat reeglit, mis sunnib avaldise tüübiks (vähemalt) kitsendatud tüübi.

 Γ  ⊢  e :: α  T
 Γ  ⊢  (e :: α) :: α  
Näide:
     
 { myid :: a → a }  ⊢  myid :: Int → Int
 { myid :: a → a }  ⊢  (myid :: Int → Int) :: Int → Int   
          

Mustrisobituse on keerukam, kuna iga juhu korral tuleb konteksti vastavalt mustrile muuta. Kasutame abifunktsiooni f, mis teisendab konteksti vastavalt mustri ja tüübi järgi.

 Γ  ⊢  e :: β           f(pi, β, Γ)  ⊢  ei :: α  S
 Γ  ⊢  case  e  of  p1 → e1  …  pn → en :: α  

Abifunktsioon f valmistab ette harude kontekstid ja kontrollib mustrite vastavust tüübile.

     
  f(_,α, Γ)= Γ         
f([],[α], Γ)= Γ         
f(c,α, Γ)= Γ   kui c on α tüüpi konstant         
f(x,α, Γ)= Γ⋃{x:: α}         
f(p : ps, [α], Γ)= f(p,α, f(ps, [α], Γ))         
f((p1, …, pn), (α1, …, αn), Γ)= f(p1, α1, … f(pn,αn,Γ)…)         
f(c p1… pn, α, Γ)= f(p1, β1, … f(pn,βn, Γ)…)         
     kus  (c:: β1 → …→βn→α) ∈ Γ         
f(_,_,_)= tüübiviga          
Näide:
     
 {}  ⊢  [1,2] ::   [Int ]           {}  ⊢  0 :: Int           { x :: Int, xs ::   [Int ] }  ⊢  x + sum  xs :: Int 
 {}  ⊢  (case  [1,2]  of  [] → 0   x : xs → x + sum  xs)  ::   Int  
          

Haskelli tüüpides võime kasutada (tüübi-) muutujaid: näiteks teame, et identusfunktsiooni tüüp on id:: a → a. Eksplitsiitselt kirjutades on aga tüüp hoopis id:: ∀ a. a → a — iga tüübi a puhul saame funktsiooni a→ a. See tähendab, et saame a kitsendada tüübiks Bool ja saame Bool →Bool . Sellise kitsenduse ehk tüübiinstantsi jaoks ongi järgmine reegel.

 Γ  ⊢  e :: ∀ α. β           α. β ⊒ γ  I
 Γ  ⊢  e :: γ  

Tingimus ∀ α. β ⊑ γ tähendab, et saame muutujate vektori α asemele kirjutada konkreetsed tüübid, et tulemus oleks γ.

Näide:
     
  ∀ a.  a⊒ Int → Bool        undefined       
∀ a. a → a⊒ Int → Int        id        
∀ a. a → a⊒ Bool → Bool        id       
∀ a  b. a → b → a⊒ ∀ b. Int → b → Int        const       
∀ a  b. a → b → a⊒ Int → Bool → Int        const        

Nii saame tüüpida polümorfseid funktsioone.

Näide:
     
  {}  ⊢  id  ::  ∀ a.   a →  a  I
 {}  ⊢  id  ::   Bool → Bool   
     ehk tavakirjas    
  {}  ⊢  id  ::   a → a  I
 {}  ⊢  id  ::   Bool → Bool   
      

Nüüd aga võime küsida: kust tekivad tüübid kujul ∀α.  α → α. Need tekivad üldistava ehk generaliseeriva reegli kaudu.

 Γ  ⊢  e :: β           α pole vaba tüübi-muutujad Γ-s  G
 Γ  ⊢  e :: ∀ α. β  

Tüübimuutuja nimetame vabaks, kui ta pole seotud ∀-iga. Seega ei saa me üldistamist rakendada tüübimuutujatele, mis esinevad (vabalt) kontekstis.

Näide: Järgnev tuletuspuu tõestab, et id on tüüpi ∀ a.  a → a.
     
 
 
 x ::  a ∈ {x :: a }
 
 M
{x :: a }  ⊢  x  ::    a 
 
 L
{}  ⊢  (λ x→ x)  ::   a → a 
 G
{}  ⊢  (λ x→ x)  ::  ∀ a.  a → a 
          

Pane Tähele! let-avaldised, do-avaldiste ja listikomprehensiooni erisüntaksid tõlgitakse tavalisteks deklaratsioonideks ja funktsioonirakendusteks. Nende jaoks pole reegleid vaja.

Tüübituletus

Tüübituletuseks püüame leida tuletuspuud avaldise e (ja konteksti Γ) jaoks. Leitavaks tüübiks võtame esialgu meta-muutuja (näiteks α) ja teeme puu (alt-üles) vastavalt avaldise süntaksile. Seejärel valime näiteks kõige üldisema tüübi, mis sobib α asemele. Sarnaselt kasutame meta-muutujaid iga kord kui me ei tea mis tüüpi kasutada.

Näide:
     
 
  (1)
{}  ⊢  (||) :: β→γ→α  
          
  (2)
{}  ⊢  False :: β  
          
 
 
 
 {}  ⊢  id :: ∀ a.  a → a 
 (3)
 {}  ⊢  id :: δ→γ  
          
  (4)
 {}  ⊢  True :: δ  
{}  ⊢  id  True :: γ 
{}  ⊢  (False  ||  id  True) :: α 
          
Sellest puust vahetippudest saame järgnevad kitsendused:
(1)
α = β = γ = Bool
(2)
β = Bool
(3)
δ = γ
(4)
δ = Bool

Tüüpimise tuletuspuu on järgnev

     
 
  M
{}  ⊢  (||) :: Bool →Bool →Bool  
          
  K
{}  ⊢  False :: Bool  
          
 
 
  M
 {}  ⊢  id :: ∀ a.  a → a  
 I
 {}  ⊢  id :: Bool →Bool  
          
  K
 {}  ⊢  True :: Bool  
 R
{}  ⊢  id  True :: Bool  
 Ri
{}  ⊢  (False  ||  id  True) :: Bool  
          

Kui peale kitsenduste lahendamist jääb mõni meta-muutuja ilma kitsendusteta, kasutame reeglit G nende muutujate sidumiseks üldsuskvantori alla. Seda teeme aga ainult deklaratsioonide tüüpimisel esimese sammuna.

Näide: Tüübime deklaratsiooni id = \ x -> x
     
 
 
  (1)
 {x:: δ }  ⊢  x :: σ  
 (2)
 {}  ⊢  (λ x→ x) :: γ  
          
Sellest puust vahetippudest saame järgnevad kitsendused:
(1)
δ = σ
(2)
γ = δ → σ

Kuna kitsenduste lahendamisel on tulemuseks δ→δ, kus δ pole kitsendatud, saame selle muutuja üldistada uueks tüübimuutujaks. Tulemus on järgnev

     
 
 
  M
 {x:: a }  ⊢  x :: a  
 L
 {}  ⊢  (λ x→ x) :: a  
 G
{}  ⊢  (λ x→ x) :: ∀ a.  a → a  
          

Tüübiklassid

Tüübiklasside kontrollimiseks on lisaks tüüpimise väidetele vaja kasutada ka tüübiklassi väiteid. Need on kujul Γ  ⊢  C α, kus Γ on eelnevalt kirjeldatud kontekst, C on tüübiklassi nimi ja α on tüüp. Näiteks Γ ⊢  Show Int või Γ ⊢  Eq Bool . Kõige lihtsamal juhul on tüübiklassi instants defineeritud programmi sees s.t. kontekstis leidub vastav instants.

 C α ∈ Γ   Mc
 Γ  ⊢  C α  
Näide:
     
 Show  Int ∈ {Show  Int, Show  a, x :: a  } 
 {Show  Int, Show  a, x :: a }  ⊢   Show  Int  
          
     
 Show  a ∈ {Show  Int, Show  a, x :: a  } 
 {Show  Int, Show  a, x :: a }  ⊢   Show  a  
          

Mitmetel juhtudel pole aga instantsid otse (standardteegi) koodis antud vaid on antud teisendamise reeglid üldiselt. Näiteks paaride võrdlus (Eq) on antud hoopis järgnevalt.

Näide: Paari võrdlemise instants.
instance (Eq a, Eq b) => Eq (a,b) where (x1,y1) == (x2,y2) = x1==x2 && y1 == y2

Sellisel puhul on kontekstis (Eq a, Eq b) ⇒ Eq (a,b)  ∈  Γ ja me saame kasutada järgnevat reeglit.

 (C1 α1,…, Cn αn) ⇒ C α∈ Γ          Γ  ⊢  C1 α1           …          Γ  ⊢  Cn αn  Dc
 Γ  ⊢  C α  
Näide:
     
  (Eq  a, Eq  b) ⇒ Eq  (a,b)  ∈ Γ          Γ  ⊢   Eq   Int           Γ  ⊢   Eq   Int
 Γ  ⊢   Eq  (Int, Int) 
          
kus Γ = {Eq Int, (Eq a, Eq b) ⇒ Eq (a,b) }

Nüüd on tüübiklasside toetamiseks vaja ainult instantsi reegli laiendamist tüübiklassidele. Tüübi kitsendusel võime kasutada tüübiklasse — aga ainult siis kui leiduvad vastavad instanstsid.

 Γ  ⊢  e ::   (C1 α1,…, Cn αn) ⇒ α           Γ  ⊢  C1 α1           …          Γ  ⊢  Cn αn  Dc
 Γ  ⊢  e :: α  
Näide:
     
 
 
 
 
show :: ∀ a. Show a ⇒ a → String  ∈  Γ 
 M
 Γ  ⊢   show :: ∀ a. Show a ⇒ a → String  
 I
Γ  ⊢   show :: Show Int ⇒ Int → String  
          
 
 
Show Int  ∈ Γ
 
 Ic
Γ  ⊢  Show Int  
 Gc
 Γ  ⊢   show :: Int → String   
          
kus on defineeritud kui Γ={Show Int, show:: ∀ a. Show a. a → String }

4.4  Graafireduktsioon ja laisk väärtustamine

Laisk väärtustus toob mõnel juhul kaasa arvutussammude arvu suurenemist. Vaatame järgmist koodi.

topelt x = x + x

Siis laisk funktsiooni rakendus vajab nelja sammu:

     
  topelt (1+1)⇝  (1+1) + (1+1)         
 ⇝  2 + (1+1)         
 ⇝  2 + 2         
 ⇝  4          

Kuid agar vajab ainult kolme sammu:

     
  topelt (1+1)
⇝
agar
 
topelt 2
         
 
⇝
agar
 
2 + 2
         
 
⇝
agar
 
4
         

Seetõttu on Haskellis kasutataksel hoopis graafireduktsiooni, mille puhul väärtustatavaks justkui where-avaldisi. Implementatsioonis aga kasutatakse muutujanimede asemel viitasid — seetõttu võime mõelda, et where-asendamine avaldise sisse toimub nii hilja kui võimalik ning seda ei loeta eraldi sammuks.

Näide:
     
  x * x where x = 1 + 1⇝  x * x where x = 2         
 ⇝  4          
     
  5 where x = 1 + 1 ⇝   5          

Loetavuse lihtsustamiseks kirjutame normaalkujul väärtuse avaldisse otse sisse. Samuti ei kasuta me where-i, kui defineeritud nime kasutakse vähem kui kahes kohas.

Näide:
     
  x where x = 1 + 1 ≡  1 + 1!          
     
  5 where x = 1 + 1 ≡  5          

Vajadusesel tuleb luua uusi muutujanimesid, et andmeid mitte kopeerida.

Näide:
  case 1:2:3:4:[] of {[] -> []; x:xs -> xs ++ xs}
     ⇝   xs++xs where xs = 2:3:4:[]

Graafireduktsiooni täpsed reeglid on kirjapandult kahjuks väga kohmakad. Väikeste näidete jaoks on ülaltoodud juhised piisavad. Kompilaatorites kasutatakse aga hoopis ilma reduktsioonideta väärtustamist, mistõttu me graafiredutkstiooni detailidesse ei lange.

Reduktsioonivaba väärtustamine

Eelnevalt kirjeldatud lihtsat väärtustusmudel on reduktsioonidel põhinev. Väärtustamine (i.k. evaluation) kitsamas mõttes on aga ilma reduktsioonideta. Reduktsiooni puhul tuleb avaldisest üles leida reedeks, see lihtsustada ja uuesti avaldisse paigutada. Kuna lihtsustusreeglid on lihtsamini mõistetavad, ei teki küsimusi protsessi korrektsuse osas. Kahjuks aga, on reduktsioon praktiliselt väga aeganõudev. Parem viis on (reduktsioonideta) väärtustamine.

Eelmine Üles Järgmine