How to read this
* <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.
Introduction to Haskell
- 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.
Introduction to untyped λ-calculus
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.
Simply-typed λ-calculus (λ → )
Resousces: barendregt, thompson-ttfp, sorensen-urzyczyn, semssm, damas-milner, ptihr, tiic, tiioc.
- Church-style λ → . Important properties: Subject Reduction, Strong Normalization.
- 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 and Type Classes
- 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.
Monads and Arrows
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:
- IO. Mocking IO by State with s ≡ RealWorld where RealWorld is a datatype.
- Monadic parser combinators.
- Concantenative programming.
- Arrow, Applicative, Applicative Arrow.
- Applicative Arrows are Monads.
- Interesting Arrows (that are not Monads): stream processors.
Haskell Programs on a Real Hardware. GHC Hacking
Resources: ghc-user-guide, especially ghc-using-ghc chapter.
Making Haskell Programs Fast
- 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
Introduction to Agda
- 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.
filters and related stuff.
- High-order relations: Reflexive, Symmetric, Transitive, Substitutive, Decidable, Trichotomous.
- Using relations in proofs and programs.
- Constructive set theory for
Needs more logic
- From Frege to type theory.
- Brief introduction to Martin-Löf’s system: Π , Σ and I types.
- Some notes on impredicativity in type theory.