Definitsioonid
Idrise programm sisaldab definitsioone; igal defineeritaval nimel on tüüp. Näiteks, loome faili test.idr:
a : Double a = 40.0 b : Double b = 30.0 c : Double c = sqrt (a*a + b*b)
Definitsioone saab lugeda interaktiivsesse keskkonda:
> idris2 test.idr
.. ja siis väärtustada
Main> c 50.0
Tüübid
Idrises on tüübid Bool, Int, Integer, Double, Char ja String.
Bool on tõeväärtuste tüüp, mille väärtused võivad olla kas True või False.
Int on 64-bit täisarvude tüüp ja Integer on piiramata pikkusega täisarvude tüüp.
Mõned tüübid on parametriseeritud teiste tüüpidega; näiteks List Bool, Maybe Bool, etc.
Üldiselt ...
on tüüpide tüüp Type ja List on funktsioon tüübiga Type -> Type, mistõttu saab sellele mingi tüübi argumendiks anda. Sarnaselt saab teha funktsioone, mis tagastavad või saavad parameetriks tüüpe.
Tüüpide kontrollimiseks saab kasutada funktsiooni the. Funktsioon the T x tagastab väärtuse x kui see on tüüpi T. Vastasel juhul tekib tüübiviga.
Main> the Int 5 5 Main> the Double 5 5.0 Main> the Int 5.5 Error: ...
Funktsioonid
Funktsioone defineeritakse võrdusmärgiga kasutades formaalsed parameetrid.
Näide:
pyth : Double -> Double -> Double pyth x y = sqrt (x*x + y*y)
Näitest saab välja lugeda:
- funktsiooni nimi:
pyth - funktsiooni tüüp:
Double -> Double -> Double - formaalsed parameetrid:
x,y - definitsiooni vasak pool:
pyth x y - definitsiooni parem pool:
sqrt (x*x + y*y)
Funktsiooni tüüp on “{$\alpha$} -> {$\beta$}”, kus {$\alpha$} on sisendi- ja {$\beta$} tulemuse tüüp.
Kahe argumendiga funktsioon on “a -> (b -> c)”, ehk “a -> b -> c”. S.t funktsioon võtab ühe argumendi ja tagastab funktsiooni, mis võtab teise argumendi ning tagastab mingi tulemuse. Funktsiooni tüübi nool on paremassotsiatiivne ehk paremalt võib sulud ära jätta.
Funktsiooni argumendid kirjutatakse funktsiooni järele:
Main> pyth 3 4 5.0
Funktsiooni rakendus on vasakassotsiatiivne:
pyth 2 3 == ((pyth 2) 3)
Funktsioone saab osaliselt rakendada ehk anda funktsiooni rakendades sellele vähem argumente. Defineerides ei pea kõiki argumente kirjutama.
pythKaks : Double -> Double pythKaks = pyth 2
Juhul, kui funktsioon tagastab funktsiooni, saab anda ka rohkem argumente, kui on formaalseid parameetreid.
Main> pythKaks 3 3.605551275463989
If-then-else
Tingimusavaldis if b then t else e väärtustub samaks väärtuseks mis t kui b väärtustub tõeseks. Vastasel juhul on tingimusavaldise väärtus sama mis e-l.
abs : Int -> Int abs n = if n<0 then -n else n
Näidiste ehk mustri-sobitamise kasutamine
Lisaks tingimuslausele saab hargneda ka vastavalt väärtuse struktuuri mustrile. Selleks on kolm võimalust: funktsiooni definitsiooni juures, with-konstruktsiooniga ja case-of konstruktsiooniga
Mustrisobitus funktsiooni defineerimisel:
f1 : Bool -> Int f1 True = 1 f1 False = 2
Mustrisobitus with-konstruktsiooniga (sulud on kohustuslikud):
f2 : Bool -> Bool -> Int
f2 a b with (a&&b)
_ | True = 2
_ | False = 3
Mustrisobitus case-of konstruktsiooniga:
f3 : Bool -> Bool -> Int
f3 a b =
case a||b of
True => 4
False => 5
Lokaalsed funktsioonid: let ja where
Kui funktsioonid muutuvad väga mahukateks, on need mõistlik tükeldada väiksemateks definitsioonideks. Idrises on lokaalsete muutujate ja funktsioonide defineerimiseks kaks konstruktsiooni: let ja where.
Let süntaks on: let x = 50 in x + x, kus x = 50 on lokaalse muutuja definitsioon ning x + x on lokaalse muutuja definitsiooni skoop ehk pärast võtmesõna in on x väärtus 50. Avaldise REPL-isse laadides saame:
Idris> let x = 50 in x + x 100 : Integer
Let konstruktsiooniga defineeritakse lokaalne muutuja või funktsioon enne selle kasutamist. Näiteks:
pyth : Double -> Double -> Double
pyth x y =
let square : Double -> Double
square x = x * x
in sqrt (square x + square y)
Where konstruktsiooniga defineeritakse lokaalne muutuja või funktsioon pärast selle kasutamist. Näiteks:
pyth : Double -> Double -> Double
pyth x y = sqrt (square x + square y)
where
square : Double -> Double
square x = x * x
Let ja where järel defineeritud funktsiooni tüüp ja definitsioon on tühemikutundlik. See tähendab, et variandid:
...
where square : Double -> Double
square x = x * x
...
where
square : Double -> Double
square x = x * x
...
let square : Double -> Double
square x = x * x
in
...
let
square : Double -> Double
square x = x * x
in
...
kompileeruvad, aga variandid, kus funktsiooni tüübideklaratsioon ja definitsioon ei ole kohakuti, näiteks:
...
where square : Double -> Double
square x = x * x
...
where
square : Double -> Double
square x = x * x
...
let square : Double -> Double
square x = x * x
in
...
jne. ei kompileeru.
Anonüümsed funktsioonid ehk lambdad
Anonüümset funktsiooni saab luua süntaksiga \ x, y, z => e, kus x, y ja z on formaalsed parameetrid ja e on avaldis. Langjoon \ tähistab {$\lambda$} sümbolit.
Anonüümseid funktsioone kasutatakse tihti, kui mingit lihtsat funktsiooni on vaja anda mõnele teisele funktsioonile argumendiks. Näiteks:
Main> map (\ x => x+10) [1,2,4] [11, 12, 14]
Infix operaatorid
Infix operaatorid on definitsioonid mis koosnevad ainult järgnevatest sümbolitest: :+-*\/=.?|&><!@$%~^#. Sellisel juhul saab neid kasutada infixselt ehk argumnentide vahel.
Näiteks: 5+2, 2*pi*r*r, Float -> Int
Infix operaatori kasutamiseks prefix-vormis tuleb see panna sulgudesse.
Näiteks: 3 + 4 == (+) 3 4
Infix operaatoril on prioriteet (i.k. precedence)
Näiteks: 3*4+5 == (3*4)+5, kuna * on tasemel 9 ja + tasemel 8.
Infix operaator võib olla parem- või vasakassotsiatiivne:
näiteks, a && b && c == a&&(b&&c) ja 2-3-4 == (2-3)-4
Neid seatakse nn. fixity deklaratsioonidega:
infixl 8 +, - infixl 9 *, / infixr 5 &&
S.t. liitmine ja lahutamine on prioriteediga 8, korrutamine ja jagamine prioriteediga 9. Aritmeetikatehted on vasakassotsiatiivsed. Konjunktsioon on prioriteediga 5 ja on paremassotsiatiivne.
Fixity deklaratsioone saab vaadata näiteks käsuga “:doc (+)”
Prefix operaatoreid saab rakendada infix-selt tagurpidi-ülakomade (`) vahel.
Näiteks: 5 `div` 2
Ennikud ja Unit tüüp
Väärtustest saab luua paare ja muid ennikuid.
Näiteks (1,'a'), ((1.1,8,'x'), False)
Enniku tüüp konstrueeritakse komponentide tüüpidest:
(1, 'a', False) : (Int,Char,Bool)
Info saab kätte mustrisobitusega:
f : (Int, Char, String ) -> Int f (x,c,ys) = x + 1
Kõige triviaalsem väärtus Idrises on ().
- Selle tüüp on samuti
()ehk() : () - Kasutatakse juhtudel, kui pole vaja informatsiooni edastada.
- Paljudes keeltes kasutatakse selle asemel tüüpi "void"
Järjendid e. listid
Järjendi tüübiks on List a, kus a on elementide tüüp.
Näiteks: List Int, List Char, List (List Float)
Järjendeid saab kirjutada näiteks nii:
[1, 2, 3], [3], [][True, False, False], [False], []- Idrise listid on arvuti mälus esindatud puudena:
[1, 2, 3] = ::
/ \
1 ::
/ \
2 ::
/ \
3 []
Pane tähele, et listi elemendid on alati vahetipu vasakud lapsed. Vahetippude paremad lapsed on alati listid.
Järjendi loomiseks on kaks konstruktorit, mis vastavad (list-tüüpi) puu tippudele.
[] : List a(::) : a -> List a -> List a
Näide: [3,2,1] == 3 :: (2 :: (1 :: []))