Ü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
- Funktsionaalse programmeerimiskeele tutvustus, λ-arvutuse tutvustus
- Keel Idris, baasväärtused ja -operatsioonid, listid
- Polümorfism, kõrgemat järku funktsioonid, fold-imine
- Uute andmestruktuuride defineerimine, tüübiklassid (ad hoc polümorfism)
- Monaadid, sisend-väljund
- Tüüpimata λ-arvutus, reduktsioon
- Lihtsalt tüübitud lambda arvutus
- 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öö!