Functional Programming

What it covers

• The functional core: recursion, pattern matching, algebraic data types, higher-order functions (map, filter, fold)
• The abstraction ladder (the course's steepest climb, strictly hierarchical): Type Classes → Functors → Applicative Functors → Monads
• Specific monads in practice: IO, State; lazy evaluation and infinite data structures
• Agda: dependent types (Vec, Fin), the Curry-Howard correspondence, equational reasoning and formal proofs of program properties

Assessment

Course project (35%) + final written exam (65%); each ≥5.0, final grade ≥5.8. The project is typically a Haskell application (e.g. a jq clone) synthesizing ADTs, parsing, and monadic structuring. The exam mixes Haskell and Agda: theory questions, implementing Functor/Applicative/Monad instances for a given type, QuickCheck property tests, evaluation-strategy tracing, plus three dedicated Agda questions (dependent types, Curry-Howard proof, equational reasoning).

Worth knowing

• No past exams are archived in this folder — check the LLM bundle's Exams.md for exam-style questions.
• The Type Class → Functor → Applicative → Monad chain is strictly cumulative: a shaky grasp of higher-order functions early on will make Monads incomprehensible later. Don't cram this course.
• The Agda half assumes Reasoning & Logic as background — if that course felt shaky, revisit it before Agda starts.
• The project is individual, not paired — no code-sharing with classmates, only general discussion.