Entry format:

`* <text> | <resources to read>`

There are two ways to learn:

- The decent one, where you start from theory and dash forward. There is a blog post about that.
- The “Real-World” one, where you start playing with Haskell trying to deduce (usually wrongly) what’s going on behind the scenes. “The book” for that approach is Learn You a Haskell for Great Good!.

We’ll try to switch between these two approaches in class. Here is the plan.

- Functions, Values, Types, Algebraic Datatypes (ADT), Pattern Matching | first 4 chapters from Gentle Introduction (Russian translation exists: part1, part2)
- Implementing Naturals, Integers, and Rationals with ADT.
- Lists and trees, maps and folds.
- Implementing standard library for pure type-classes-less Haskell: naturals, integers, rationals, lists, trees, associative arrays.

Resources: first 50 pages or so from TTFP, first sections from Selinger’s notes, first chapters from Sørensen, Uzryczyn.

- Definitions: pre-terms, terms,
*α*-conversion,*β*-reduction. - Booleans, naturals and simple computations.
- Omega and Y, fixed points and recursive functions.
- Normalization orders. Important properties: normal order normalization.
- Important properties: substitution lemma, Church-Rosser.
- Translating simple Haskell (especially datatypes) into
*λ*. - Implementing untyped lambda interpreter in Haskell.

Resousces: barendregt, thompson-ttfp, sorensen-urzyczyn, semssm, damas-milner, ptihr, tiic, tiioc.

- Church-style
*λ*_{ → }. Important properties: Subject Reduction, Strong Normalization. - Recursion.
- Convertability relation. Why it matters.
- Curry-style. Mixed (Haskell) style.
- Type inference for
*λ*_{ → }. - Implementing type inference in Haskell.

Resources: typeclassopedia, gentle-introduction-to-haskell, gentle-introduction-to-haskell-ru-1, gentle-introduction-to-haskell-ru-2.

- Abstract algebra: Monoid, Group, Ring. Category theory: Category, Functor, Natural Transformation. How this relates to our library.
- Introducing Type-classes. To our library.

- Hindley-Milner type inference. Type checking and type inference in presence of type-classes.
- Type-classes are functions’ arguments.
- GHC’s extensions for type-classes and ADTs. Packing up a type-class into ADT.

Resources: corresponding chapters from Gentle, monads-as-computation, monads-as-containers, typeclassopedia, arrows, fop.

- Different definitions for monads: bind, fish, fmap/join,
- and their equivalence.
- Standard monads:
- Maybe.
- List.
- State.
- IO. Mocking IO by State with
*s*≡*R**e**a**l**W**o**r**l**d*where*R**e**a**l**W**o**r**l**d*is a datatype. - Monadic parser combinators.

- Concantenative programming.
- Arrow, Applicative, Applicative Arrow.
- Applicative Arrows are Monads.
- Interesting Arrows (that are not Monads): stream processors.

Resources: ghc-user-guide, especially ghc-using-ghc chapter.

- Haskell heap structure: thunks/closures, boxed values. Case is force. Bottom propagation. | The Haskell Heap series here (bottom to top)
- Computation primitives: seq (pseq), par. Parallel computations in Haskell are easy (kind of). DeepSeq, Parallel.Strategies.
- Unboxed types and primitives. | ghc-primitives
- Reading GHC Core. | haskell-core, reading-ghc-core (see cited links!)
- Dumping optimizations. Profiling. | ghc-debugging, ghc-runtime-control, ghc-profiling

- When and where should I add strictness annotations? Niffty tricks.
- Form high-level abstraction to optimal assembly: deforestation, stream fusion. GHC’s rewrite “RULES”.
- Data structures: UArray (doesn’t compile anymore :( ), Data.ByteString, Data.Text. | bos-text (read the source!)
- When nothing else helps: CPS transformation, FFI and unsafePerformIO. | stricthaskell

- Datatypes and records syntax. ⊥, ⊤, ℕ. Function syntax. Common operations for naturals.
- Type families. Encoding simple predicates for ℕ as functions to
`Set`

and as type families. - Dependent types and dependent pattern matching: let’s rule out the impossible cases with ⊥!
- Convertability relation again. Pattern unification.
- Type families and dependent pattern matching: dotted patterns are (more or less) inlined unification constraints.
- Famous type family: propositional equality.
- Proving equality properties for naturals.

`List`

s,`Vec`

tors,`Fin`

s.`map`

s,`filter`

s and related stuff.- High-order relations: Reflexive, Symmetric, Transitive, Substitutive, Decidable, Trichotomous.
- Using relations in proofs and programs.
- Constructive set theory for
`List`

s.

- From Frege to type theory.
- Brief introduction to Martin-Löf’s system: Π , Σ and
*I*types. - Some notes on impredicativity in type theory.