Functional Programming

• Tuesdays 10:00-11:30, ICT-A2.
• Wednesdays 10:00-11:30, ICT-404.
• Course code: ITI0212.

Project

• Course project – due 24 April 2020
• You should use draw_board.idr as a starting point.

Exam

You should have received a link to a Doodle poll where you can choose the time for your oral examination. A zoom link will be emailed to you shortly before the time of your examination.

• the examination is oral
• it is required that you have access to a computer with Idris installed. The exam will begin with the examiners giving you 6 problems. The problems are designed so that a typical examination takes 30-60 minutes.
• The problems are closely related to the exercise sheets. The first problem will be from exercise sheets 1 and 2, the second from exercise sheets 3 and 4, and so forth. The best way to prepare for the exam is to make sure that you can solve the problems from the exercise sheets.
• We will require you to share your screen so that we can see you solve the problems.
• You can do the problems in any order. You can start and come back to problems. If you get stuck we can offer you hints.

Homework assignments

• Homework assignment 1.
• Homework assignment 2.
• Homework assignment 3. (review problems)

Exercises

• Exercise sheet 1.
• Exercise sheet 2.
• Exercise sheet 3.
• Exercise sheet 4.
• Exercise sheet 5.
• Exercise sheet 6.
• Exercise sheet 7.
• Exercise sheet 8.
• Exercise sheet 9.
• Exercise sheet 10.
• Exercise sheet 11.
• Exercise sheet 12.

Lectures

• Lecture 1. Introduction. 28 January.
• Lecture 2. Basic functions. 4 February.
• Lecture 3. Higher-order functions. 11 February.
• Lecture 4. A bit of dependent types. 18 February.
• Lecture 5. I/O and Maybe. 10 March
• Lecture 6. Data and Folds. Available in two parts: audio and screencast. The screencast is viewable with asciinema. 24 March
• Lecture 7. Some Functional Data Structures. 31 March
• Lecture 8. Shapely Types. 7 April (Idris source files: shaped lists, shapeless trees, shapely trees, )
• Lecture 9. Interfaces. 14 April (notes, examples)
• Lecture 10. Propositions as Types. 21 April (even.idr, leq.idr)
• Lecture 11. Equality Types. 28 April (script)
• Lecture 12. Negation and Decidability. 28 April (script)

Labs

• 6th Lab, 25 March.
  • Exercise sheet 6.
  • Ask questions in channel #taltechiti0212 on irc.freenode.org!
• 5th Lab, 18 March.
  • Exercise sheet 5.
• 4th Lab, 11 March.
  • Exercise sheet 4.
  • Solutions.
• 3rd Lab, 26 February.
  • Exercise sheet 3.
• 2nd Lab, 12 February.
  • Exercise sheet 2.
• 1st Lab, 29 January.
  • Install Idris.
  • Install Atom (or Emacs).
  • Install the package language-idris (inside Atom).
  • Windows may need you to add the folder containing idris.exe to the PATH system variable.
  • Exercise sheet 1.

Materials

The primary textbook of the course is “Type-Driven development with Idris” by Edwin Brady, available online via the library. Complementary material is “Learn you a Haskell for Great Good!” by Lipovača, and “The craft of functional programming”, by Thompson.

• Extra exercises: you can try to solve the 99 Haskell Problems in Idris. You can find koans from the group of Idris Hackers; and Edwin Brady has some basic exercises.