CS410-17

being the lecture materials and exercises for the 2017/18 session of CS410 Advanced Functional Programming at the University of Strathclyde

Strathclyders only: one minute papers and lecture videos will appear on our Marx site.

Installation instructions

0. Check if you're using bash $ echo $0

1. If using bash: Add "export PATH=$HOME/.cabal/bin:$PATH" to the bottom of your .profile file if it isn't already there. Else if using tcsh: Add "set path = ($home/.cabal/bin $path)" to the bottom of your .cshrc file if it isn't already there.

2. $ cabal update

3. $ cabal install alex

4. $ cabal install cpphs

5. $ cabal install happy

6. $ cabal install Agda

7. $ agda-mode setup

8. $ emacs test.agda -- You should see an Agda menu and (Agda) in the mode line.

9. $ git clone https://github.com/pigworker/CS410-17

Lecture videos on YouTube

1. Tuesday 19 September Programs and Proofs
2. Friday 22 September more Programs and Proofs, Introducing "with"
3. Tuesday 26 September Proof by Induction
4. Friday 29 September Sigma, Difference, Vector Take
5. Tuesday 3 October How Rewrite Works
6. Friday 6 October A Comedy of (Entirely Non-Deliberate) Errors
7. Tuesday 10 October "Dominoes", no really, this time
8. Friday 13 October Functors
9. Tuesday 17 October From Functors to Monads
10. Friday 20 October Natural Transformations and Monads
11. Tuesday 24 October From Monads to Input/Output
12. Friday 27 October How to Run a Program (and come a-cropper) bug report
13. Tuesday 31 October Monads on Indexed Sets (Ex2)
14. Friday 3 November What is an Application?
15. Tuesday 7 November Coinduction and Coalgebras
16. Friday 10 November Polynomial Data and Codata
17. Tuesday 14 November A Polynomial Universe
18. Friday 17 November The Zipper (Differentiating Polynomial Types)

Other useful stuff

1. SpaceMonads! my keynote from CodeMesh 2016, on which Ex2 is based