Functional Programming

Lambda calculus

    Lecture

    Functional vs. imperative programming.
    Lambda Calculus. Application and abstraction.

    Free and bound variables. Combinators.
    Function of multiple variables, currying.
    Substitution, substitution lemma.

    Beta- and eta-conversion.
    Extensions of pure lambda calculus, delta-conversion.

    Lab

    Lambda Calculus as a programming language.
    Encoding boolean values and pairs.
    Church numerals and simple operations on them.

Recursion and reduction

    Lecture

    Fixed point theorem, Y-combinator.

    Redexes. One- and multi-step reduction. Normal form. Reduction graphs.

    Church-Rosser theorem and its corollaries. Reduction strategies.
    Normalization Theorem.

    Lab

    Church numerals: predecessor, subtraction. Primitive recursion. Lists.
    Turing and Curry fixed point combinators.

Simply typed lambda calculus

    Lecture

    Types in programming languages.

    Preterms. Typing statements. Contexts. Church and Curry systems.

    Properties of typed lambda calculus. Relating the Church and Curry systems.

    Decidability of type assignment. Strong end weak normalization. Curry-Howard correspondence.

    Lab

    Type inference for the Church and Curry systems.

Introduction to Haskell

    Lecture

    Language specification. GHC compiler and interactive environment. Hoogle.

    Variable binding. Function encoding. Recursion.

    Syntax of Haskell expressions. Modules.

    Partial application, currying. Infix operators, sections. Point-free style.

    Lab

    Recursive function encoding

Programming in Haskell

    Lecture

    Errors. Bottom. Strict and nonstrict functions. Lazy and eager evaluation. Seq.

    Algebraic data types. Pattern matching and its semantic.

    Type и newtype declarations. Field labels.

    Lab

    Lists. Standard operations on lists. High order functions.
    "Infinite" data structures. List comprehension.

Haskell type system

    Lecture

    Parametric and ad hoc polymorphism. Type classes.
    Instance declaration. Example: classes Eq and Ord.

    Kinds. Type operators as a parameter of type class declaration.
    Class Functor.

    Implementation of type classes.

    Lab

    Standard type classes: Enum and Bound, Num, Show and Read.

Applicative functors and folds

    Lecture

    Functor laws. Type class Applicative and its instances.
    Two ways of declaring lists as an applicative functor. Type class Alternative.

    Monoids. Instances of Monoid type class.

    List folds. Left and right folds. Lazy and strict versions of fold.

    Type class Foldable.

    Lab

    Usage of applicative functors and folds.

Monads

    Lecture

    Monads. Type class Monad. Example: monad Identity.

    Laws of Monad. Do-notation.

    Maybe monad: computations in the context of possible failure.

    List monad: computations with multiple results.

    Lab

    Programming with standard monads.

Using monads

    Lecture

    Input/output in pure languages. IO monad. Interactions with file system.

    Monads for logging, reading from constant environment and working with mutable states: Reader, Writer, State.

    Lab

    Input/output. Working with (pseudo)random values.

Monad transformes

    Lecture

    Type class Alternative. Regex parsers. Type class MonadPlus.

    Error monad: computations which may throw exceptions.

    Cont monad: computations which can be interrupted and resumed.

    Combining monadic effects. Monad transformers.

    Lab

    Monadic computations with multiple effects.

Type inference

    Lecture

    Type inference. Principle (most general) type. Properties of the type substitution.

    Composition of the type substitution.

    Unificator, unification theorem. Principle pair. Hindley–Milner algorithm.

    Lab

    Hindley–Milner type inference algorithm in Haskell.

Polymorphic type systems

    Lecture

    A weak and a strong version of polymorphism. Let-polymorphism. High order polymorphism.
    Universal abstraction and application. Impredicativity. Strong normalization.

    Systems with dependent types. Type families. Kinds for type families. Type of dependent product.

    Lab

    Generalized algebraic datatype (GADTs). Existential types.
    Type families in Haskell. Type-level programming.

Parametricity

    Lecture

    Parametricity as a property of polymorphic type systems. Reynolds abstraction theorem.
    Free theorems

    Lab

    Optimizations with rewriting rules in GHC. Fold/build rule.

Purely functional data structures

    Lecture

    Immutable data structures and efficient algorithms. Significance of the lazy evaluation.

    Amortized complexity. Zippers. Flexible arrays.