CSE3100: Functional Programming

Functional programming is a style of programming where programs are constructed by defining and applying functions. In pure functional code, the output of a function only depends on the value of its arguments, so the same expression always produces the same result. This is in sharp contrast to imperative and object-oriented languages, where every statement can have side effects that influence the results of other statements.

Apart from the absence of side-effects, another important feature of most functional programming languages are their powerful type systems. By modeling the different classes of data used in a program, types can be used to structure programs and detect many common errors that would otherwise go unnoticed. Certain languages with so-called dependent type systems can even specify any imaginable functional property in the type of a program, guaranteeing that the program works as it is supposed to before it is ever executed.

Why study functional programming?
• Functional programming allows you to model the real world at a high level of abstraction in order to develop software that is clear, concise, and correct.
• By learning functional programming, you will also learn new ways to think about programs that make you a better programmer in any programming language.
• Functional programming languages are becoming increasingly commonplace, and other mainstream languages are integrating more functional features (lambdas, higher-order functions, pattern matching, immutable data, …)
• Pure functional programming makes it easy to reason about program correctness by using techniques such as equational reasoning, property-based testing, and formal verification.
• Static typing and immutability allow you to quickly change and refactor an existing program with confidence that the result is correct.
• Functional programming languages such as Haskell and Agda include many recent developments from the research on programming languages, which usually take 10 to 30 years to make their way into mainstream languages. By learning them you will get an idea how the future of programming languages might look like.

In the first part of this course, you will learn how to program in Haskell, a purely functional programming language. Concretely, you will learn…
• how to write programs that can manipulate and return functions as first-class data.
• how to define and manipulate your own data structures, by using algebraic datatypes, pattern matching, and recursion.
• how to automatically test important properties of your programs with the QuickCheck tool.
• how to avoid code duplication and write code at a higher level of abstraction by using type parameters and type classes.
• how to avoid unneccessary computation and program with infinite data structures by relying on lazy evaluation.
• how to distinguish between pure and impure computations, and use monads to write programs that make this difference explicit.

In the second part of this course, you will learn how to use Agda, another purely functional programming language that is similar to Haskell but has a more powerful dependent type system. In this part, you will learn…
• how to express logical properties as types through the Curry-Howard correspondence.
• how to develop Agda programs interactively with the typechecker and detect errors as you are writing the program.
• how to enforce invariants of your programs at the type level by using indexed datatypes and dependent pattern matching.