Funktsionaalprogrammeerimine 2024/25 sügis

Uute tüüpide loomine

Uusi tüüpe saab Idrises luua kahel viisil:

• "Type" ehk avaldis, mille tüüp on Type, ja
• "data" ehk uue algebralise andmetüübi loomine.

Type

Saame defineerida tüübisünonüüme:

Pikkus : Type
Pikkus = Int

Saame defineerida keerukamaid funktsioone, mis tagastavad tüübi:

Res : Type -> Bool -> Type
Res t False = t
Res t True  = List t

Keerukamatest juhtudest on pikemalt juttu sõltuvate tüüpide peatükis.

data

Andmetüüpide loomine on detailiderohke ja algajale segadust tekitav. Seetõttu, vaatame näiteid.

Näide: tõeväärtused

Tõeväärtuste tüüp Bool on defineeritud järgnevalt:

data Bool = True | False

Sellest koodireast loeme välja järgnevat:

• defineeritakse uus andmetüüp Bool : Type
• defineeritakse konstruktor True : Bool
• defineeritakse konstruktor False : Bool.

Siis saab kasutada mustrisobitust:

f : Bool -> ...
f True  =  ...
f False =  ...

Näide: Naturaalarvud Nat

Naturaalarvud on (standardteegis) defineeritud järgmiselt:

data Nat = Z | S Nat

Ehk siis:

• Nat on naturaalarvude tüüp;
• Z ehk null on naturaalarv;
• kui n on naturaalarv, siis ühe võrra suurem arv S n on naturaalarv.

Näide:

add : Nat -> Nat -> Nat
add Z     y = y
add (S x) y = S (x+y)

Näide: Listid

Listid on (standardteegis) defineeritud järgmiselt:

data List a = Nil | (::) a (List a)

Ehk siis:

• Iga tüübi a jaoks eksisteerib list List a;
• tühja listi konstruktor [] : List a;
• mittetühja listi konstruktor (::) : a -> List a -> List a.

Kasutamise näide:

len : List a -> Nat    -- prelüüdis  length
len Nil       = 0
len (_ :: xs) = 1 + len xs

Algebralised andmetüübid

Sõna "algebralised" tähendab siin seda, et tüüpe saab "liita" ja "korrutada". Tüüpide liitmine a+b tähenab, et väärtus võib olla tüübist a või tüübist b. Tüüpide korrutis a*b tähendab, et väärtuses sisaldub nii a tüüpi väärtus ja b tüüpi väärtus.

Tüüpide korrutamist teostab, näiteks, paari tüüp (a,b).

Tüüpide liitmist teostab, näiteks, tüüp Either a b.

data Either a b = Left a | Right b

Algebralised andmetüübid lubavad andmestruktuure modulaarselt üles ehitada.

data üldiselt

Lisaks eelnevalt näidatud süntaksile on Idrises olemas detailsem süntaks (suvalise {$n$}, {$m$}, ja {$k$} jaoks)

data T : t{$_1$} -> .. -> t{$_n$} -> Type where
{$\quad$} ...
{$\quad$} c{$_m$} : a{$_1$} -> .. -> a{$_k$} -> T v{$_1$} .. v{$_n$}
{$\quad$} ...

S.t. defineeritakse tüübikonstruktor T tüübiga t{$_1$} -> .. -> t{$_n$} -> Type, kus t{$_i$} on mingid tüübid. Lisaks, defineeritakse {$m$} andmekonstruktorit, kus igal konstruktoril on mingi arv parameetreid ja mis tagastab T v{$_1$} .. v{$_n$}, kus v{$_i$} on mingid väärtused v{$_i$} : t{$_i$}.

Pane tähele, et konstruktori parameetrite ja tüübikonstruktori parameetrite vahel võib nii tekkida väga keerulisi seoseid. Selliseid seoseid saab kasutada sõltuvate tüüpidega programmeerimise ja loogilise tõestamise jaoks.

Kirjed

Erisüntaks algebraliste andmetüübide jaoks, kus on palju nn. korrutatavaid tüüpe.

record Point where
    constructor MkPoint 
    x, y, z : Double

record Sphere where
    constructor MkSphere
    center: Point
    radius: Double 

Saab kasutada konstruktorit

pt1 : Point  -- "vana" süntaksiga
pt1 = MkPoint 10 20 12

... või anda argumendid nimeliselt

sp1 : Sphere  -- kirjete süntaks
sp1 = MkSphere { radius = 2, center = pt1 }

Kirje välju saab projitseerida.

  Main> sp1.center.x
  10.0

Selliseid projektsioone saab ka ise defineerida:

(.dist) : Point -> Double
(.dist) p = sqrt (p.x^2 + p.y^2)

  Main> pt1.dist
  22.360679774997898

Uut kirjet saab luua ka vana kirje põhjal:

resize : Sphere -> (dr: Double) -> Sphere
resize c dr = { radius := c.radius + dr } c

Väljale saab rakendada teisendusfunktsiooni.

resize_alt : Sphere -> (dr: Double)  -> Sphere
resize_alt c dr = { radius $= (+ dr) } c

Seda ka läbi mitme taseme:

move : (dx: Double)->(dy: Double)->(dz: Double)->Sphere->Sphere
move dx dy dz = { center.x $= (+ dx), 
                  center.y $= (+ dy), 
                  center.z $= (+ dz) }

Pane tähele, kuidas on kasutatud osalist rakendamist!