Arvutiteaduse instituut
  1. Kursused
  2. 2024/25 sügis
  3. Funktsionaalprogrammeerimine (LTAT.03.019)
EN
Logi sisse

Funktsionaalprogrammeerimine 2024/25 sügis

  • Üldinfo
    • Õppekorraldus
  • Kursus
    • KKK
    • Installimine
    • Kodutöö 1
    • Kodutöö 2
    • Kodutöö 3
    • Kodutöö 4
    • Kodutöö 5
    • Kodutöö 6
    • Kodutöö 7
    • Kodutöö 8
    • Kodutöö 9
    • Kodutöö 10
    • Kodutöö 11
    • Kodutöö 12
    • Kodutöö 13
    • Kodutöö 14
  • Konspekt
    • Baasväärtused ja tüübid
    • 𝜆-arvutus
    • Kõrgemat järku funktsioonid
    • Interaktiivne programmeerimine
    • Uute tüüpide loomine
    • Liidesed
    • Sisend-Väljund
    • Laiskus
    • Lihtsalt tüübitud 𝜆-arvutus
    • Tüübituletus
    • Sõltuvad tüübid
    • Tõestamine Idrises
    • Kvantitatiivne tüübiteooria
  • Moodle
  • Zulip (sisselogides näed linki)

Praktikum 0 - Tarkvara paigaldus

Toome välja mõned näited, kuidas Idris2 installida. Võite kasutada teisi meetodeid -- peamine, et teil oleks töötav Idris2 REPL (i.k. read-eval-print loop) ja mingi koodiredaktor. Alles viimastes praktikumides on ülesanded, mida on soovitatav lahendada plugin-at kasutades. Kui tarkvara paigaldamine õnnestus, saate läbida allpool toodud harjutuse.

Mac OS X - Intel (Homebrew)

 brew install rlwrap
 brew install idris2

Windows 10 (WSL)

  • Paigaldada WSL (soovitatavalt WSL2 aga WSL1 töötab ka.)
  • Installida WSL-i Ubuntu-22.04 (Microsoft store kaudu või käsurea käsuga ubuntu)
  • Installida Idris2 kasutades Ubuntu käsurida:
 sh <(curl -L https://nixos.org/nix/install) --daemon
 exit
 nix-env -i idris2
 nix-env -i rlwrap
  • Installida VS Code Windowsi (vt. õpetust all)

Windows (mitte WSL)

  • Õpetused TalTech-i FP kursusest: https://cs.taltech.ee/staff/iavara/idris/
  • Muidugi töötab ka VirtualBox+Ubuntu-22.04 aga siis peate ka VS Code linuxisse installima.

Linux (nix)

Käsureal täita järgnevad käsud. Esimene käsk installib nixos-i siis tuleb terminal sulgeda ja uuesti avada. Kolmas käsk installib idris2-e.

 sh <(curl -L https://nixos.org/nix/install) --daemon
 exit
 nix-env -i idris2
 nix-env -i rlwrap

Ubuntu (apt) kui nix ei tööta

 sudo apt update
 sudo apt install chezscheme git build-essential libgmp-dev rlwrap
 wget https://github.com/idris-lang/Idris2/archive/refs/tags/v0.7.0.tar.gz
 tar -xvzf v0.7.0.tar.gz
 cd Idris2-0.7.0
 make bootstrap SCHEME=scheme
 make install
 cd ..
 echo 'export PATH="$HOME/.idris2/bin:$PATH"' >> ~/.bashrc
 echo 'export LD_LIBRARY_PATH="$HOME/.idris2/lib:$LD_LIBRARY_PATH"' >> ~/.bashrc

Visual Studio Code

  1. Lae alla ja paigalda VS Codium või VS Code
    • Ubuntus: sudo apt install code*.deb
  2. Käivita VS Code
  3. WSL puhul paigalda laiendus "WSL" ja käivita code Ubuntust
  4. Paigalda laiendus "Idris Language" (meraymond)
    • Laienduse "Idris Language" sätetes vali: Idris2 Mode ja Idris Path pane "idris2"
    • Seadista klahvikobinatsioonid järgnevalt:
      1. Kopeeri seadistus laienduse detailidest (Keybindings alt)
      2. Ava: File -> Preferences -> Keyboard Shortcuts
      3. Keyboard Shortcuts vahelehel paremal üleval väike ikoon "Open Keyboard Shortcuts (JSON)"
      4. Nüüd asenda/lisa sinna kopeeritud seadistused.
  5. Arendamisel avage VS Code-s vastav kataloog (kui avate ainult faili siis ei pruugi laiendus töötada)
    • Näiteks käsurealt: codium .

VIM

  • Idrise looja Edwin Brady kasutab arendamiseks oma vim-i režiimi

Töökeskkonna tutvustus

Selle kursuse ülesandeid on mugav lahendada selliselt, et samal ajal on lahti koodiredaktor (näiteks VS Codium) ja käsurida/terminal Idris2 REPL-ga. Suurema monitoriga/ekraanilahutusega saavad need aknad olla kõrvuti. Sülearvutil võib olla mugavam kui mõlemad on täisekraanis s.t. vahetada nende vahel Alt-Tab/Command-Tab ga.

Tehke läbi järgnev lühike harjutus:

  1. Avage käsurida, kus saate idrist käivitada.
  2. Looge uus kataloog: mkdir idris_test
  3. Minge sinna kataloogi: cd idris_test
  4. Looge fail test0: touch test0.idr
  5. Avage VSCode: code .
  6. Käivitage REPL: rlwrap idris2 test0.idr
    • Kui teil ei õnnestunud rlwrap-i installimine, siis kasutage lihtsalt idris2 test0.idr
  7. REPL-is arvutage midagi: 5+5+5
  8. Kopeerige järgnev kood VSCode-s avatud faili (ärge salvestamist unustage)
 liida5 : Int -> Int
 liida5 x = x+5
  1. Laadige REPL-is fail uuest: :r
  2. REPL-is arvutage: liida5 (5+5)
  3. Hõljuge hiirega liida5 kohal
    • Peaks tekkima kastike Main.liida5: Int -> Int
  4. Lisage faili lõppu kommentaar -- liida5 1
  5. Selekteerige redaktoris avaldis liida5 1, vajutage klahvikombinatsioon Ctrl-Alt-i
    • Peaks tekkima juurde => 6
  6. Sule REPL: :q
  • Arvutiteaduse instituut
  • Loodus- ja täppisteaduste valdkond
  • Tartu Ülikool
Tehniliste probleemide või küsimuste korral kirjuta:

Kursuse sisu ja korralduslike küsimustega pöörduge kursuse korraldajate poole.
Õppematerjalide varalised autoriõigused kuuluvad Tartu Ülikoolile. Õppematerjalide kasutamine on lubatud autoriõiguse seaduses ettenähtud teose vaba kasutamise eesmärkidel ja tingimustel. Õppematerjalide kasutamisel on kasutaja kohustatud viitama õppematerjalide autorile.
Õppematerjalide kasutamine muudel eesmärkidel on lubatud ainult Tartu Ülikooli eelneval kirjalikul nõusolekul.
Courses’i keskkonna kasutustingimused