Functional Programming and Proof Checking Course Plan

How to read this

Entry format:

* <text> | <resources to read>

Introduction

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 $\lambda$-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, $\alpha$-conversion, $\beta$-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 $\lambda$.
• Implementing untyped lambda interpreter in Haskell.

Simply-typed $\lambda$-calculus ($\lambda_{\to}$)

Resousces: ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps, https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385, http://www.win.tue.nl/~hzantema/semssm.pdf, http://www.cs.cmu.edu/~crary/819-f09/DamasMilner82.pdf, http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-rank/index.htm, https://personal.cis.strath.ac.uk/adam.gundry/type-inference/, http://requestforlogic.blogspot.com/2010/10/type-inference-in-and-out-of-context.html.

• Church-style $\lambda_{\to}$. Important properties: Subject Reduction, Strong Normalization.
• Recursion.
• Convertability relation. Why it matters.
• Curry-style. Mixed (Haskell) style.
• Type inference for $\lambda_{\to}$.
• Implementing type inference in Haskell.

Primitive Haskell

Resources: http://www.haskell.org/haskellwiki/Typeclassopedia, http://www.haskell.org/tutorial/, http://www.rsdn.ru/article/haskell/haskell_part1.xml, http://www.rsdn.ru/article/haskell/haskell_part2.xml.

• 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, http://www.haskell.org/haskellwiki/Monads_as_computation, http://www.haskell.org/haskellwiki/Monads_as_containers, http://www.haskell.org/haskellwiki/Typeclassopedia, http://www.cse.chalmers.se/~rjmh/Papers/arrows.pdf, http://www.soi.city.ac.uk/~ross/papers/fop.html.

• Different definitions for monads: bind, fish, fmap/join,
• and their equivalence.
• Standard monads:
  • Maybe.
  • List.
  • State.
  • IO. Mocking IO by State with $s \equiv 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: http://www.haskell.org/ghc/docs/latest/html/users_guide/index.html, especially http://www.haskell.org/ghc/docs/latest/html/users_guide/using-ghc.html 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. | http://www.haskell.org/ghc/docs/latest/html/users_guide/primitives.html
• Reading GHC Core. | http://www.haskellforall.com/2012/10/hello-core.html, http://stackoverflow.com/questions/6121146/reading-ghc-core (see cited links!)
• Dumping optimizations. Profiling. | http://www.haskell.org/ghc/docs/latest/html/users_guide/options-debugging.html, http://www.haskell.org/ghc/docs/latest/html/users_guide/runtime-control.html, http://www.haskell.org/ghc/docs/latest/html/users_guide/profiling.html

Making Haskell Programs Efficient

• When and where should I add strictness annotations? Niffty tricks.
• From high-level abstraction to optimal assembly: deforestation, stream fusion. GHC’s rewrite “RULES”.
• Data structures: UArray (doesn’t compile anymore :( ), Data.ByteString, Data.Text. | https://bitbucket.org/bos/text/src (read the source!)
• When nothing else helps: CPS transformation, FFI and unsafePerformIO. | http://users.aber.ac.uk/afc/stricthaskell.html

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.

Primitive Agda

• =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.

Needs more logic

• From Frege to type theory.
• Brief introduction to Martin-Löf’s system: $\Pi$, $\Sigma$ and $I$ types.
• Some notes on impredicativity in type theory.