Üldiselt
Funktsionaalprogrammeerimine (ehk FP) on välja kasvanud λ-arvutuse teooriast ja on oma heade omaduste tõttu leidnud tee paljudesse levinud programmeerimiskeeltesse. Kuigi funktsionaalses stiilis saab programmeerida nii Pythonis, Javas, C++-is, C#-is kui ka JavaScriptis, eelistame õppimiseks puhast funktsionaalset keelt Idris. Lisaks FP alustele õpime tüübipõhist programmeerimist, mis väidab, et tüüpe arvestades on lihtsam kirjutada korrektseid ja tõhusaid programme. Kursuse lõpus vaatame põgusalt paari tänapäevasemat FP teemat: sõltuvate tüüpide teooriat ja kvantitatiivset tüübiteooriat. Sõltuvad tüübid Idrises võimaldavad näiteks funktsioonide korrektust tõestada. Kvantitatiivses tüübiteoorias saame lisaks väljendada, mitu korda mingit väärtust kasutatakse -- võimaldades täpselt spetsifitseerida piiratud ressurssidega arvutusi, näiteks mitmelõimelist arvutamist.
Teemad nädalate kaupa (TODO)
- Sissejuhatus, funktsionaalse programmeerimiskeele tutvustus, paradigmad.
- λ-arvutuse tutvustus, baasväärtused ja -tüübid, rekursiivsed funktsioonid täisarvudel.
- Substitutsioon, kõrgemat järku funktsioonid, listid.
- Uute tüüpide loomine, andmestruktuurid, kirjed.
- Reduktsioon, λ-termid Idrises.
- Liidesed, do-notatsioon, sisend-väljund.
- Andmed λ-arvutuses.
- Vahekontrolltöö!
- Churchi tees
- Laisk väärtustamine ja lõpmatud struktuurid
- Tüübituletus
- Kombinaatorloogika
- Lineaarsete tüüpidega sisend-väljund
- Vektorid ja muud sõltuvad tüübid
- Tõestused tüübiteooria abil
- Kontrolltöö!
Hindamine
Hinde skaala: 0p .. 50p → F, 51p .. 60p → E, 61p .. 70p → D, ...
Hinde moodustavad:
- Kontrolltööd (2*32p, 2*10p alampiir, praksi ja/või sessi ajal)
- Kodutööd (12*3p, Moodle)
- Lisaks projektiülesanne + esitlus (6 boonuspunkti)
- Active Quiz ja Tagasiside (iga küsitlus 0.5 boonuspunkti, Moodle)
Kontrolltööd
Kontrolltöid on 2:
- Vahekontrolltöö 9. nädalal (8. praktikumis)
- Kontrolltöö 16. nädalal (15. praktikumis)
Mõlemat kontrolltööd saab lahendada kuni 2 korda, esimene kord semestri ajal praktikumis ning teine kord eksamisessiooni ajal. Kahest katsest läheb arvesse parim.
Kontrolltööd on avatud materjalidega: lubatud on enda lahenduste, näidislahenduste ja interneti kasutamine. Kontrolltöö ajal on suhtlemine keelatud.
Kontrolltööd toimuvad üldjuhul Deltas kohapeal. Kontrolltööst haigestumise vms. mõjuval põhjusel puudumise korral võtta ühendust praktikumijuhendajaga.